pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

HoareLogic: yet another way to prove an invariant of a transition system

Browse source
This commit is contained in:
Adam Chlipala 2016-03-27 15:33:27 -04:00
parent c8e3a3fdcd
commit a180698487
1 changed files with 185 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

187
HoareLogic.v
View file

@ -119,6 +119,9 @@ Inductive hoare_triple : assertion -> cmd -> assertion -> Prop :=
(forall h v, P h v -> I h v)
-> hoare_triple (fun h v => I h v /\ beval b h v = true) c I
-> hoare_triple P (While_ I b c) (fun h v => I h v /\ beval b h v = false)
| HtAssert : forall P I : assertion,
(forall h v, P h v -> I h v)
-> hoare_triple P (Assert I) P
| HtConsequence : forall (P Q P' Q' : assertion) c,
hoare_triple P c Q
-> (forall h v, P' h v -> P h v)
@ -172,6 +175,7 @@ Infix "<-" := set (no associativity, at level 70) : cmd_scope.
Infix ";;" := Seq (right associativity, at level 75) : cmd_scope.
Notation "'when' b 'then' then_ 'else' else_ 'done'" := (If_ b then_ else_) (at level 75, e at level 0).
Notation "{{ I }} 'while' b 'loop' body 'done'" := (While_ I b body) (at level 75).
Notation "'assert' {{ I }}" := (Assert I) (at level 75).
Delimit Scope cmd_scope with cmd.
Infix "+" := plus : reset_scope.
@ -196,7 +200,7 @@ Notation "{{ P }} c {{ Q }}" := (hoare_triple P c%cmd Q) (at level 90, c at next
(** ** Swapping the values in two variables *)
Ltac ht1 := apply HtSkip || apply HtAssign || apply HtWrite || eapply HtSeq
|| eapply HtIf || eapply HtWhile
|| eapply HtIf || eapply HtWhile || eapply HtAssert
|| match goal with
| [ |- hoare_triple ?pre _ _ ] => eapply HtConsequence with (P := pre); [ | tauto | ]
end.
@ -209,7 +213,7 @@ Ltac ht := simplify; repeat ht1; cbv beta; propositional; subst;
repeat match goal with
| [ _ : context[?a <=? ?b] |- _ ] => destruct (a <=? b); try discriminate
| [ H : ?E = ?E |- _ ] => clear H
end; simplify; propositional; auto; try linear_arithmetic.
end; simplify; propositional; auto; try equality; try linear_arithmetic.
Theorem swap_ok : forall a b,
{{_&v ~> v $! "x" = a /\ v $! "y" = b}}
@ -339,3 +343,182 @@ Proof.
cases (k ==n x $! "j"); ht.
Qed.
(** * An alternative correctness theorem for Hoare logic, with small-step semantics *)
Inductive step : heap * valuation * cmd -> heap * valuation * cmd -> Prop :=
| StAssign : forall h v x e,
step (h, v, Assign x e) (h, v $+ (x, eval e h v), Skip)
| StWrite : forall h v e1 e2,
step (h, v, Write e1 e2) (h $+ (eval e1 h v, eval e2 h v), v, Skip)
| StStepSkip : forall h v c,
step (h, v, Seq Skip c) (h, v, c)
| StStepRec : forall h1 v1 c1 h2 v2 c1' c2,
step (h1, v1, c1) (h2, v2, c1')
-> step (h1, v1, Seq c1 c2) (h2, v2, Seq c1' c2)
| StIfTrue : forall h v b c1 c2,
beval b h v = true
-> step (h, v, If_ b c1 c2) (h, v, c1)
| StIfFalse : forall h v b c1 c2,
beval b h v = false
-> step (h, v, If_ b c1 c2) (h, v, c2)
| StWhileFalse : forall I h v b c,
beval b h v = false
-> step (h, v, While_ I b c) (h, v, Skip)
| StWhileTrue : forall I h v b c,
beval b h v = true
-> step (h, v, While_ I b c) (h, v, Seq c (While_ I b c))
| StAssert : forall h v (a : assertion),
a h v
-> step (h, v, Assert a) (h, v, Skip).
Hint Constructors step.
Definition trsys_of (st : heap * valuation * cmd) := {|
Initial := {st};
Step := step
|}.
Definition unstuck (st : heap * valuation * cmd) :=
snd st = Skip
\/ exists st', step st st'.
Lemma hoare_triple_unstuck : forall P c Q,
{{P}} c {{Q}}
-> forall h v, P h v
-> unstuck (h, v, c).
Proof.
induct 1; unfold unstuck; simplify; propositional; eauto.
apply IHhoare_triple1 in H1.
unfold unstuck in H1; simplify; first_order; subst; eauto.
cases x.
cases p.
eauto.
cases (beval b h v); eauto.
cases (beval b h v); eauto.
apply H0 in H2.
apply IHhoare_triple in H2.
unfold unstuck in H2; simplify; first_order.
Qed.
Lemma hoare_triple_Skip : forall P Q,
{{P}} Skip {{Q}}
-> forall h v, P h v -> Q h v.
Proof.
induct 1; auto.
Qed.
Lemma hoare_triple_step : forall P c Q,
{{P}} c {{Q}}
-> forall h v h' v' c',
step (h, v, c) (h', v', c')
-> P h v
-> {{h''&v'' ~> h'' = h' /\ v'' = v'}} c' {{Q}}.
Proof.
induct 1.
invert 1.
invert 1; ht; eauto.
invert 1; ht; eauto.
invert 1; simplify.
eapply HtConsequence; eauto.
propositional; subst.
eapply hoare_triple_Skip; eauto.
econstructor; eauto.
invert 1; simplify.
eapply HtConsequence; eauto; equality.
eapply HtConsequence; eauto; equality.
invert 1; simplify.
eapply HtConsequence with (P := h'' & v'' ~> h'' = h' /\ v'' = v').
apply HtSkip.
auto.
simplify; propositional; subst; eauto.
econstructor.
eapply HtConsequence; eauto.
simplify; propositional; subst; eauto.
econstructor; eauto.
invert 1; simplify.
eapply HtConsequence; eauto.
econstructor.
simplify; propositional; subst; eauto.
simplify.
eapply HtConsequence.
eapply IHhoare_triple; eauto.
simplify; propositional; subst; eauto.
auto.
Qed.
Theorem hoare_triple_invariant : forall P c Q h v,
{{P}} c {{Q}}
-> P h v
-> invariantFor (trsys_of (h, v, c)) unstuck.
Proof.
simplify.
apply invariant_weaken with (invariant1 := fun st => {{h&v ~> h = fst (fst st)
/\ v = snd (fst st)}}
snd st
{{_&_ ~> True}}).
apply invariant_induction; simplify.
propositional; subst; simplify.
eapply HtConsequence; eauto.
equality.
cases s.
cases s'.
cases p.
cases p0.
simplify.
eapply hoare_triple_step; eauto.
simplify; auto.
simplify.
cases s.
cases p.
simplify.
eapply hoare_triple_unstuck; eauto.
simplify; auto.
Qed.
(* A very simple example, just to show all this in action. *)
Definition forever := (
"i" <- 1;;
"n" <- 1;;
{{h&v ~> v $! "i" > 0}}
while 0 < "i" loop
"i" <- "i" * 2;;
"n" <- "n" + "i";;
assert {{h&v ~> v $! "n" >= 1}}
done;;
assert {{_&_ ~> False}}
(* Note that this last assertion implies that the program never terminates! *)
)%cmd.
Theorem forever_ok : {{_&_ ~> True}} forever {{_&_ ~> False}}.
Proof.
ht.
Qed.
Theorem forever_invariant : invariantFor (trsys_of ($0, $0, forever)) unstuck.
Proof.
eapply hoare_triple_invariant.
apply forever_ok.
simplify; trivial.
Qed.