Skip to content

GitLab

why3
why3
Commit b45604c2 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

modified definition of permutation; quicksort proof updated

parent 0496718b
Hide whitespace changes
Inline Side-by-side
Showing with 208 additions and 12 deletions
.gitignore
View file @ b45604c2
......@@ -156,10 +156,8 @@ why.conf
/examples/programs/vstte10_max_sum/
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/
/examples/programs/insertion_sort_list/
/examples/programs/mergesort_list/
/examples/programs/same_fringe/
/examples/programs/quicksort/
/examples/programs/algo63/
/examples/programs/algo64/
/examples/programs/algo65/
......
examples/programs/insertion_sort_list/why3session.xml 0 → 100644
View file @ b45604c2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/insertion_sort_list/why3session.xml">
<file name="../insertion_sort_list.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter insert" expl="correctness of parameter insert" sum="1ab3de41db4f19ec372372833aaeb2c0" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insert.1" expl="correctness of parameter insert" sum="76ce5493fcb11812e4e0e2698821a9c7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insert.2" expl="correctness of parameter insert" sum="ba3b39ae8e0a43555fed2cbd3108f3b6" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter insert.3" expl="correctness of parameter insert" sum="ff85e099c9e0bf62cd804ace872aefc3" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.25"/>
</proof>
</goal>
<goal name="WP_parameter insert.4" expl="correctness of parameter insert" sum="eecdbeb9ac4fb34fe11cdb3681c32bf4" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort" expl="correctness of parameter insertion_sort" sum="43755e483026796b703bffb5d4046c34" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.1" expl="correctness of parameter insertion_sort" sum="f1743569992089d7a7adee34e760d448" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.2" expl="correctness of parameter insertion_sort" sum="de6677511339e34ead245491d373655e" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3" expl="correctness of parameter insertion_sort" sum="3e193c91b649ab35cae9b3555ee4c05b" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.09"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.4" expl="correctness of parameter insertion_sort" sum="2aec1cc621d57570ae9049fc6be1fb0c" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/programs/quicksort.mlw
View file @ b45604c2
......@@ -30,7 +30,7 @@ module Quicksort
for i = l + 1 to r do
invariant { (forall j:int. l < j <= !m -> t[j] < v) and
(forall j:int. !m < j < i -> t[j] >= v) and
permut_sub t (at t L) l r and
permut_sub t (at t L) l (r+1) and
t[l] = v and l <= !m < i }
if t[i] < v then begin m := !m + 1; swap t i !m end
done;
......@@ -38,11 +38,11 @@ module Quicksort
quick_rec t l (!m - 1);
quick_rec t (!m + 1) r
end end
{ (l <= r and sorted_sub t l r and permut_sub t (old t) l r) or
{ (l <= r and sorted_sub t l (r+1) and permut_sub t (old t) l (r+1)) or
(l > r and array_eq t (old t)) }
let quicksort (t : array int) =
{}
{ }
quick_rec t 0 (length t - 1)
{ sorted t and permut t (old t) }
......
examples/programs/quicksort/why3session.xml 0 → 100644
View file @ b45604c2
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/quicksort/why3session.xml">
<file name="../quicksort.mlw" verified="true" expanded="true">
<theory name="Quicksort" verified="true" expanded="true">
<goal name="WP_parameter swap" expl="correctness of parameter swap" sum="e75f744f287ab933e3389b0e4eef5b9a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec" expl="correctness of parameter quick_rec" sum="f581292fd7a87b96f4b555f6180e4348" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.1" expl="precondition" sum="437e900bf0d49e2cbd137a4e4afaf0d1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.2" expl="precondition" sum="4e4e1cc5965c63899da7c33518e5f8a7" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.2.1" expl="correctness of parameter quick_rec" sum="909229a19a56396d5eac43f07ac6278e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.2.2" expl="correctness of parameter quick_rec" sum="fa274e41073ff66c4e1e663a94d234ef" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.2.3" expl="correctness of parameter quick_rec" sum="909229a19a56396d5eac43f07ac6278e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.2.4" expl="correctness of parameter quick_rec" sum="fa274e41073ff66c4e1e663a94d234ef" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter quick_rec.3" expl="precondition" sum="b4763a07d58489e51daa421d2654e91e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.4" expl="precondition" sum="9bb11b2bb943e6148de441e616e8fd96" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.5" expl="normal postcondition" sum="d06487f91003d45379244ba78f978f86" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.6" expl="for loop initialization" sum="29ebf93b42994ddd85bc42d33bdbf5ce" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.7" expl="for loop preservation" sum="040dfe39a3340b772f5dfda974290830" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.8" expl="precondition" sum="084d38a6497f80e071ea7ce93a0fb35a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.9" expl="precondition" sum="d651db3bee641a43a0c81014c86066f3" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.10" expl="precondition" sum="41f48cf1f8c17fccc96ce1409f80fa85" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="16.46"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.11" expl="normal postcondition" sum="b595baacbd4fe7f2f30ee4c374a1a092" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter quick_rec.12" expl="normal postcondition" sum="5b3a80ba060fba075e1e017f678b2b96" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="29" edited="" obsolete="true">
<result status="valid" time="0.04"/>
</proof>
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quick_rec.12.1" expl="normal postcondition" sum="5b3a80ba060fba075e1e017f678b2b96" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter quicksort" expl="correctness of parameter quicksort" sum="0c3a73454cf08bad762947e15c791964" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter quicksort.1" expl="precondition" sum="46527162c35ba8b0ae9cb7e2aaf91374" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter quicksort.2" expl="normal postcondition" sum="37fccf13e4acbc8b375b7e7b456e7447" proved="true" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.04"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.08"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
modules/array.mlw
View file @ b45604c2
......@@ -131,9 +131,18 @@ module ArrayPermut
logic permut (a1 a2: array 'a) =
a1.length = a2.length and M.permut_sub a1.elts a2.elts 0 a1.length
use import module ArrayEq
lemma array_eq_sub_permut:
forall a1 a2: array 'a, l u: int.
array_eq_sub a1 a2 l u -> permut_sub a1 a2 l u
lemma array_eq_permut:
forall a1 a2: array 'a.
array_eq a1 a2 -> permut a1 a2
end
(***
module TestArray
use import int.Int
......@@ -142,7 +151,7 @@ module TestArray
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
set a1 3 4;
a1[3] <- 4;
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
......@@ -168,7 +177,6 @@ module TestArray
assert { a2[24] = False }
end
***)
(*
Local Variables:
......
theories/map.why
View file @ b45604c2
......@@ -55,6 +55,7 @@ theory MapPermut
use import int.Int
use export Map
use import MapEq
logic exchange (a1 a2 : map int 'a) (i j : int) =
a1[i] = a2[j] and a2[i] = a1[j] and
......@@ -66,7 +67,8 @@ theory MapPermut
inductive permut_sub (map int 'a) (map int 'a) int int =
| permut_refl :
forall a : map int 'a. forall l u : int. permut_sub a a l u
forall a1 a2 : map int 'a. forall l u : int.
map_eq_sub a1 a2 l u -> permut_sub a1 a2 l u
| permut_sym :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
......@@ -84,13 +86,13 @@ theory MapPermut
lemma permut_eq :
forall a1 a2 : map int 'a. forall l u : int.
l <= u -> permut_sub a1 a2 l u ->
forall i:int. (i < l or u < i) -> a2[i] = a1[i]
forall i:int. (i < l or u <= i) -> a2[i] = a1[i]
lemma permut_exists :
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u ->
forall i : int. l <= i <= u ->
exists j : int. l <= j <= u and a2[i] = a1[j]
forall i : int. l <= i < u ->
exists j : int. l <= j < u and a2[i] = a1[j]
end
......
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