Commit 7bb2c97d authored by Andrei Paskevich's avatar Andrei Paskevich
parents 2c487dd1 4afeabbd
......@@ -131,7 +131,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
encoding_explicit encoding_guard encoding_sort \
encoding_instantiate simplify_array filter_trigger \
introduction abstraction close_epsilon lift_epsilon \
eval_match instantiate_predicate
eval_match instantiate_predicate smoke_detector
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq tptp simplify gappa \
cvc3 yices
......
......@@ -487,9 +487,12 @@ not and you have to use the IDE to update it.
\begin{itemize}
\item The exit code is 0 if no difference was detected, 1 if there
was. Other exit codes mean some failure in running the replay.
\item option \texttt{-s}: suppresses the output of the final tree view
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath
\item option \texttt{-force}: force writing a new session file even if some proofs did not replay correctly.
\item option \texttt{-s}: suppresses the output of the final tree view.
\item option \texttt{-I \textsl{<path>}}: add \textsl{<path>} to the loadpath.
\item option \texttt{-force}: force writing a new session file even if
some proofs did not replay correctly.
\item option \texttt{-smoke-detector \{none|top|deep\}} try to detect
if the context is self-contradicting.
\item option \texttt{-latex \textsl{<dir>}}: produce a summary of
the replay under the form of a tabular environment in LaTeX, one
tabular for each theory, one per file, in directory \texttt{\textsl{<dir>}}.
......@@ -499,6 +502,46 @@ not and you have to use the IDE to update it.
% the replay in HTML syntax.
\end{itemize}
\paragraph{Smoke Detector}
The smoke detector try to detect if the context is self-contradicting
and, thus, that anything can be proved in this context. The smoke
detector can't be run on outdated session and doesn't modify the session.
It has three possible configurations :
\begin{itemize}
\item \texttt{none} : don't run the smoke detector
\item \texttt{top} : The negation of each proved goals
tries to be proved with the same timeout and the same prover which
prove the goal.
\begin{verbatim}
[ ... ]
Goal G : forall x:int. q x -> (p1 x \/ p2 x)
\end{verbatim}
becomes
\begin{verbatim}
[ ... ]
Goal G : ~ (forall x:int. q x -> (p1 x \/ p2 x))
\end{verbatim}
\item \texttt{deep} : The same technique as \texttt{top} but the
negation is pushed under the universal quantification (without
changing them) and under the implication. The previous example becomes
\begin{verbatim}
[ ... ]
Goal G : forall x:int. q x /\ ~ (p1 x \/ p2 x)
\end{verbatim}
\end{itemize}
The name of the goals which triggered the smoke detector are printed :
\begin{verbatim}
goal 'G', prover 'Alt-Ergo 0.93.1': Smoke detected!!!
\end{verbatim}
Moreover \texttt{Smoke detected} (exit code 1) is printed at the end if the smoke
detector has been trigged, or \texttt{No smoke detected} (exit code 0)
otherwise.
\paragraph{Customizing LaTeX output}
The generated LaTeX files contain some macros that must be defined
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="formula/why3session.xml">
name="hoare_logic/formula/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
......@@ -61,7 +61,7 @@
expanded="true">
<goal
name="Test1"
sum="6bcc11f84daf50293f0fb99637a8f70a"
sum="ad0268b5331a68e8313850369f12a695"
proved="true"
expanded="true"
shape="Lamk_identc0LasetaconstaFalseV0aTrueainfix =aevalaForaFnotaFatomV0aFfalseV1aFalse">
......@@ -70,21 +70,21 @@
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.59"/>
<result status="valid" time="0.24"/>
</proof>
</goal>
</theory>
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla :=
| Fterm : expr -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla .
Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
| (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
| (Fnot f1) => ~ (eval_fmla s f1)
end.
Unset Implicit Arguments.
Parameter subst_expr: expr -> ident -> expr -> expr.
Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
match e with
| (Econst _) => ((subst_expr e x t) = e)
| (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
((subst_expr e x t) = e))
| (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
(subst_expr e2 x t)))
end.
Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)).
Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (subst_expr e x t))
| (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
| (Fnot f1) => (Fnot (subst f1 x t))
end.
Unset Implicit Arguments.
Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)), (many_steps s i
sqt Sskip) -> (eval_fmla sqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:ident) (e:expr),
(valid_triple (subst q x e) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem if_rule : forall (e:expr) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold valid_triple.
intros e p q i1 i2 (H1,H2).
intros s H s' H'.
inversion H'; subst; auto.
inversion H0; subst; auto.
apply H1 with (s:=s2); auto.
simpl; auto.
apply H2 with (s:=s2); auto.
simpl; auto.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Parameter mk_ident: Z -> ident.
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z))
(i1:stmt) (i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) ->
exists s2:(map ident Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2
s3 Sskip).
(* YOU MAY EDIT THE PROOF BELOW *)
intros s1 s3 i i3 H.
elim H.
(* case 1/2 : 0 steps *)
intros s i0 H0 i1 i2 H12.
subst; discriminate.
(* case 2/2 : at least one step *)
intros s2 s4 s5 i1 i2 i4.
intros Hstep Hmany Hind.
intros H4 i5 i6 H56.
subst.
inversion Hstep; subst.
(* case 1: one_step_seq (no skip) *)
elim Hind with (i1:=i1qt) (i2:=i6); auto; clear Hind.
intros s6 (H1,H2).
exists s6.
split; auto.
eapply many_steps_trans; eauto.
(* case 2: one_step_seq_skip *)
exists s4.
split; [constructor | auto].
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
| Sseq : stmt -> stmt -> stmt
| Sif : expr -> stmt -> stmt -> stmt
| Swhile : expr -> stmt -> stmt .
Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition state := (map ident Z).
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
| Ominus => (x - y)%Z
| Omult => (x * y)%Z
end.
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
| (Econst n) => n
| (Evar x) => (get s x)
| (Ebin e1 op e2) => (eval_bin (eval_expr s e1) op (eval_expr s e2))
end.
Unset Implicit Arguments.
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Sif e i1 i2) s i1)
| one_step_if_false : forall (s:(map ident Z)) (e:expr) (i1:stmt)
(i2:stmt), ((eval_expr s e) = 0%Z) -> (one_step s (Sif e i1 i2) s i2)
| one_step_while_true : forall (s:(map ident Z)) (e:expr) (i:stmt),
(~ ((eval_expr s e) = 0%Z)) -> (one_step s (Swhile e i) s (Sseq i
(Swhile e i)))
| one_step_while_false : forall (s:(map ident Z)) (e:expr) (i:stmt),
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
| many_steps_trans : forall (s1:(map ident Z)) (s2:(map ident Z)) (s3:(map
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
Axiom many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
(many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip)).
Axiom many_steps_seq : forall (s1:(map ident Z)) (s3:(map ident Z)) (i1:stmt)
(i2:stmt), (many_steps s1 (Sseq i1 i2) s3 Sskip) -> exists s2:(map ident
Z), (many_steps s1 i1 s2 Sskip) /\ (many_steps s2 i2 s3 Sskip).
Inductive fmla :=
| Fterm : expr -> fmla
| Fand : fmla -> fmla -> fmla
| Fnot : fmla -> fmla .
Set Implicit Arguments.
Fixpoint eval_fmla(s:(map ident Z)) (f:fmla) {struct f}: Prop :=
match f with
| (Fterm e) => ~ ((eval_expr s e) = 0%Z)
| (Fand f1 f2) => (eval_fmla s f1) /\ (eval_fmla s f2)
| (Fnot f1) => ~ (eval_fmla s f1)
end.
Unset Implicit Arguments.
Parameter subst_expr: expr -> ident -> expr -> expr.
Axiom subst_expr_def : forall (e:expr) (x:ident) (t:expr),
match e with
| (Econst _) => ((subst_expr e x t) = e)
| (Evar y) => ((x = y) -> ((subst_expr e x t) = t)) /\ ((~ (x = y)) ->
((subst_expr e x t) = e))
| (Ebin e1 op e2) => ((subst_expr e x t) = (Ebin (subst_expr e1 x t) op
(subst_expr e2 x t)))
end.
Axiom eval_subst_expr : forall (s:(map ident Z)) (e:expr) (x:ident) (t:expr),
((eval_expr s (subst_expr e x t)) = (eval_expr (set s x (eval_expr s t))
e)).
Set Implicit Arguments.
Fixpoint subst(f:fmla) (x:ident) (t:expr) {struct f}: fmla :=
match f with
| (Fterm e) => (Fterm (subst_expr e x t))
| (Fand f1 f2) => (Fand (subst f1 x t) (subst f2 x t))
| (Fnot f1) => (Fnot (subst f1 x t))
end.
Unset Implicit Arguments.
Axiom eval_subst : forall (s:(map ident Z)) (f:fmla) (x:ident) (t:expr),
(eval_fmla s (subst f x t)) -> (eval_fmla (set s x (eval_expr s t)) f).
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (s:(map
ident Z)), (eval_fmla s p) -> forall (sqt:(map ident Z)), (many_steps s i
sqt Sskip) -> (eval_fmla sqt q).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem skip_rule : forall (q:fmla), (valid_triple q Sskip q).
(* YOU MAY EDIT THE PROOF BELOW *)
unfold valid_triple.
intros q s H s' H'.
inversion H'; subst; auto.
inversion H0.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
Inductive expr :=