Language Semantics and Verification

The general problem is to give a denotational and operational semantics for a simple first-order programming language, to show the two semantics are equivalent, to prove some general laws of program equivalence based on the semantics, and to carry out program verification based on the semantics. The answers need not be detailed formal proofs, but they should present the key ideas and steps in a clear and concise manner and convince the examiner that details could if asked for.

The language is defined as follows. Assume given a set Var of variables Cst of constants and families of n-ary operation symbols P_{n} (primitive), F_{n} (user defined). Assume Cst contains at the element nil. expressions: The set of expressions is the least set (of abstract syntax trees) Exp satisfying

Exp = Var + Cst + let{Var ← Exp}Exp + if(Exp, Exp, Exp) + ⋃_{n∈Nat} O_{n}(Exp^{n})

where O_{n} = P_{n} ∪ F_{n}.

definitions: The set of definitions Dfn is defined by

Dfn = (F_{n}(Var^{n}) ← Exp)^{∗}

Thus Dfn is the set of systems of defining equations.

cst, cst_{0}, … range over Cst, exp, exp_{0}, … range over Exp, f, g, f_{0}, … range over F, p, … range over P, and dfn, dfn′ range over Dfn. Free and bound variables of expressions are defined as usual with let{x ← exp_{0}}exp_{1} binding x in exp_{1}.

Problem (1): A definition dfn is well-formed if each function symbol is defined at most once, for each f(x_{1}, …, x_{n}) ← exp in dfn the x_{i} are distinct variables, the free variables of exp are among x_{1}, …, x_{n}, and the definable function symbols of exp are among the symbols defined in dfn. Define (ala Plotkin) the static semantics of definitions that characterizes the set of well-formed definitions.

A program is a pair (exp, dfn) such that dfn is well-formed, exp contains no free variables, and the definable function symbols occuring in exp are defined in dfn.

To define the semantics we assume given a function Peval : P_{n} × Cst^{n} ⟶^{eval} Cst defining an interpretation of the primitive operations. [Assume for simplicity that Peval is total.] The semantics of programs is the obvious call-by-value semantics. if takes the false branch if the the test evaluates to nil and the true branch otherwise. Application of a defined function is evaluation of the body with formal parameters replaced by values of the arguments.

Problem (2): Give a standard denotational semantics for the language—i.e. define a partial function Eval from programs (exp, dfn) to constants.

Problem (3): Give an operational semantics for the language. Take configurations to be programs (exp, dfn) and define a transition relation ↦ on such configurations. Note that terminal configurations are those of the form (cst, dfn) and that the definition component does not change.

Problem (4): Prove that the behavior induced by the operational semantics is a (partial) function and that it agrees with the denotational semantics. I.e. let ↦^{∗} be the transitive, reflexive closure of ↦ and prove • (exp, dfn) ↦^{∗} (cst, dfn) and (exp, dfn) ↦^{∗} (cst′, dfn) implies cst = cst′.

• (exp, dfn) ↦^{∗} (cst, dfn) iff Eval(exp, dfn) = cst.

A substitution σ is finite map from variables to constants. Substitutions lift homomorphically to expressions (mapping variables not in the domain to themselves, and taking care to rename bound variables so as not to be in the domain of the substitution). A context C is an expression with a hole. C[exp] is the result of filling the hole by exp – possibly trapping free variables in exp. We write Eval(exp_{0}, dfn_{0}) ∼ Eval(exp_{1}, dfn_{1}) to mean that both sides are undefined or both evaluate to the same constant.

expression equivalence: Expression equivalence is defined by exp_{0} ∼ exp_{1} iff Eval(σ(exp_{0}), dfn) ∼ Eval(σ(exp_{1}), dfn) for all definitions dfn and substitutions σ such that (σ(exp_{1}), dfn) is a program.

Problem (5): Prove the following

• let{x ← e_{0}}f(…, x, …) ∼ f(…, e_{0}, …)

• ∼ is a congruence on expressions: if exp_{0} ∼ exp_{1} and C is a context then C[exp_{0}] ∼ C[exp_{1}]

[Clarification – the explicit occurrence of x in the argument list is intended as the unique occurrence of x in the let-body.]

zero-order and tail-recursive: An expression is zero-order if it contains no occurrences of definable function symbols. Let Exp_{z} denote the set of zero-order expressions. The set of tail-recursive expressions is the least subset Exp_{t} of Exp satisfying

Exp_{t} = Exp_{z} + let{Var ← Exp_{z}}Exp_{t} + if(Exp_{z}, Exp_{t}, Exp_{t}) + ⋃_{n∈Nat} F_{n}(Exp_{z}^{n})

A definition is tail-recursive if the bodies of each equation is tail-recursive.

Problem (6): Formulate an anolog of the method of invariant assertions (cf. Manna lectures) for proving partial correctness assertions about tail-recursive function descriptions – pairs f : dfn such that f is defined in dfn and dfn is tail-recursive. Prove the method is a sound inference rule.

For the final problem assume that the constants are the closure of the set of natural numbers and nil under pairing, and that there are the usual Lisp operations of car, cdr, cons, null, .. Let dfn be the following definition.

rev(x)  ← reva(x, nil)
reva(x, y) ← if(null(x), y, reva(cdr(x), cons(car(x), y)))
r(x)  ← if(or(null(x), null(cdr(x))),

x,

cons(car(r(cdr(x))), r(cons(car(x), r(cdr(r(cdr(x))))))))

f(x)  ← f(x)

where or is the usual abbreviation using if. Assume that we are working in a first-order theory of this pairing structure, that we have suitable definitions of Lists (with List induction) and of the reverse operation on Lists.

Problem (7): • Prove that f(x) does not terminate for any x.

• Give invariant assertions to prove that rev reverses lists (when defined).

• Prove that r is defined for all Lists and computes the reverse function.