CIS 500 — Software FoundationsFinal ExamMay 9, 2011Answer keyHoare Logic1. (7 points) What does it mean to say that the Hoare triple {{P}} c {{Q}} is valid?Answer: {{P}} c {{Q}} means that, for any states st and st’, if st satisfies P and c / st ⇓st’, then st’ satisfies Q.2. (18 points) Recall the Hoare rule for reasoning about sequences of commands:{{P}} c1 {{Q}} {{Q}} c2 {{R}}{{P}} c1;c2 {{R}}Hoare SeqFormally, this rule corresponds to a theorem:Theorem hoare_seq : forall P Q R c1 c2,{{P}} c1 {{Q}} ->{{Q}} c2 {{R}} ->{{P}} c1;c2 {{R}}.Give a careful informal proof (in English) of this theorem.Answer: To show that the Hoare triple {{P}} c1;c2 {{R}} is valid, we must show that, for anystates st and st’’, if st satisfies P and c1;c2 / st ⇓ st’’, then st’’ satisfies R. So suppose stsatisfies P and c1;c2 / st ⇓ st’.By the definition of the evaluation relation, there must be some state st’ such that c1 / st ⇓st’ and c2 / st’ ⇓ st’’. Since {{P}} c1 {{Q}} is a valid triple, we know that st’ satisfies Q.But then, since {{Q}} c2 {{R}} is a valid triple, we know that st’’ satisfies R, as required.3. (12 points) In the Imp program below, we have provided a precondition and p ostc ondition.In the blank before the loop, fill in an invariant that would allow us to annotate the rest of theprogram.{ True }X := nY := XZ := 0{ _____________________________________________ }WHILE Y <> 0 DOZ := Z + X;Y := Y - 1END{ Z = n*n }Answer: Z + Y*n = n*n ∧ X = nGrading scheme: Common mistakes included• Using subtraction to state the invariant without including an assertion about the relative sizesof the things being subtracted (-2 points)• Omitting X = n from the invariant (-3 points)Otherwise, 4 points each for:• invariant holds before the loop• invariant is preserved by the loop• invariant and negation of loop test implies final assertion1STLC4. (16 points) Recall the definition of the substitution operation in the simply typed lambda-calculus (with no extensions, and omitting base types such as booleans for brevity):Fixpoint subst (s:tm) (x:id) (t:tm) : tm :=match t with| tm_app t1 t2 => tm_app (subst s x t1) (subst s x t2)| tm_var x’ => if beq_id x x’ then s else t| tm_abs x’ T t1 => tm_abs x’ T (if beq_id x x’ then t1 else (subst s x t1))end.This definition uses Coq’s Fixpoint facility to define substitution as a function. Suppose, instead,we wanted to define substitution as an inductive relation substi. We’ve begun the definition byproviding the Inductive header and one of the constructors; your job is to fill in the rest of theconstructors. (Your answer should be such that subst s x t = t’ <-> substi s x t t’, for alls, x, t, and t’, but you do not need to prove it).Answer:Inductive substi (s:tm) (x:id) : tm -> tm -> Prop :=| s_app : forall t1 t2 t1’ t2’,substi s x t1 t1’ ->substi s x t2 t2’ ->substi s x (tm_app t1 t2) (tm_app t1’ t2’)| s_var1 :substi s x (tm_var x) s| s_var2 : forall x’,beq_id x x’ = false ->substi s x (tm_var x’) (tm_var x’)| s_abs1 : forall T t1,substi s x (tm_abs x T t1) (tm_abs x T t1)| s_abs2 : forall x’ T t1 t1’,beq_id x x’ = false ->substi s x t1 t1’ ->substi s x (tm_abs x’ T t1) (tm_abs x’ T t1’).2References5. (12 points) The next few problems concern the STLC extended with natural numbers andreferences (reproduced on page 13, with the same informal notations as we’re using here).(a) In this system, is there a type T that makesx:T; [] |- (\x:Nat. 2 * x) (x x) : Natprovable? If so, what is it?Answer: No.(b) Is there a type T that makesempty; [] |- (\x:Ref Nat. ((\_:Unit. !x), (\y:Nat. x := y))) (ref 0) : Tprovable? If so, what is it?Answer: (Unit->Nat)*(Nat->Unit)(c) Is there a type T that makesx:T; [] |- !(!(!x)) : Natprovable? If so, what is it?Answer: Ref (Ref (Ref Nat))(d) Is there a type T that makesx:T; [] |- (\y:Nat*Nat. pred (y.fst)) (x.snd x.fst) : Natprovable? If so, what is it?Answer: S * (S -> Nat*Nat), for any type S.36. (8 points) Briefly explain the term aliasing. Give one reason why it is a good thing and onereason why it is bad.Answer: Aliasing can happen in any language with a pointers and a heap. It occurs when twodifferent variables both refer to the same heap cell — or, more generally, when a single heap cell isaccessible to a program via multiple “paths” of pointers. It is both a good thing and a bad thing:good, because it is the basis of shared state and so fundamental to mainstream OO programming;but also bad, because it makes reasoning about programs more difficult. For example, executing theassignments x := 5; y := 6 leaves x set to 5 unless x and y are aliases for the same cell.47. (24 points) Recall the preservation theorem for the STLC with references. In formal Coqnotation it looks like this:Theorem preservation : forall ST t t’ T st st’,has_type empty ST t T ->store_well_typed empty ST st ->t / st ==> t’ / st’ ->exists ST’,(extends ST’ ST /\has_type empty ST’ t’ T /\store_well_typed empty ST’ st’).Informally, it looks like this:Theorem (Preservation): If empty; ST |- t : T with ST |- st, and t in store sttakes a step to t’ in store st’, then there exists some store typing ST’ that extends STand for which empty; ST’ |- t’ : T and ST’ |- st’.(a) Briefly explain why the extra (compared to preservation for the pure STLC) refinement“exists ST’...” is nee ded here.Answer: Because reducing a term of the form ref v allocates a new location l and yields las the result of reduction, but l is not in the domain of ST and hence no t typable under ST.5(b) The proof of this theorem relies on some subsidiary lemmas:Lemma store_weakening : forall Gamma ST ST’ t T,extends ST’ ST ->has_type Gamma ST t T ->has_type Gamma ST’ t T.Lemma store_well_typed_snoc : forall ST st t1 T1,store_well_typed ST st ->has_type empty ST t1 T1 ->store_well_typed (snoc ST T1) (snoc st t1).Lemma assign_pres_store_typing : forall ST st l t,l < length st ->store_well_typed ST st ->has_type empty ST t (store_ty_lookup l ST) ->store_well_typed ST (replace l t st).Lemma substitution_preserves_typing : forall Gamma ST x s S t T,has_type empty ST s S ->has_type (extend Gamma x S) ST t T ->has_type Gamma ST (subst x s t) T.Suppose we carry out a proof of preservation by induction on the given typing derivation. Inwhich cases of the proof are the above lemmas used?Match names of lemmas to proof cases by drawing a line from from