Compare commits
2 commits
d1b62ad2b5
...
93336c705e
Author | SHA1 | Date | |
---|---|---|---|
Théophile Bastian | 93336c705e | ||
Théophile Bastian | 06f655c1c1 |
96
wp.v
96
wp.v
|
@ -157,47 +157,45 @@ Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
|
|||
Definition assertOfExpr : Expr -> Assert :=
|
||||
fun expr mem => expr mem <> 0%Z.
|
||||
|
||||
Definition assertImplLogical : Assert -> Assert -> Prop :=
|
||||
fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
|
||||
Definition assertImplLogical (a1 a2: Assert): Prop :=
|
||||
forall (m: Mem), (a1 m) -> (a2 m).
|
||||
|
||||
|
||||
(***** Hoare provability *****************************************************)
|
||||
|
||||
Parameter hoare_provability : Assert -> Instr -> Assert -> Prop.
|
||||
Notation "|- [| pre |] instr [| post |]" :=
|
||||
(hoare_provability pre instr post) (at level 30): assert.
|
||||
Reserved Notation "|- [| x |] y [| z |]" (at level 30).
|
||||
|
||||
Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
|
||||
Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
|
||||
(|- [|a1|] abort [|a2|]) % assert.
|
||||
Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
|
||||
(|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
|
||||
Axiom h_conseq:
|
||||
forall (a1: Assert), forall (a1': Assert),
|
||||
forall (a2: Assert), forall (a2': Assert),
|
||||
forall (s: Instr),
|
||||
(|- [| a1' |] s [| a2' |]) % assert ->
|
||||
(assertImplLogical a1 a1') ->
|
||||
(assertImplLogical a2' a2) ->
|
||||
(|- [| a1 |] s [| a2 |]) % assert.
|
||||
Axiom h_seq:
|
||||
forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
|
||||
forall (s1: Instr), forall (s2: Instr),
|
||||
(|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
|
||||
(|- [|a1|] (seq s1 s2) [|a3|]) % assert.
|
||||
Axiom h_if:
|
||||
forall (a1: Assert), forall (a2: Assert),
|
||||
forall (e: Expr),
|
||||
forall (s1: Instr), forall (s2: Instr),
|
||||
(|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
|
||||
(|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
|
||||
(|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
|
||||
Axiom h_while:
|
||||
forall (inv: Assert),
|
||||
forall (e: Expr),
|
||||
forall (s: Instr),
|
||||
(|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
|
||||
(|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
|
||||
Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
|
||||
| H_skip: forall pre, hoare_provability pre skip pre
|
||||
| H_abort: forall pre, forall post, hoare_provability pre abort post
|
||||
| H_assign: forall post, forall (x: Var), forall (e: Expr),
|
||||
(|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
|
||||
| H_conseq:
|
||||
forall pre, forall post,
|
||||
forall pre', forall post',
|
||||
forall s,
|
||||
|
||||
(|- [| pre' |] s [| post' |]) % assert ->
|
||||
(assertImplLogical pre pre') ->
|
||||
(assertImplLogical post' post) ->
|
||||
(|- [| pre |] s [| post |]) % assert
|
||||
| H_seq:
|
||||
forall pre, forall mid, forall post, forall s1, forall s2,
|
||||
(|- [|pre|] s1 [|mid|]) % assert ->
|
||||
(|- [|mid|] s2 [|post|]) % assert ->
|
||||
(|- [|pre|] (seq s1 s2) [|post|]) % assert
|
||||
| H_if:
|
||||
forall pre, forall post, forall expr, forall sIf, forall sElse,
|
||||
(|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
|
||||
(|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
|
||||
(|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
|
||||
| H_while:
|
||||
forall inv, forall expr, forall sBody,
|
||||
(|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
|
||||
(|- [| inv |] (while expr sBody)
|
||||
[| inv /\ ~ (assertOfExpr expr) |]) % assert
|
||||
where "|- [| pre |] instr [| post |]" :=
|
||||
(hoare_provability pre instr post) : assert.
|
||||
|
||||
(***** Hoare: provability implies consequence ********************************)
|
||||
|
||||
|
@ -214,10 +212,32 @@ Definition hoare_consequence (pre: Assert) (instr: Instr) (post: Assert) :=
|
|||
Notation "|= [| pre |] instr [| post |]" :=
|
||||
(hoare_consequence pre instr post) (at level 30): assert.
|
||||
|
||||
Lemma weaken_in_conseq:
|
||||
forall a1, forall a2, forall m,
|
||||
assertImplLogical a1 a2 -> conseq_or_bottom a1 m ->
|
||||
conseq_or_bottom a2 m.
|
||||
Proof.
|
||||
intros a1 a2 m impl conseq. destruct m.
|
||||
- apply conseq.
|
||||
- simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
|
||||
Qed.
|
||||
|
||||
|
||||
Theorem hoare_provability_implies_consequence :
|
||||
forall (pre: Assert), forall (s: Instr), forall (post: Assert),
|
||||
( |- [| pre |] s [| post |] ) % assert
|
||||
-> ( |= [| pre |] s [| post |] ) % assert.
|
||||
Proof.
|
||||
(* TODO *)
|
||||
Admitted.
|
||||
intros pre instr post. intros deduction.
|
||||
induction deduction; intros mem preInMem; simpl.
|
||||
- exact preInMem.
|
||||
- trivial.
|
||||
- exact preInMem.
|
||||
- apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
|
||||
apply IHdeduction. apply H. exact preInMem.
|
||||
- destruct (interp s1 (MemElem mem)) eqn:mRel.
|
||||
admit.
|
||||
apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
|
||||
specialize IHdeduction1 with mem as IH1_mem.
|
||||
rewrite mRel in IH1_mem. apply IH1_mem. assumption.
|
||||
-
|
||||
|
|
Loading…
Reference in a new issue