Programming Language Comprehensive, August 21, 1997

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

Question 1: Give a formal proof (or natural deduction style proof-tree) that the following specification is partially correct:

{true} N := 14518 ; while N > 0 do N := N - 17 {N = 0 } .

Note that 14518 = 17 ∗ 854.

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 the local definition block from Tennent’s simple applicative language. What is the extensionality rule of inference? Argue that it is sound. (For less credit, discuss the soundness of the rule of inference for while coommands in the simple imperative language.)

Question 3:

a) Formulate an intuitively correct definition of

[[ ∃ Y(B) ]]σ

where B is a boolean expression. (‘∃ Y’ means ‘there exists Y’.)

b) Recall the form of the assignment axioms:

{[B](X ↦ E)} X := E {B} .

These axioms have a “backward” direction to them. In contrast, here is a form of “forward” axiom for assignment statements:

{B} X := E {∃ Y ([B](X ↦ Y) and X = [E](X ↦ Y)}

where Y is a variable that does not occur in B and does not occur in E. Assume that B is a boolean expression and show that this axiom is valid. Hint: The ‘Y’ in the post condition is the “old” value of X, i.e. the value of ‘X’ before X := E is executed.

Question 4: Calculate and simplify as much as you can by following the computational steps of a plausible interpreter for the simple imperative language:

[[ letrec h : val[nat] → val[nat] be λ n:val[nat].if n = 0 then 1 else g(h(n-1)) in h(2)]] u

Show all steps.

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:

a) Define domain. If you have in my mind a particular book or paper for this definition, tell which one.

b) A directed set is a nonempty subset A of a partially ordered set D with the property that every two elements in A have an upper bound in A. A partially ordered set D is complete if every directed subset of D has a least upper bound in D. Denote the least upper bound of a set A by ⨆ A. We call a partially ordered set which is complete a dcpo. (This stands for directed-complete partial order.) Let D and E be dcpo’s. A function f : D ⟶ E is a compact iff {f(a) | a ∈ A} is directed and f(⨆ A) ⊑ ⨆{f(a) | a ∈ A} for all directed subsets of D. Give an example of a function which is compact, but not monotone. You must specify f, D and E.