Commit f45b8ae4 authored by MARCHE Claude's avatar MARCHE Claude

some cleaning

parent e42b9985
......@@ -217,9 +217,11 @@ pvsbin/
/examples/*/*.byte
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
/examples/*.html
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
/examples/style.css
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
......
......@@ -37,3 +37,44 @@ module LemmaFunction2
sum a 0 (length a) >= 0
end
module M
use import int.Int
type list 'a = Nil | Cons 'a (list 'a)
function length (l:list 'a) : int =
match l with
| Nil -> 0
| Cons x r -> 1 + length r
end
let rec lemma_length_non_neg (l:list 'a) : unit
variant { l }
ensures { length l >= 0 }
=
match l with
| Nil -> ()
| Cons x r -> lemma_length_non_neg r
end
let rec toy_example(l:list 'a) : unit
(* variant { l } does not work (not a sub-term) *)
variant { length l }
(* works if we add the "ghost lemma_length_non_neg" *)
=
match l with
| Nil -> ()
| Cons _ Nil -> ()
| Cons x (Cons _ r) ->
ghost lemma_length_non_neg l;
toy_example (Cons x r)
end
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="3" memlimit="1000"/>
<file name="../lemma_functions.mlw" expanded="true">
<theory name="LemmaFunction1" sum="517c6ac9e27af62740c4517179a6ab8a" expanded="true">
<goal name="WP_parameter f" expl="VC for f" sum="956a86c77e03c5e1222ce4600716dca8" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="g" sum="28365d75b1205717e9be771a4efb4084" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="LemmaFunction2" sum="9984ac57e47da6e204b72db634713475" expanded="true">
<goal name="WP_parameter sum_nonneg" expl="VC for sum_nonneg" sum="c0b6e3bf002eb3391197e114225b407c" expanded="true">
<proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="g1" sum="8c36bac0106b2fcb2e3f896f44c58607" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="M" sum="78ec23e4aa96c446527cbbb757ce288f" expanded="true">
<goal name="WP_parameter lemma_length_non_neg" expl="VC for lemma_length_non_neg" sum="97f0d74034fa8f7b1e804b0784e3e053" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter toy_example" expl="VC for toy_example" sum="cbbcff76a2e5b8b9b83a4d0a809b5c91" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
</why3session>
module M
use import int.Int
lemma l1: 1 = 1
let f (x:int) : int
ensures { result > 0 }
=
(* assert { x > 0 }; *)
42
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
version="0.95.2"/>
<file
name="../test_merge.mlw"
verified="true"
expanded="true">
<theory
name="M"
locfile="../test_merge.mlw"
loclnum="3" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="l1"
locfile="../test_merge.mlw"
loclnum="7" loccnumb="8" loccnume="10"
sum="41600830d468d02ad00fa968a56cacde"
proved="true"
expanded="true"
shape="ainfix =c1c1">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter f"
locfile="../test_merge.mlw"
loclnum="9" loccnumb="6" loccnume="7"
expl="VC for f"
sum="98b7bd9a4c152591f929c11204735fb8"
proved="true"
expanded="true"
shape="ainfix &gt;c42c0">
<label
name="expl:VC for f"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="WP_parameter f.1"
locfile="../test_merge.mlw"
loclnum="9" loccnumb="6" loccnume="7"
expl="1. postcondition"
sum="98b7bd9a4c152591f929c11204735fb8"
proved="true"
expanded="true"
shape="postconditionainfix &gt;c42c0">
<label
name="expl:VC for f"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
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