CIS 500 — Software FoundationsFinal ExamMay 9, 2011Name or WPE-I number:Scores:123456789Total (120 max)Hoare Logic1. (7 points) What does it mean to say that the Hoare triple {{P}} c {{Q}} is valid?12. (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.23. (12 points) In the Imp program below, we have provided a precondition and postcondition.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 }3STLC4. (16 points) Recall the definition of the substitution operation in the simply typed lamb da-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).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’)4References5. (12 points) The next few problems concern the STLC extended with natural numbers andreferences (reproduced on page 15, 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?(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?(c) Is there a type T that makesx:T; [] |- !(!(!x)) : Natprovable? If so, what is it?(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?56. (8 points) Briefly explain the term aliasing. Give one reason why it is a good thing and onereason why it is bad.67. (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 needed here.7(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 each lemma to each proofcase that uses it.store weakeningstore well typed snocassign pres store typingsubstitution preserves typingT AbsT AppT RefT DerefT Assign8(c) Here is the beginning of the T Ref case of the proof. Complete the case.Theorem (Preservation): If empty; ST |- t : T with ST |- st, and t in store st takes astep to t’ in store st’, then there exists some store typing ST’ that extends ST and for whichempty; ST’ |- t’ : T and ST’ |- st’.Proof: By induction on the given derivation of empty; ST |- t : T.• ...cases for other rules...• If the last rule in the derivation is T_Ref, then t = ref t1 for some t1 and, moreover,empty; ST |- t1 : T1 for some T1, with T = Ref T1.Fill in rest of case:9Subtyping8. (8 points) Recall the simply-typed lambda calculus extended with products and subtyping(reproduced on page 17).The subtyping rule for productsS1 <: T1 S2 <: T2-------------------- (S_Prod)S1*S2 <: T1*T2intuitively corresponds to the “depth” subtyping rule for records. Extending the analogy, we mightconsider adding a “permutation” rule-------------- (S_ProdP)T1*T2 <: T2*T1for products.Is this a good idea? Briefly explain why or why not.109. (15 points) The preservation and progress theorems about the STLC with subtyping (page 17)depend on a number of technical lemmas, including the following one, which describes the possible“shapes” of types that are subtypes of an arrow type:Lemma: For all types U, V1, and V2, if U <: V1 -> V2, then thereexist types U1 and U2 such that(a) U = U1 -> U2,(b) V1 <: U1, and(c) U2 <: V2.The following purported proof of this lemma contains two significant mistakes. Explain whatis wrong and how the proof should be corrected.Proof : By induction on a derivation of U <: V1 -> V2.• The last rule in the derivation cannot be S Prod or S Top since V1 -> V2 is not a producttype or Top.• If the last rule in the derivation is S Arrow, all the desired facts follow directly from theform of the rule.• Suppose the last rule in the derivation is S Trans. Then, from the form of the rule, thereis some type U’ with U <: U’ and U’ <: V1 -> V2. We must show that U’ = U1’ -> U2’,with V1 <: U1’ and U2’ <: V2; this follows from the induction