Skip to content

GitLab

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

list.Sorted generalized for elements of any type

parent e2fb1f1f
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 564 additions and 139 deletions
.gitignore
View file @ 0f6593e1
......@@ -164,4 +164,5 @@ why3.conf
/modules/string/
/modules/stack/
/modules/queue/
/modules/pqueue/
examples/programs/insertion_sort_list.mlw
View file @ 0f6593e1
......@@ -5,7 +5,7 @@ module M
use import int.Int
use import list.Length
use import list.Sorted
use import list.SortedInt
use import list.Permut
let rec insert x l variant { length l } =
......
examples/programs/insertion_sort_list/why3session.xml
View file @ 0f6593e1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/insertion_sort_list/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../insertion_sort_list.mlw" verified="true" expanded="true">
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter insert" expl="parameter insert" sum="25c24baa4bc72c76f094d989bdbdd219" proved="true" expanded="true" shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix <=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1IasortedV1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insert.1" expl="parameter insert" sum="099ffda715f4b33e0d64a009e456166e" proved="true" expanded="true" shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVVtIasortedV1FF">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<why3session
name="examples/programs/insertion_sort_list/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="yices"
name="Yices"
version="1.0.27"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../insertion_sort_list.mlw"
verified="true"
expanded="true">
<theory
name="WP M"
verified="true"
expanded="true">
<goal
name="WP_parameter insert"
expl="parameter insert"
sum="a45ea2ff7f8dd7b70d2580780f66e462"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix <=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1IasortedV1FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter insert.1"
expl="parameter insert"
sum="65feb55c3a7c4a9641aa9d9b8b51f0fb"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVVtIasortedV1FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter insert.2" expl="parameter insert" sum="f9cbbe314c8a2e2825c280d8f882e282" proved="true" expanded="true" shape="CV1aNiltaConsVVapermutaConsV0V1aConsV0V1AasortedaConsV0V1Iainfix <=V0V2IasortedV1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="WP_parameter insert.2"
expl="parameter insert"
sum="9c2b72957da289ef92caba64988f9fc9"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV0V1AasortedaConsV0V1Iainfix <=V0V2IasortedV1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insert.3" expl="parameter insert" sum="06bd45504e018ae3b20a98fa9d5ac06b" proved="true" expanded="true" shape="CV1aNiltaConsVVasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="WP_parameter insert.3"
expl="parameter insert"
sum="04e343cdd3cde524e1b6d6cd3596dffa"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insert.4" expl="parameter insert" sum="0a133ebb44619ebfce3cab3fdd9040e3" proved="true" expanded="true" shape="CV1aNiltaConsVVapermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.14"/>
<goal
name="WP_parameter insert.4"
expl="parameter insert"
sum="090eed092aabbc07848c36702a84d1c8"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVapermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FIasortedV3Aainfix <alengthV3alengthV1Aainfix <=c0alengthV1Iainfix <=V0V2NIasortedV1FF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.16"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter insertion_sort" expl="parameter insertion_sort" sum="3c38e5cabf89523efce0797980e1eef3" proved="true" expanded="true" shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAtAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter insertion_sort.1" expl="parameter insertion_sort" sum="d9fd7c14671630548e7bfb2ab1871803" proved="true" expanded="true" shape="CV0aNilapermutV0aNilAasortedaNilaConsVVtF">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter insertion_sort"
expl="parameter insertion_sort"
sum="46635995e70dafba62918db97266e98f"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAtAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter insertion_sort.1"
expl="parameter insertion_sort"
sum="7963349a720db53ba491c9bca7053a8b"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVtF">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.2" expl="parameter insertion_sort" sum="7da0abebad5e9106838132c79477cb22" proved="true" expanded="true" shape="CV0aNiltaConsVVtAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="WP_parameter insertion_sort.2"
expl="parameter insertion_sort"
sum="27a3062937b8ed1da51c09ec52470022"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVtAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<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="parameter insertion_sort" sum="d5c33c1472fa4a03063ca3ba353b5925" proved="true" expanded="true" shape="CV0aNiltaConsVVasortedV3IapermutV2V3AasortedV3FItAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter insertion_sort.3"
expl="parameter insertion_sort"
sum="6ef15f5b330e8edef7df11c869826969"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVasortedV3IapermutV2V3AasortedV3FItAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.4" expl="parameter insertion_sort" sum="f2e7ff6664eafd0ec0ccca520c2d17db" proved="true" expanded="true" shape="CV0aNiltaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FItAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<goal
name="WP_parameter insertion_sort.4"
expl="parameter insertion_sort"
sum="502c37d439bb83979123f028666cb157"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FIasortedV3IapermutV2V3AasortedV3FItAainfix <alengthV2alengthV0Aainfix <=c0alengthV0F">
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
</transf>
......
examples/programs/mergesort_list.mlw
View file @ 0f6593e1
......@@ -5,7 +5,7 @@ module M
use import int.Int
use import list.Length
use import list.Sorted
use import list.SortedInt
use import list.Append
use import list.Permut
......
examples/programs/sorted_list.mlw
View file @ 0f6593e1
......@@ -4,7 +4,7 @@ module FindInSortedList
use import int.Int
use import list.Mem
use import list.Sorted
use import list.SortedInt
lemma Sorted_not_mem:
forall x y : int, l : list int.
......
examples/programs/sorted_list/why3session.xml
View file @ 0f6593e1
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/sorted_list/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../sorted_list.mlw" verified="true" expanded="true">
<theory name="WP FindInSortedList" verified="true" expanded="true">
<goal name="Sorted_not_mem" sum="065ba337071029143930bed502bf4f54" proved="true" expanded="true" shape="amemV0aConsV1V2NIasortedaConsV1V2Iainfix <V0V1F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<why3session
name="examples/programs/sorted_list/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="yices"
name="Yices"
version="1.0.27"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../sorted_list.mlw"
verified="true"
expanded="true">
<theory
name="WP FindInSortedList"
verified="true"
expanded="true">
<goal
name="Sorted_not_mem"
sum="0e5b025f01157d802e4968ce08ccd4c4"
proved="true"
expanded="true"
shape="amemV0aConsV1V2NIasortedaConsV1V2Iainfix <V0V1F">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter find" expl="parameter find" sum="3088f11d3e64fa3492117d9f16ba16b0" proved="true" expanded="true" shape="CV1aNilamemV0V1qfaConsVVamemV0V1qainfix =V4aTrueAainfix >V0V2Oainfix =V0V2IamemV0V3qainfix =V4aTrueFAasortedV3IasortedV1FF">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<goal
name="WP_parameter find"
expl="parameter find"
sum="d06791b94cf6be238e76a7a9c8c63a80"
proved="true"
expanded="true"
shape="CV1aNilamemV0V1qfaConsVVamemV0V1qainfix =V4aTrueAainfix >V0V2Oainfix =V0V2IamemV0V3qainfix =V4aTrueFAasortedV3IasortedV1FF">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
......
modules/queue.mlw
View file @ 0f6593e1
......@@ -25,7 +25,7 @@ module Queue
| Cons x t -> result = x /\ q.elts = t end }
| Empty -> { q.elts = old q.elts = Nil }
val top:
val peek:
q: t 'a ->
{}
'a
......@@ -35,7 +35,7 @@ module Queue
val clear: q: t 'a -> {} unit writes q {q.elts = Nil }
val copy: q: t 'a -> {} t 'a { result = q }
val copy: q: t 'a -> {} t 'a reads q { result = q }
val is_empty:
q: t 'a -> {} bool reads q { result=True <-> q.elts = Nil }
......@@ -61,9 +61,9 @@ module Test
let test1 () =
let s = Queue.create () in
Queue.push 1 s;
let x = Queue.top s in assert { x = 1 };
let x = Queue.peek s in assert { x = 1 };
Queue.push 2 s;
let x = Queue.top s in assert { x = 1 };
let x = Queue.peek s in assert { x = 1 };
()
end
......
theories/list.why
View file @ 0f6593e1
......@@ -132,22 +132,31 @@ end
theory Sorted
use export List
use import int.Int
inductive sorted (l: list int) =
type t
predicate le t t
inductive sorted (l: list t) =
| Sorted_Nil:
sorted Nil
| Sorted_One:
forall x: int. sorted (Cons x Nil)
forall x: t. sorted (Cons x Nil)
| Sorted_Two:
forall x y: int, l: list int.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
forall x y: t, l: list t.
le x y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
use import Mem
lemma Sorted_mem:
forall x: int, l: list int.
(forall y: int. mem y l -> x <= y) /\ sorted l <-> sorted (Cons x l)
lemma sorted_mem:
forall x: t, l: list t.
(forall y: t. mem y l -> le x y) /\ sorted l <-> sorted (Cons x l)
end
theory SortedInt
use import int.Int
clone export Sorted with type t = int, predicate le = (<=)
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