Programming Language Comprehensive, January, 1996

Instructions. Do all 6 questions. You have 2 hours.

Question 1: The command sequence below is partially correct with respect to the pre- and postconditions given. Explain why the command sequence terminates whenever the precondition holds. Give a loop invariant that, together with the assumption of termination, implies the postcondition.

{Y ≥ 0} J := 1; Z := X; K := Y; while K > 0 do

if odd(K) then J := J ∗ Z; K:=(K div 2); Z := Z ∗ Z)

{J = XY}

Question 2: Suppose we have a programming language P and we provide a denotational semantics for it. Suppose we then go on to provide a formal system of axioms and rules. Discuss the relationship between the denotational semantics and the formal system of axioms and rules. Give an example of the denotation of a construct from Tennent’s mini-imperative language. What is the rule of inference corresponding to the while-statement.

Question 3: State Hoare’s axiom for assignment statements, and explain why it is valid. Explain why a specification such as {false} C {0 = 1} is valid.

Question 4: Give the semantic equation for the local-definition block

let ι be P in Q .

Explain how the informal expression

(λ ι Q)P

explains the semantics of the local definition block.

Question 5: Give an example of a syntactical programming language construct which is NOT context-free, and briefly sketch an explanation for your example.

Question 6: What is the fundamental idea behind the semantics of

letrec ι : Θ be P in Q

Explain the distinctions between

letrec n : val[nat] be n + 1 in true

and let n be n + 1 in true