Commit 71b2aa03 by Asma Tafat-Bouzid

### blocking semantic

parent 085407cd
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.MinMax. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). (* Why3 assumption *) Inductive datatype := | TYunit : datatype | TYint : datatype | TYbool : datatype . Axiom datatype_WhyType : WhyType datatype. Existing Instance datatype_WhyType. (* Why3 assumption *) Inductive value := | Vvoid : value | Vint : Z -> value | Vbool : bool -> value . Axiom value_WhyType : WhyType value. Existing Instance value_WhyType. (* Why3 assumption *) Inductive operator := | Oplus : operator | Ominus : operator | Omult : operator | Ole : operator . Axiom operator_WhyType : WhyType operator. Existing Instance operator_WhyType. Axiom mident : Type. Parameter mident_WhyType : WhyType mident. Existing Instance mident_WhyType. Axiom mident_decide : forall (m1:mident) (m2:mident), (m1 = m2) \/ ~ (m1 = m2). (* Why3 assumption *) Inductive ident := | mk_ident : Z -> ident . Axiom ident_WhyType : WhyType ident. Existing Instance ident_WhyType. (* Why3 assumption *) Definition ident_index(v:ident): Z := match v with | (mk_ident x) => x end. Axiom ident_decide : forall (m1:ident) (m2:ident), (m1 = m2) \/ ~ (m1 = m2). (* Why3 assumption *) Inductive term := | Tvalue : value -> term | Tvar : ident -> term | Tderef : mident -> term | Tbin : term -> operator -> term -> term . Axiom term_WhyType : WhyType term. Existing Instance term_WhyType. (* Why3 assumption *) Fixpoint var_occurs_in_term(x:ident) (t:term) {struct t}: Prop := match t with | (Tvalue _) => False | (Tvar i) => (x = i) | (Tderef _) => False | (Tbin t1 _ t2) => (var_occurs_in_term x t1) \/ (var_occurs_in_term x t2) end. (* Why3 assumption *) Inductive fmla := | Fterm : term -> fmla | Fand : fmla -> fmla -> fmla | Fnot : fmla -> fmla | Fimplies : fmla -> fmla -> fmla | Flet : ident -> term -> fmla -> fmla | Fforall : ident -> datatype -> fmla -> fmla . Axiom fmla_WhyType : WhyType fmla. Existing Instance fmla_WhyType. (* Why3 assumption *) Inductive stmt := | Sskip : stmt | Sassign : mident -> term -> stmt | Sseq : stmt -> stmt -> stmt | Sif : term -> stmt -> stmt -> stmt | Sassert : fmla -> stmt | Swhile : term -> fmla -> stmt -> stmt . Axiom stmt_WhyType : WhyType stmt. Existing Instance stmt_WhyType. Axiom decide_is_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip). (* Why3 assumption *) Definition type_value(v:value): datatype := match v with | Vvoid => TYunit | (Vint int) => TYint | (Vbool bool1) => TYbool end. (* Why3 assumption *) Inductive type_operator : operator -> datatype -> datatype -> datatype -> Prop := | Type_plus : (type_operator Oplus TYint TYint TYint) | Type_minus : (type_operator Ominus TYint TYint TYint) | Type_mult : (type_operator Omult TYint TYint TYint) | Type_le : (type_operator Ole TYint TYint TYbool). (* Why3 assumption *) Definition type_stack := (list (ident* datatype)%type). Parameter get_vartype: ident -> (list (ident* datatype)%type) -> datatype. Axiom get_vartype_def : forall (i:ident) (pi:(list (ident* datatype)%type)), match pi with | Nil => ((get_vartype i pi) = TYunit) | (Cons (x, ty) r) => ((x = i) -> ((get_vartype i pi) = ty)) /\ ((~ (x = i)) -> ((get_vartype i pi) = (get_vartype i r))) end. (* Why3 assumption *) Definition type_env := (map mident datatype). (* Why3 assumption *) Inductive type_term : (map mident datatype) -> (list (ident* datatype)%type) -> term -> datatype -> Prop := | Type_value : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (v:value), (type_term sigma pi (Tvalue v) (type_value v)) | Type_var : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (v:ident) (ty:datatype), ((get_vartype v pi) = ty) -> (type_term sigma pi (Tvar v) ty) | Type_deref : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (v:mident) (ty:datatype), ((get sigma v) = ty) -> (type_term sigma pi (Tderef v) ty) | Type_bin : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (t1:term) (t2:term) (op:operator) (ty1:datatype) (ty2:datatype) (ty:datatype), (type_term sigma pi t1 ty1) -> ((type_term sigma pi t2 ty2) -> ((type_operator op ty1 ty2 ty) -> (type_term sigma pi (Tbin t1 op t2) ty))). (* Why3 assumption *) Inductive type_fmla : (map mident datatype) -> (list (ident* datatype)%type) -> fmla -> Prop := | Type_term : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (t:term), (type_term sigma pi t TYbool) -> (type_fmla sigma pi (Fterm t)) | Type_conj : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) -> ((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fand f1 f2))) | Type_neg : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (f:fmla), (type_fmla sigma pi f) -> (type_fmla sigma pi (Fnot f)) | Type_implies : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (f1:fmla) (f2:fmla), (type_fmla sigma pi f1) -> ((type_fmla sigma pi f2) -> (type_fmla sigma pi (Fimplies f1 f2))) | Type_let : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (x:ident) (t:term) (f:fmla) (ty:datatype), (type_term sigma pi t ty) -> ((type_fmla sigma (Cons (x, ty) pi) f) -> (type_fmla sigma pi (Flet x t f))) | Type_forall1 : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYint) pi) f) -> (type_fmla sigma pi (Fforall x TYint f)) | Type_forall2 : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYbool) pi) f) -> (type_fmla sigma pi (Fforall x TYbool f)) | Type_forall3 : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (x:ident) (f:fmla), (type_fmla sigma (Cons (x, TYunit) pi) f) -> (type_fmla sigma pi (Fforall x TYunit f)). (* Why3 assumption *) Inductive type_stmt : (map mident datatype) -> (list (ident* datatype)%type) -> stmt -> Prop := | Type_skip : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)), (type_stmt sigma pi Sskip) | Type_seq : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (s1:stmt) (s2:stmt), (type_stmt sigma pi s1) -> ((type_stmt sigma pi s2) -> (type_stmt sigma pi (Sseq s1 s2))) | Type_assigns : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (x:mident) (t:term) (ty:datatype), ((get sigma x) = ty) -> ((type_term sigma pi t ty) -> (type_stmt sigma pi (Sassign x t))) | Type_if : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (t:term) (s1:stmt) (s2:stmt), (type_term sigma pi t TYbool) -> ((type_stmt sigma pi s1) -> ((type_stmt sigma pi s2) -> (type_stmt sigma pi (Sif t s1 s2)))) | Type_assert : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (p:fmla), (type_fmla sigma pi p) -> (type_stmt sigma pi (Sassert p)) | Type_while : forall (sigma:(map mident datatype)) (pi:(list (ident* datatype)%type)) (guard:term) (body:stmt) (inv:fmla), (type_fmla sigma pi inv) -> ((type_term sigma pi guard TYbool) -> ((type_stmt sigma pi body) -> (type_stmt sigma pi (Swhile guard inv body)))). (* Why3 assumption *) Definition env := (map mident value). (* Why3 assumption *) Definition stack := (list (ident* value)%type). Parameter get_stack: ident -> (list (ident* value)%type) -> value. Axiom get_stack_def : forall (i:ident) (pi:(list (ident* value)%type)), match pi with | Nil => ((get_stack i pi) = Vvoid) | (Cons (x, v) r) => ((x = i) -> ((get_stack i pi) = v)) /\ ((~ (x = i)) -> ((get_stack i pi) = (get_stack i r))) end. Axiom get_stack_eq : forall (x:ident) (v:value) (r:(list (ident* value)%type)), ((get_stack x (Cons (x, v) r)) = v). Axiom get_stack_neq : forall (x:ident) (i:ident) (v:value) (r:(list (ident* value)%type)), (~ (x = i)) -> ((get_stack i (Cons (x, v) r)) = (get_stack i r)). Parameter eval_bin: value -> operator -> value -> value. Axiom eval_bin_def : forall (x:value) (op:operator) (y:value), match (x, y) with | ((Vint x1), (Vint y1)) => match op with | Oplus => ((eval_bin x op y) = (Vint (x1 + y1)%Z)) | Ominus => ((eval_bin x op y) = (Vint (x1 - y1)%Z)) | Omult => ((eval_bin x op y) = (Vint (x1 * y1)%Z)) | Ole => ((x1 <= y1)%Z -> ((eval_bin x op y) = (Vbool true))) /\ ((~ (x1 <= y1)%Z) -> ((eval_bin x op y) = (Vbool false))) end | (_, _) => ((eval_bin x op y) = Vvoid) end. (* Why3 assumption *) Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type)) (t:term) {struct t}: value := match t with | (Tvalue v) => v | (Tvar id) => (get_stack id pi) | (Tderef id) => (get sigma id) | (Tbin t1 op t2) => (eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)) end. (* Why3 assumption *) Inductive compatible : datatype -> value -> Prop := | Compatible_bool : forall (b:bool), (compatible TYbool (Vbool b)) | Compatible_int : forall (n:Z), (compatible TYint (Vint n)) | Compatible_void : (compatible TYunit Vvoid). (* Why3 assumption *) Definition existe_compatible(ty:datatype) (v:value): Prop := match ty with | TYbool => exists b:bool, (v = (Vbool b)) | TYint => exists n:Z, (v = (Vint n)) | TYunit => (v = Vvoid) end. (* Why3 assumption *) Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident datatype)) (pi:(list (ident* value)%type)) (pit:(list (ident* datatype)%type)): Prop := (forall (id:mident), (compatible (get sigmat id) (get sigma id))) /\ forall (id:ident), (compatible (get_vartype id pit) (get_stack id pi)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem eval_type_term : forall (t:term), match t with | (Tvalue v) => True | (Tvar i) => True | (Tderef m) => True | (Tbin t1 o t2) => (forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident* datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) -> ((type_term sigmat pit t2 ty) -> (existe_compatible ty (eval_term sigma pi t2)))) -> ((forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident* datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) -> ((type_term sigmat pit t1 ty) -> (existe_compatible ty (eval_term sigma pi t1)))) -> forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident* datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) -> ((type_term sigmat pit t ty) -> (existe_compatible ty (eval_term sigma pi t)))) end. destruct t; auto. simpl. intros. induction ty. ae. induction o; ae. (* TYbool *) induction o. (* Oplus *) ae. (* Ominus *) ae. (* Omult *) ae. (* Ole *) eexists. inversion H2; subst; clear H2. clear H1. assert (ty1 = TYint). admit. subst. assert (ty2 = TYint). admit. subst. Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -323,10 +323,32 @@ Fixpoint eval_term(sigma:(map mident value)) (pi:(list (ident* value)%type)) pi t2)) end. Axiom eval_bool_term : forall (sigma:(map mident value)) (pi:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident* datatype)%type)) (t:term), (type_term sigmat pit t TYbool) -> exists b:bool, ((eval_term sigma pi t) = (Vbool b)). (* Why3 assumption *) Inductive compatible : datatype -> value -> Prop := | Compatible_bool : forall (b:bool), (compatible TYbool (Vbool b)) | Compatible_int : forall (n:Z), (compatible TYint (Vint n)) | Compatible_void : (compatible TYunit Vvoid). (* Why3 assumption *) Definition existe_compatible(ty:datatype) (v:value): Prop := match ty with | TYbool => exists b:bool, (v = (Vbool b)) | TYint => exists n:Z, (v = (Vint n)) | TYunit => (v = Vvoid) end. (* Why3 assumption *) Definition compatible_env(sigma:(map mident value)) (sigmat:(map mident datatype)) (pi:(list (ident* value)%type)) (pit:(list (ident* datatype)%type)): Prop := (forall (id:mident), (compatible (get sigmat id) (get sigma id))) /\ forall (id:ident), (compatible (get_vartype id pit) (get_stack id pi)). Axiom eval_type_term : forall (t:term) (sigma:(map mident value)) (pi:(list (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident* datatype)%type)) (ty:datatype), (compatible_env sigma sigmat pi pit) -> ((type_term sigmat pit t ty) -> (existe_compatible ty (eval_term sigma pi t))). (* Why3 assumption *) Fixpoint eval_fmla(sigma:(map mident value)) (pi:(list (ident* value)%type)) ... ...
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment