Commit d514f045 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

a few more syntax updates

parent 20204945
......@@ -41,11 +41,20 @@ p4 = 10 - (2 - 3)
</pre></blockquote>}
*)
constant p0 : prog = Cte 0
constant p1 : prog = Sub (Cte 10) (Cte 6)
constant p2 : prog = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2))
constant p3 : prog = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6))
constant p4 : prog = Sub (Cte 10) (Sub (Cte 2) (Cte 3))
val constant p0 : prog
ensures { result = Cte 0 }
val constant p1 : prog
ensures { result = Sub (Cte 10) (Cte 6) }
val constant p2 : prog
ensures { result = Sub (Sub (Cte 10) (Cte 6)) (Sub (Cte 7) (Cte 2)) }
val constant p3 : prog
ensures { result = Sub (Sub (Cte 7) (Cte 2)) (Sub (Cte 10) (Cte 6)) }
val constant p4 : prog
ensures { result = Sub (Cte 10) (Sub (Cte 2) (Cte 3)) }
end
......@@ -94,13 +103,13 @@ holds.
(* Note: Why3 definitions introduced by "function" belong to the logic
part of Why3 language *)
function eval_0 (e:expr) : int =
let rec function eval_0 (e:expr) : int =
match e with
| Cte n -> n
| Sub e1 e2 -> eval_0 e1 - eval_0 e2
end
function interpret_0 (p:prog) : int = eval_0 p
let function interpret_0 (p:prog) : int = eval_0 p
(** Tests, can be replayed using
{h <blockquote><pre>
......@@ -147,10 +156,10 @@ function eval_1 (e:expr) (k: int->'a) : 'a =
match e with
| Cte n -> k n
| Sub e1 e2 ->
eval_1 e1 (\ v1. eval_1 e2 (\ v2. k (v1 - v2)))
eval_1 e1 (fun v1 -> eval_1 e2 (fun v2 -> k (v1 - v2)))
end
function interpret_1 (p : prog) : int = eval_1 p (\ n. n)
function interpret_1 (p : prog) : int = eval_1 p (fun n -> n)
(** Soundness *)
......@@ -482,11 +491,11 @@ function eval_1 (e:expr) (k:value -> 'a) : 'a =
match e with
| Cte n -> k (if n >= 0 then Vnum n else Underflow)
| Sub e1 e2 ->
eval_1 e1 (\ v1.
eval_1 e1 (fun v1 ->
match v1 with
| Underflow -> k Underflow
| Vnum v1 ->
eval_1 e2 (\ v2.
eval_1 e2 (fun v2 ->
match v2 with
| Underflow -> k Underflow
| Vnum v2 -> k (if v1 >= v2 then Vnum (v1 - v2) else Underflow)
......@@ -494,7 +503,7 @@ function eval_1 (e:expr) (k:value -> 'a) : 'a =
end)
end
function interpret_1 (p : prog) : value = eval_1 p (\ n. n)
function interpret_1 (p : prog) : value = eval_1 p (fun n -> n)
lemma cps_correct_expr:
......@@ -526,8 +535,8 @@ function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
match e with
| Cte n -> if n >= 0 then k n else kerr ()
| Sub e1 e2 ->
eval_2 e1 (\ v1.
eval_2 e2 (\ v2.
eval_2 e1 (fun v1 ->
eval_2 e2 (fun v2 ->
if v1 >= v2 then k (v1 - v2) else kerr ())
kerr) kerr
end
......@@ -541,15 +550,15 @@ function eval_2 (e:expr) (k:int -> 'a) (kerr: unit -> 'a) : 'a =
end
with eval_2a (e2:expr) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
(\ v1. eval_2 e2 (eval_2b v1 k kerr) kerr)
(fun v1 -> eval_2 e2 (eval_2b v1 k kerr) kerr)
with eval_2b (v1:int) (k:int -> 'a) (kerr : unit -> 'a) : int -> 'a =
(\ v2. if v1 >= v2 then k (v1 - v2) else kerr ())
(fun v2 -> if v1 >= v2 then k (v1 - v2) else kerr ())
function interpret_2 (p : prog) : value =
eval_2 p (\ n. Vnum n) (\ _. Underflow)
eval_2 p (fun n -> Vnum n) (fun _ -> Underflow)
lemma cps2_correct_expr_aux:
......@@ -585,13 +594,13 @@ function eval_3 (e:expr) (k:int -> value) : value =
end
with eval_3a (e2:expr) (k:int -> value) : int -> value =
(\ v1. eval_3 e2 (eval_3b v1 k))
(fun v1 -> eval_3 e2 (eval_3b v1 k))
with eval_3b (v1:int) (k:int -> value) : int -> value =
(\ v2. if v1 >= v2 then k (v1 - v2) else Underflow)
(fun v2 -> if v1 >= v2 then k (v1 - v2) else Underflow)
function interpret_3 (p : prog) : value = eval_3 p (\ n. Vnum n)
function interpret_3 (p : prog) : value = eval_3 p (fun n -> Vnum n)
let rec lemma cps3_correct_expr (e:expr) : unit
variant { e }
......@@ -817,7 +826,7 @@ recompose ([n1 C], e2) = recompose (C, n1 - e2)
</pre></blockquote>}
*)
function recompose (c:context) (e:expr) : expr =
let rec function recompose (c:context) (e:expr) : expr =
match c with
| Empty -> e
| Left c e2 -> recompose c (Sub e e2)
......
......@@ -11,7 +11,7 @@ module DfaExample
use import option.Option
type stream model { mutable state: list char }
type stream = abstract { mutable state: list char }
val input: stream
......
......@@ -2,113 +2,71 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="Coq" version="8.4pl6" timelimit="8" steplimit="1" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="4000"/>
<prover id="8" name="Z3" version="4.4.0" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="1" memlimit="1000"/>
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="660b70fa1d4035d9e6c3f57fd8521252" expanded="true">
<theory name="DfaExample" sum="a19ab18d9ec071c6937a8e3fcf29f296" expanded="true">
<goal name="nil_notin_r1">
<proof prover="2" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.79"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="7"><result status="valid" time="0.08" steps="140"/></proof>
<proof prover="0"><result status="valid" time="0.08" steps="244"/></proof>
</goal>
<goal name="WP_parameter all_in_r0" expl="VC for all_in_r0">
<proof prover="7"><result status="valid" time="2.96" steps="2858"/></proof>
<goal name="VC all_in_r0" expl="VC for all_in_r0">
<proof prover="0"><result status="valid" time="0.03" steps="106"/></proof>
</goal>
<goal name="words_in_r1_end_with_one">
<proof prover="8"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1">
<goal name="VC words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1">
<transf name="split_goal_wp">
<goal name="WP_parameter words_in_r1_suffix_in_r1.1" expl="1. assertion">
<proof prover="7" memlimit="1000"><result status="valid" time="0.04" steps="78"/></proof>
<goal name="VC words_in_r1_suffix_in_r1.1" expl="1. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
<goal name="WP_parameter words_in_r1_suffix_in_r1.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.15"/></proof>
<goal name="VC words_in_r1_suffix_in_r1.2" expl="2. postcondition">
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter zero_w_in_r1" expl="VC for zero_w_in_r1">
<proof prover="8"><result status="valid" time="0.21"/></proof>
<goal name="VC zero_w_in_r1" expl="VC for zero_w_in_r1">
<proof prover="3"><result status="valid" time="0.51"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1" expl="VC for one_w_in_r1">
<goal name="VC one_w_in_r1" expl="VC for one_w_in_r1">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.1" expl="1. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.28" steps="377"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.2" expl="2. assertion">
<proof prover="7" memlimit="1000"><result status="valid" time="0.24" steps="386"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.3" expl="3. assertion">
<proof prover="7" memlimit="1000"><result status="valid" time="0.04" steps="40"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.4" expl="4. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter one_w_in_r1.4.1" expl="1. VC for one_w_in_r1">
<proof prover="7" memlimit="1000"><result status="valid" time="0.25" steps="337"/></proof>
</goal>
<goal name="WP_parameter one_w_in_r1.4.2" expl="2. VC for one_w_in_r1">
<proof prover="7" memlimit="1000"><result status="valid" time="0.01" steps="11"/></proof>
<goal name="VC one_w_in_r1.1" expl="1. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC one_w_in_r1.2" expl="2. assertion">
<proof prover="0"><result status="valid" time="0.45" steps="270"/></proof>
</goal>
<goal name="VC one_w_in_r1.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="40"/></proof>
</goal>
<goal name="VC one_w_in_r1.4" expl="4. postcondition">
<transf name="introduce_premises">
<goal name="VC one_w_in_r1.4.1" expl="1. postcondition">
<transf name="split_goal_wp">
<goal name="VC one_w_in_r1.4.1.1" expl="1. VC for one_w_in_r1">
<proof prover="0"><result status="valid" time="0.21" steps="242"/></proof>
</goal>
<goal name="VC one_w_in_r1.4.1.2" expl="2. VC for one_w_in_r1">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="zero_w_in_r2">
<proof prover="7" memlimit="1000"><result status="valid" time="0.04" steps="75"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="84"/></proof>
</goal>
<goal name="one_w_in_r2">
<proof prover="7" memlimit="1000"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="WP_parameter astate1" expl="VC for astate1">
<transf name="split_goal_wp">
<goal name="WP_parameter astate1.1" expl="1. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
</goal>
<goal name="WP_parameter astate1.2" expl="2. variant decrease">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate1.3" expl="3. postcondition">
<transf name="split_goal_wp">
<goal name="WP_parameter astate1.3.1" expl="1. VC for astate1">
<proof prover="7" memlimit="1000"><result status="valid" time="0.04" steps="9"/></proof>
</goal>
<goal name="WP_parameter astate1.3.2" expl="2. VC for astate1">
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="48"/></proof>
</goal>
<goal name="WP_parameter astate1.3.3" expl="3. VC for astate1">
<proof prover="7" memlimit="1000"><result status="valid" time="0.05" steps="37"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter astate1.4" expl="4. variant decrease">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate1.5" expl="5. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.12" steps="244"/></proof>
</goal>
</transf>
<goal name="VC astate1" expl="VC for astate1">
<proof prover="0"><result status="valid" time="0.06" steps="193"/></proof>
</goal>
<goal name="WP_parameter astate2" expl="VC for astate2">
<transf name="split_goal_wp">
<goal name="WP_parameter astate2.1" expl="1. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="62"/></proof>
</goal>
<goal name="WP_parameter astate2.2" expl="2. variant decrease">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate2.3" expl="3. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.06" steps="163"/></proof>
</goal>
<goal name="WP_parameter astate2.4" expl="4. variant decrease">
<proof prover="7" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="WP_parameter astate2.5" expl="5. postcondition">
<proof prover="7" memlimit="1000"><result status="valid" time="0.12" steps="117"/></proof>
</goal>
</transf>
<goal name="VC astate2" expl="VC for astate2">
<proof prover="0"><result status="valid" time="0.05" steps="227"/></proof>
</goal>
</theory>
</file>
......
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