### Spring 2002, CSE 428: Assignment 2

Distributed: Jan 26.
Due: Feb 7 in class.
Total maximum score: 100 points.

The purpose of this assignment is to provide experience with interpretation of expressions and simple commands.
1. [Points 20] Consider the following boolean expressions:

(1) if x = 0 then true else (x = 1 or x > 1 or 1/x > 1).
(2) x = 0 or x = 1 or x > 1 or 1/x > 1

Assuming that x is declared as an integer, and that at the moment in which the expressions are evaluated x is associated to a non-negative number, say what are the results (true, false or error), depending on the value of x, of (1) and (2) when
(a) "or" is interpreted as a strict operator
and when
(b) "or" is interpreted as a non-strict operator

2. [Points 20] Assume that we want to enrich the language of boolean expressions with the boolean operator "implies" (logical implication), by adding the production

Exp ::= Exp implies Exp

and with the following meaning:

r |- e1  eval  false
---------------------------
r |- (e1 implies e2) eval true

r |- e1  eval  true     r |- e2  eval  v
------------------------------------------------
r |- (e1 implies e2)  eval v

Say what is the result (true, false or error) of the following expression, where x is declared as an integer:

x > 0 implies (x = 1 or x > 1 or 1/x > 1)

3. [Points 10] For each of the following three while commands, say for which initial values of x it eventually terminates. Assume that x is declared as an integer variable.

(1) while x > 0 do x := x - 1
(2) while not (x = 0) do  x := x - 1
(3) while x > 0 do x := x + 1

Note: we say that a while command "terminates" when the condition is or becomes false (sooner or later).

4. [Points 20] Assume that we have the following type rules for a small language of expressions.

tm |- Exp1 : real   tm |- Exp2 : real
________________      _______________________________________
tm |-  x : tm(x)             tm |- Exp1 + Exp2 : real

tm |- Exp : int        tm |- Exp1 : int   tm |- Exp2 : int
________________       _______________________________________
tm |- Exp : real              tm |- Exp1 + Exp2 : int

Assume also that the variables x and y are also allowed as expressions. Write down all the type mappings, tm, such that tm assigns these two variables a type and such that

tm |- x + y : real

is provable.

5. [Points 30] Consider two looping constructions. The while loop is given an operational semantics in class and on page 59 of the textbook. Consider the repeat-until loop given by the following operational semantics. (This loop operator is inspired by one in Pascal and is sometimes called a do.)

sigma1 |- Stm ==> sigma2     sigma2 |- Exp eval false
_____________________________________________________
sigma1 |- repeat Stm until Exp ==> sigma2

sigma1 |- Stm ==> sigma0
sigma0 |- Exp eval true
sigma0 |- repeat Stm until Exp ==> sigma2
________________________________________________________________
sigma1 |- repeat Stm until Exp ==> sigma2

(This last rules has three premises, listed over each other so it fits on a page better.) Do the following two things:

1. Write an expression using sequencing (semicolon), conditional, and while that is equivalence to repeat-until.
2. Write an expression using sequencing (semicolon), conditional, and repeat-until that is equivalence to while.

If you wish, you may also use the skip statement, if necessary, which is defined as simply

___________________________
sigma |- skip ==> sigma