From a18069848708a57f48861b1d239c387e2d46877b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 27 Mar 2016 15:33:27 -0400 Subject: [PATCH] HoareLogic: yet another way to prove an invariant of a transition system --- HoareLogic.v | 187 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 185 insertions(+), 2 deletions(-) diff --git a/HoareLogic.v b/HoareLogic.v index 9a017ec..7d02e4e 100644 --- a/HoareLogic.v +++ b/HoareLogic.v @@ -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.