We axiomatise Hoare Logic in LEGO and thus assign a semantics to the imperative programming language. The LEGO system uses the kind Prop as its logical universe, in fact, Prop is isomorphic to intuitionistic higher-order logic. But we are not only interested in formulae of raw intuitionistic higher-order logic, we also want to talk about the value of variables which depend on a dynamic environment. We therefore use the kind Env->Prop. It is straightforward to lift operations from Prop to Env->Prop e.g, limplies denotes implication. Hoare triples intuitively assert that if the program S is executed in a state such that holds and S terminates, then it will produce a state such that holds.
The most complicated rule deals with the assignment statement
because general updating is not expressible within the type theory, but fortunately, we only have to update values of variables. These are guarded by environments and therefore, updating can be achieved by functional composition.
** Module lib_hoare Imports lib_update lib_ipl $HD : {sort|location->Type}((Env sort)->Prop)->(prog|sort)-> ((Env sort)->Prop)->Prop $Inv : {sort|location->Type}{p:(Env sort)->Prop}HD p (skip|sort) p $Assign : {sort|location->Type}{x:location}{t:(Env sort)->sort x} {p:(Env sort)->Prop} HD (compose p (update|sort x t)) (assign|sort x t) p $Seq : {sort|location->Type}{p,q,r:(Env sort)->Prop}{S1,S2:prog|sort} (HD p S1 r)->(HD r S2 q)->HD p (seq S1 S2) q $Ifthenelse : {sort|location->Type}{p,q:(Env sort)->Prop}{b:(Env sort)->bool} {S1,S2:prog|sort} (HD ([sigma:Env sort]and (p sigma) (is_true (b sigma))) S1 q)-> (HD ([sigma:Env sort]and (p sigma) (is_false (b sigma))) S2 q)-> HD p (ifthenelse b S1 S2) q $While : {sort|location->Type}{p:(Env sort)->Prop}{b:(Env sort)->bool} {S:prog|sort} (HD ([sigma:Env sort]and (p sigma) (is_true (b sigma))) S p)-> HD p (while b S) ([sigma:Env sort]and (p sigma) (is_false (b sigma))) $Con : {sort|location->Type}{p,p1,q,q1:(Env sort)->Prop}{S:prog|sort} (limplies p p1)->(limplies q1 q)->(HD p1 S q1)->HD p S q $HD_elim : {sort|location->Type} {C_HD:((Env sort)->Prop)->(prog|sort)->((Env sort)->Prop)->Prop} ({p:(Env sort)->Prop}C_HD p (skip|sort) p)-> ({x:location}{t:(Env sort)->sort x}{p:(Env sort)->Prop} C_HD (compose p (update|sort x t)) (assign|sort x t) p)-> ({p,q,r:(Env sort)->Prop}{S1,S2:prog|sort}(C_HD p S1 r)-> (C_HD r S2 q)->C_HD p (seq S1 S2) q)-> ({p,q:(Env sort)->Prop}{b:(Env sort)->bool}{S1,S2:prog|sort} (C_HD ([sigma:Env sort]and (p sigma) (is_true (b sigma))) S1 q)-> (C_HD ([sigma:Env sort]and (p sigma) (is_false (b sigma))) S2 q)-> C_HD p (ifthenelse b S1 S2) q)-> ({p:(Env sort)->Prop}{b:(Env sort)->bool}{S:prog|sort} (C_HD ([sigma:Env sort]and (p sigma) (is_true (b sigma))) S p)-> C_HD p (while b S) ([sigma:Env sort]and (p sigma) (is_false (b sigma))))-> ({p,p1,q,q1:(Env sort)->Prop}{S:prog|sort}(limplies p p1)-> (limplies q1 q)->(C_HD p1 S q1)->C_HD p S q)->{p:(Env sort)->Prop} {S:prog|sort}{q:(Env sort)->Prop}(HD p S q)->C_HD p S q * Conl = ... : {sort|location->Type}{p,p1,q:(Env sort)->Prop}{S:prog|sort} (limplies p p1)->(HD p1 S q)->HD p S q * Conr = ... : {sort|location->Type}{p,q,q1:(Env sort)->Prop}{S:prog|sort} (limplies q1 q)->(HD p S q1)->HD p S q * Inv_lemma = ... : {sort|location->Type}{p,p':(Env sort)->Prop}(limplies p' p)-> HD p' (skip|sort) p * Assign_lemma = ... : {sort|location->Type}{x:location}{t:(Env sort)->sort x} {p,p':(Env sort)->Prop}(limplies p' (compose p (update|sort x t)))-> HD p' (assign|sort x t) p * While_lemma = ... : {sort|location->Type}{p,q:(Env sort)->Prop}{b:(Env sort)->bool} {S:prog|sort} (limplies ([sigma:Env sort]and (p sigma) (is_false (b sigma))) q)-> (HD ([sigma:Env sort]and (p sigma) (is_true (b sigma))) S p)-> HD p (while b S) q