mpri-coq-project/wp.v

156 lines
5.4 KiB
Coq
Raw Normal View History

2017-10-19 15:25:03 +02:00
(* Projet Coq - WP - MPRI 2.7.1 *)
(***** Partie 1 : definition de While ****************************************)
Require Import ZArith.BinInt.
Import Z.
Definition Var := nat.
2017-10-19 15:25:03 +02:00
Definition Mem := Var -> Z.
Definition Expr:= Mem -> Z.
Inductive Instr : Type :=
| skip: Instr
| abort: Instr
| assign: Var -> Expr -> Instr
| seq: Instr -> Instr -> Instr
| ifelse: Expr -> Instr -> Instr -> Instr
| while: Expr -> Instr -> Instr.
Definition ifonly (exp: Expr) (inst: Instr) : Instr :=
ifelse exp inst skip.
(***** CPO *******************************************************************)
Fixpoint nat_eq x y :=
match x, y with
| 0, 0 => true
| 0, S _ => false
| S _, 0 => false
| S x0, S y0 => nat_eq x0 y0
end.
Definition Sequence (S: Type) := nat -> S.
Inductive cpo (T: Type): Type :=
| CpoError: (cpo T)
| CpoElem: T -> (cpo T).
Definition cpo_leq: forall (T: Type), cpo T -> cpo T -> Prop :=
fun T x y => match x, y with
| CpoError _, _ => True
| CpoElem _ x0, CpoElem _ y0 => x0 = y0
| _, _ => False
end.
Arguments cpo_leq {T} _ _.
Infix "cpo<=" := cpo_leq (at level 100).
Definition is_chain: forall (T: Type), Sequence (cpo T) -> Prop :=
fun T chain => forall (n: nat), (chain n) cpo<= (chain (S n)).
Arguments is_chain {T} _.
Definition is_lub_of: forall (T: Type), Sequence (cpo T) -> cpo T -> Prop :=
fun T chain elt => forall (n: nat), (chain n) cpo<= elt.
Arguments is_lub_of {T} _ _.
Axiom find_lub: forall (T: Type), Sequence (cpo T) -> cpo T.
Arguments find_lub {T} _.
Axiom find_lub_correct:
forall (T: Type), forall (chain: Sequence (cpo T)),
is_chain chain -> is_lub_of chain (find_lub chain).
Arguments find_lub_correct {T} {chain} _.
(***** Interpretation ********************************************************)
Definition subst: Mem -> Var -> Z -> Mem :=
fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
if nat_eq v v2 then z else m v2.
2017-11-16 15:22:35 +01:00
Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
Definition MemCpo := cpo Mem.
Definition MemError := CpoError Mem.
Definition MemElem := CpoElem Mem.
Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
match mem with
| CpoError _ => MemError
| CpoElem _ mem0 =>
match inst with
| skip => MemElem mem0
| abort => MemError
2017-11-16 15:22:35 +01:00
| assign v e => (MemElem (mem0 [v <- (e mem0)]))
| seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
2017-11-16 15:22:35 +01:00
| ifelse guard instrIf instrElse =>
if ((guard mem0) =? 0) % Z
then interp instrIf mem
else interp instrElse mem
| while guard body =>
let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
match n with
| 0 => mem
| S m =>
match while_chain (MemElem mem0) m with
| CpoError _ => MemError
| CpoElem _ submem =>
if ((guard submem) =? 0) % Z
then interp body (MemElem submem)
else mem
end
end
in find_lub (fun n =>
match while_chain (MemElem mem0) n with
| CpoError _ => MemError
| CpoElem _ submem =>
if ((guard submem) =? 0) % Z
then MemError
else MemElem submem
end)
end
end.
2017-11-16 15:22:35 +01:00
(***** Validite, prouvabilite pour Hoare *************************************)
Definition Assert := Mem -> Prop.
Delimit Scope assert with assert.
Definition assertTop : Assert := fun _ => True.
Definition assertBot : Assert := fun _ => False.
Definition assertNot : Assert -> Assert :=
fun orig mem => ~ (orig mem).
Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
Definition assertAnd : Assert -> Assert -> Assert :=
fun x1 x2 mem => (x1 mem) /\ (x2 mem).
Infix "/\" := assertAnd : assert.
Definition assertOr : Assert -> Assert -> Assert :=
fun x1 x2 mem => (x1 mem) \/ (x2 mem).
Infix "\/" := assertOr : assert.
Definition assertImpl : Assert -> Assert -> Assert :=
fun x1 x2 => (~x1 \/ x2) % assert.
Infix "->" := assertImpl : assert.
Definition assertForall : Var -> Assert -> Assert :=
fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
Definition existsForall : Var -> Assert -> Assert :=
fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
Notation "'exists' x" := (existsForall x)
(at level 87, no associativity): assert.
Definition assertMemForall : Assert -> Assert :=
fun asser mem => forall (mem: Mem), asser mem.
Notation "'\-/m' x" := (assertMemForall x)
(at level 90, no associativity): assert.
Definition existsMemForall : Assert -> Assert :=
fun asser mem => exists (mem: Mem), asser mem.
Notation "'exists_m' x" := (existsMemForall x)
(at level 87, no associativity): assert.
Definition substAssert : Assert -> Var -> Z -> Assert :=
fun asser ident val mem => asser (mem [ident <- val]).
Notation "a < x <- z >" := (substAssert a x z)
(at level 50, left associativity).
Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
Notation "a < x <- 'expr' z >" := (substAssertExpr a x z)
(at level 50, left associativity).