Written Assignment 4

In these problems, you’ll be working with the basic imperative language (a so-called While-language) we saw in class. We rst set up the language grammar.

Var x ::

AExp a ::= x j Z j a1 + a2 j a1    a2 j
BExp b ::= b1 && b2 j a1 < a2 j
Comm c ::= skip j x    a j c1; c2 j if b then c1 else c2 j while b do c

In words, we have:

program variables (we use the letter x for any variable);

arithmetic expressions (we use the letter a for any arith expr.); boolean expressions (we use the letter b for any boolean expr.); commands (we use the letter c for any command).

In our language all variables will be integer-valued; we use the letter n for any numeric constant (like 42). In imperative languages, the behavior of a program depends on the current state of its variables. We will

model this state with a store s, a function mapping every variable in Var to an integer in Z. We write s(x) to mean the current value of x in s, and we write s[x 7!n] to mean the updated store where all variables hold the same value as in s, except variable x is updated to hold the integer n. Throughout, we use the letter s for any store.

Each arithmetic expression represents an integer in a given store s. We can de ne:

s(n) = n

s(a1 + a2) = s(a1) plus s(a2)
s(a1    a2) = s(a1) times s(a2)

and so on. The right-hand side of each case above is a number|we write \plus" and \times" out to emphasize that these are the mathematical addition and multiplication on numbers, not symbols in a program. Likewise, each boolean expression represents a boolean in a given store s. We can de ne:

s(b1 && b2) = s(b1) and s(b2)
s(a1 < a2) = s(a1) is less than s(a2)

and so on. Again, the right-hand side of each case is a boolean.

Running a command changes the store|it may write to variables in memory. Furthermore, the next command to execute also depends on the store. Accordingly, we will de ne an operational semantics on con gurations, (command, store) pairs: (c; s) ! (c0 ; s0 ) means that running command c on store s leads to a new store s0 and a remaining command c0 . The operational semantics are as follows:

1




s(a) = n



(c1; s) ! (c10 ; s0 )








(x   a; s)
!
(skip; s[x   n])
(c
; c
; s)
!
(c0
; c
; s0 )

(skip; c ; s)
!

(c
; s)




7!

1
2



1
2


2


2





s(b) = true












s(b) = false






















(if b then c1 else c2; s) ! (c1; s)




(if b then c1 else c2; s) ! (c2; s)







s(b) = true












s(b) = false















(while b do c; s) ! (c; while b do c; s)




(while b do c; s) ! (skip; s)


The pair (skip; s) does not step: this is the halting con guration, representing a program that is done.

    • While-language: basics (15)

Suppose there are just two variables: x and y. We’ll write [n1; n2] for the store where x holds n1 and y holds n2. Using the operational semantics and starting in the initial store s0 = [0; 0] (i.e., x and y are initialized to zero), step the following con gurations until they reach the halting con guration:

(a)
(x
x + 1; s0)


(b)
(x
3; y   y + x; s0)


(c)
(if x < y then x   2 else x
2; s0)

(d)
(x
1; if x < y then x
2 else x
2; s0)
(e)
(x
2; while y < x do y
y + 1; s0)


For each problem, you should write down a sequence (c1; s1) ! (c2; s2) ! ! (cn; sn), where the last pair should be (skip; s) for some store s. Of course, your answers should involve speci c commands and stores rather than using the letters c and s.

    • While-language: conditionals (10)

Rust’s match construct is like a conditional command. We’ll model a baby version of this feature, adding the following syntax to our language:

Comm c ::=    j cond fb ) c;  ) c0 g j cond fb1 ) c1; b2 ) c2;  ) c3g


The idea is that cond fb ) c; ) c0 g executes c if b is true in the initial store, otherwise it executes c0 . Likewise, cond fb1 ) c1; b2 ) c2; ) c3g executes c1 if b1 is true, otherwise it executes c2 if b2 is true, otherwise it executes c3. Note that the arms are considered in order|left to right|and the guards b1; b2 might overlap.


Extend the operational semantics to handle these features. Do not use if-then-else for this part! Hint: you can get by with four new rules like the ones above: two for stepping the two-armed conditional, and two for stepping the three-armed conditional.








2
    • While-language: do-until (5)

We can also extend the language with a do-until loop:

Comm c ::=    j do c until b

This command should always execute the body c at least once. Then, it should exit if b is true, and continue looping if b is false.

Extend the operational semantics to handle this kind of loop. Do not use While loops for this part! (You can use everything else, though.) Hint: you can get by with just one new rule.




















































3