Semantics of Programming Languages Comprehensive Exam

January, 1999

Instructions

Answer all parts of all questions; you have four hours.

To maximize partial credit for an incomplete proof, you should:

• provide as much of the proof as you can;

• describe what remains to be proven and how that (when combined with what you have proven) would complete the proof;

• indicate (where possible) how you suspect that the missing piece could be proven.

The last two pages of this exam include a summary of relevant terminology and partialcorrectness inference rules.

Questions

1a) Is the following equivalence valid?

(for N do N := N+1) ≡ diverge

If the equivalence is valid, prove it. If it is invalid, give a couner-example and explain why your counter-example shows the equivalence is invalid.

1b) Is the following equivalence valid?

(if B then C_{1} else C_{2}); C_{3} ≡ if B then (C_{1};C_{3}) else (C_{2};C_{3})

If the equivalence is valid, prove it. If it is invalid, give a couner-example and explain why your counter-example shows the equivalence is invalid.

2) Let D be a domain with partial order relation ⊑. Definition: Let f : D ⟶ D and let d ∈ D. f is increasing at d if d ⊑ f(d). An element e of D is the least fixed point of f above d if

• d ⊑ e,

• f(e) = e,

• for all e′ such that d ⊑ e′: f(e′) = e′ implies e ⊑ e′.

Denote the least fixed point of f above d, if it exists, by fix_{d}(f).

Proposition: If f : D ⟶ D is continuous, and increasing at d, then fix_{d}(f) exists and

fix_{d}(f) = ⨆_{i=0}^{∞} f^{i}(d) .

Part a) Prove the proposition.

Part b) Let f, g : D ⟶ D be continuous functions on D that are both increasing at d. Prove that all of the fixed points in the following equation exist, and that the equation holds:

g(fix_{d}(f ∘ g)) = fix_{d}(g ∘ f) .

3) Give a formal proof in Floyd-Hoare logic (see attachment) that the following command is partially correct with respect to the indicated pre- and post-conditions.

{A ≥ 0} X := 0; Y := A; while X < Y do

(Y := Y - 1; X := X + 1); {Y = A div 2}

4) Let D_{⊥} = {a, b, ⊥} be a domain with bottom element ⊥. Thus, ⊥ ⊑ a and ⊥ ⊑ b. Suppose that a and b are incomparable in the partial order ⊑. Let S = {x, y}. S is just a set without any ordering.

Part a) List the elements in the set of functions S ⟶ D_{⊥} and describe the ordering among them in the “pointwise” ordering that is determined by ⊑. Note that each element that you must list is a function, and that a function can be described by listing the ordered pairs in its graph.

Part b) Now let D and E be domains with bottom elements. A function f : D ⟶ E is strict if f(⊥_{D}) = ⊥_{E}. Suppose D has exactly 1000 elements and E has exactly 50 elements. How many functions in the set of functions D ⟶ E (the set of all functions from D to E) are strict?

Terminology

A domain (technically, an ω-complete partial order) is a pair (D, ⊑) such that: • ⊑ is a partial order

• D has a least element ⊥_{D}

• Every chain x_{0} ⊑ x_{1} ⊑ ⋯ ⊑ x_{n} ⊑ ⋯ in D has a supremum (least upper bound). A function f : D → E between domains (D, ⊑_{D}) and (E, ⊑_{E}) is continuous if, for all

chains in D,

f( ⨆_{n=0}^{∞} x_{n}) = ⨆_{n=0}^{∞} f(x_{n}).

A fixed point of a function f : D → D is an element x ∈ D such that f(x) = x. A least fixed point of f is a fixed point x such that, for all other fixed points y, x ⊑ y.

The least fixed point of a continuous function f, denoted fix(f ), can be calculated by

fix(f) = ⨆_{n=0}^{∞} f^{n}(⊥).

Axioms and Rules of Inference for Floyd-Hoare Logic

These axioms are taken directly from Tennent’s Semantics of Programming Languages.

Command-specific axioms and rules of inference

{P }skip{P } {true}diverge{false} {[P](ι ↦ E)}ι := E{P } {P }C {Q} ⟹{P }(C ){Q} {P }C_{0} {Q} & {Q}C_{1} {R} ⟹{P }C_{0} ; C_{1} {R} {P and B}C_{0} {Q} & {P and not B}C_{1} {Q} ⟹{P }if B then C_{0} elseC_{1} {Q} {P and B}C {P } ⟹{P }while B do C {P and not B}

Other axioms and rules of inference

Pre-condition Strengthening: P_{0} ⊃ P_{1} & {P_{1}}C {Q} ⟹{P_{0}}C {Q} Post-condition Weakening: Q_{0} ⊃ Q_{1} & {P }C {Q_{0}} ⟹{P }C {Q_{1}} Pre-condition Disjunction: {P_{1}}C {Q} & ⋯ & {P_{n}}C {Q} ⟹{P_{1} or ⋯ or P_{n}}C {Q} Post-condition Conjunction: {P }C {Q_{1}} & ⋯ & {P }C {Q_{n}} ⟹{P }C {Q_{1} and ⋯ and Q_{n}}

Semantics of some commands

[[(X)]] = [[X]] .

[[ if B then X_{0} else X_{1} ]]s = \{ \begin{matrix}[[X_{0}]]s & if [[B]] = true \\ [[X_{1}]]s & if [[B]] = false \end{matrix}

[[true]]s = true

[[not B]]s = \{ \begin{matrix}false & if [[B]]s = true \\ true & if [[B]]s = false \end{matrix}

[[B_{0} and B_{1}]]s = ([[B_{0}]]s and [[B_{1}]]s) [[N_{0} < N_{1}]]s = ([[N_{0}]]s < [[N_{1}]]s) [[E_{0} = E_{1}]]s = ([[E_{0}]]s < [[E_{1}]]s) [[0]]s = 0 [[succ N]]s = ([[N]]s) + 1 [[skip]]s = s [[C_{0}; C_{1}]]s = [[C_{1}]]([[C_{0}]]s) [[ for N do C]]s = [[C]]^{[[N]]s}(s) [[diverse]]s is undefined, for all states s.