Commit 5dc73a2e by MARCHE Claude

### hoare logic: wp continued

parent d3fce80e
 ... ... @@ -26,7 +26,6 @@ use import int.Int use import bool.Bool type value = | Verror | Vint int | Vbool bool ... ... @@ -36,55 +35,58 @@ type state = {| var_env : list value; ref_env: list value |} (* semantics of formulas *) function eval_bin (x:value) (op:operator) (y:value) : value = predicate eval_bin (x:value) (op:operator) (y:value) (res:value) = match x,y with | Vint x,Vint y -> match op with | Oplus -> Vint (x+y) | Ominus -> Vint (x-y) | Omult -> Vint (x*y) | Oplus -> res = Vint (x+y) | Ominus -> res = Vint (x-y) | Omult -> res = Vint (x*y) end | _,_ -> Verror | _,_ -> false end use import list.Nth function get_env (i:int) (env:list value) : value = predicate get_env (i:int) (env:list value) (res:value) = match nth i env with | None -> Verror | Some v -> v end function eval_term (s:state) (t:term) : value = match t with | Tconst n -> Vint n | Tvar i -> get_env i (var_env s) | Tderef i -> get_env i (ref_env s) | Tbin t1 op t2 -> eval_bin (eval_term s t1) op (eval_term s t2) | None -> false | Some v -> v = res end inductive eval_term state term value = | eval_const : forall s:state, n:int. eval_term s (Tconst n) (Vint n) | eval_var : forall s:state, i:int, res:value. get_env i (var_env s) res -> eval_term s (Tvar i) res | eval_deref : forall s:state, i:int, res:value. get_env i (ref_env s) res -> eval_term s (Tderef i) res | eval_bin : forall s:state, op:operator, t1 t2:term, r1 r2 r:value. eval_term s t1 r1 -> eval_term s t2 r2 -> eval_bin r1 op r2 r -> eval_term s (Tbin t1 op t2) r function my_state :state = {| var_env = Cons (Vint 42) Nil; ref_env = Nil |} goal Test13 : eval_term my_state (Tconst 13) = Vint 13 eval_term my_state (Tconst 13) (Vint 13) goal Test42 : eval_term my_state (Tvar 0) = Vint 42 eval_term my_state (Tvar 0) (Vint 42) goal Test55 : eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) = Vint 55 eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) (Vint 55) (* predicate eval_fmla (s:state) (f:fmla) = match f with | Fterm t -> match eval_term s t with | Verror -> false | Vint n -> n <> 0 | Vbool b -> b = True predicate eval_fmla (s:state) (f:fmla) (b:bool) = match f with | Fterm t -> eval_term s t with | Verror -> false | Vint n -> n <> 0 | Vbool b -> b = True end | Fand f1 f2 -> eval_fmla s f1 /\ eval_fmla s f2 | Fnot f -> not (eval_fmla s f) ... ...
 ... ... @@ -48,52 +48,73 @@ version="2.19"/> shape="aeval_termamy_stateaTconstc13aVintc13"> shape="aeval_termamy_stateaTvarc0aVintc42"> shape="aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55"> ... ...
 ... ... @@ -22,7 +22,6 @@ Inductive fmla := | Fforall : fmla -> fmla . Inductive value := | Verror : value | Vint : Z -> value | Vbool : bool -> value . ... ... @@ -47,15 +46,16 @@ Definition var_env(u:state): (list value) := | (mk_state var_env1 _) => var_env1 end. Definition eval_bin(x:value) (op:operator) (y:value): value := match (x, Definition eval_bin(x:value) (op:operator) (y:value) (res:value): Prop := match (x, y) with | ((Vint x1), (Vint y1)) => match op with | Oplus => (Vint (x1 + y1)%Z) | Ominus => (Vint (x1 - y1)%Z) | Omult => (Vint (x1 * y1)%Z) | Oplus => (res = (Vint (x1 + y1)%Z)) | Ominus => (res = (Vint (x1 - y1)%Z)) | Omult => (res = (Vint (x1 * y1)%Z)) end | (_, _) => Verror | (_, _) => False end. Inductive option (a:Type) := ... ... @@ -77,30 +77,34 @@ Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), ((nth n l) = (nth (n - 1%Z)%Z r))) end. Definition get_env(i:Z) (env:(list value)): value := match (nth i Definition get_env(i:Z) (env:(list value)) (res:value): Prop := match (nth i env) with | None => Verror | (Some v) => v | None => False | (Some v) => (v = res) end. Set Implicit Arguments. Fixpoint eval_term(s:state) (t:term) {struct t}: value := match t with | (Tconst n) => (Vint n) | (Tvar i) => (get_env i (var_env s)) | (Tderef i) => (get_env i (ref_env s)) | (Tbin t1 op t2) => (eval_bin (eval_term s t1) op (eval_term s t2)) end. Unset Implicit Arguments. Inductive eval_term : state -> term -> value -> Prop := | eval_const : forall (s:state) (n:Z), (eval_term s (Tconst n) (Vint n)) | eval_var : forall (s:state) (i:Z) (res:value), (get_env i (var_env s) res) -> (eval_term s (Tvar i) res) | eval_deref : forall (s:state) (i:Z) (res:value), (get_env i (ref_env s) res) -> (eval_term s (Tderef i) res) | eval_bin1 : forall (s:state) (op:operator) (t1:term) (t2:term) (r1:value) (r2:value) (r:value), (eval_term s t1 r1) -> ((eval_term s t2 r2) -> ((eval_bin r1 op r2 r) -> (eval_term s (Tbin t1 op t2) r))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem Test55 : ((eval_term (mk_state (Cons (Vint 42%Z) (Nil:(list value))) (Nil:(list value))) (Tbin (Tvar 0%Z) Oplus (Tconst 13%Z))) = (Vint 55%Z)). Theorem Test55 : (eval_term (mk_state (Cons (Vint 42%Z) (Nil:(list value))) (Nil:(list value))) (Tbin (Tvar 0%Z) Oplus (Tconst 13%Z)) (Vint 55%Z)). (* YOU MAY EDIT THE PROOF BELOW *) simpl. apply eval_bin1 with (r1:=Vint 42) (r2:=Vint 13). constructor. red; simpl. generalize (nth_def _ 0 (Cons (Vint 42) Nil)). SearchAbout nth. unfold eval_bin; simpl. unfold get_env; simpl. generalize (nth_def _ 0 (Cons (Vint 42) Nil)). ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!