[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
[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)
[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).
[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.
[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:
If you wish, you may also use the skip statement, if necessary, which is defined as simply
___________________________ sigma |- skip ==> sigma