CS 440: Programming Languages Assignment: Big-step semantics
IMP Rules
CS 440: Programming Languages
Assignment: Big-step semantics
The following are the big-step semantic rules of the simple imperative language (IMP) as described in class.
LITERAL <i,σ>⇓e i when i∈Z VAR <u,σ>⇓e v if u:=v ∈ σ < e1,σ >⇓e v1 < e2,σ >⇓e v2
ARITH
< e1 ⊕ e2, σ >⇓e v1 ⊕ v2 Figure 1: Arithmetic expressions
LITERAL <b,σ>⇓b b if b∈{true,false} VAR <u,σ>⇓b v if u:=v ∈ σ < e1,σ >⇓e v1 < e2,σ >⇓e v2
REL
<e1 ve2,σ>⇓b v1 vv2 Figure 2: Boolean expressions
SEQ
SKIP <skip,σ>⇓σ <S1,σ>⇓σ′ <S2,σ′ >⇓σ′′
<S1;S2,σ>⇓σ′′
< b,σ >⇓b false < S2,σ >⇓ σ′
< e, σ >⇓e v ASSIGN <x:=e,σ>⇓σ[x:=v]
<b,σ>⇓b true <S1,σ>⇓σ′ IF-T <ifbthenS1 elseS2,σ>⇓σ′
IF-F <ifbthenS1 elseS2,σ>⇓σ′ <b,σ>⇓b true <S,σ>⇓σ′
< b,σ >⇓b false WHILE-F <whilebdoS,σ>⇓σ
WHILE-T
<whilebdoS,σ′ >⇓σ′′ < while b do S, σ >⇓ σ′′
Figure 3: Statements
1
Logistics and Submission
Please submit your solutions as a PDF (typed or neatly handwritten!) on Blackboard by the due date.
1
1. 2.
Extending the language
(5 points) We wish to add Boolean negation to IMP, via the ! operator. Write down inference rules to describe the big-step semantics of this operator.
(10 points) We wish to add for loops to IMP, which will have the form “for v in a0 to a1 do S”, which will run statement S with the variable v taking on values a0 , a0 + 1, ..., a1 . E.g., “for x in 1 to 5 do S” will run S with x taking on values 1, 2, 3, 4, 5, in that order.
Write down inference rules to describe the big-step semantics of the for statement. Note that the loop variable is allowed to clash with pre-existing variables, and it may remain in the environment after the loop completes.
2 Proofs
-
(5 points) Draw a proof tree for the following assertion:
< t := a + b; a := b; b := t, {a := 5, b := 10} >⇓ {t := 15, a := 10, b := 15} -
(5 points) Draw a proof tree for the following assertion:
< if x > y then m := x ∗ 10 else m := y ∗ 10, {x := 10, y := 20} >⇓ {x := 10, y := 20, m := 200} -
Consider the program P = “for x in m to n do sum := sum + x” (which makes use of the for statement defined in the previous section). Note that m and n are not variables, but represent arbitrary integer constants.
-
(a) (5 points) Describe the environment σ′ such that < P, σ0 >⇓ σ′, where σ0 is an environment which maps all variables to 0. Hint: you may make use of the summation operator (Σ).
-
(b) (5 points) Write down a program Q using the while statement, which is semantically equivalent to P.
-
(c) (10 points) Prove that P and Q are equivalent when run in starting state σ0.
-
2
