Commit 44ccf071 authored by Andrei Paskevich's avatar Andrei Paskevich

stdlib/array: make array.Sorted compatible with strict orders

parent 862ded13
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/> <prover id="0" name="Alt-Ergo" version="2.0.0" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="11" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC3" version="2.4.1" timelimit="11" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
...@@ -196,7 +196,7 @@ ...@@ -196,7 +196,7 @@
<goal name="VC mergesort_rec" expl="VC for mergesort_rec" proved="true"> <goal name="VC mergesort_rec" expl="VC for mergesort_rec" proved="true">
<transf name="split_vc" proved="true" > <transf name="split_vc" proved="true" >
<goal name="VC mergesort_rec.0" expl="postcondition" proved="true"> <goal name="VC mergesort_rec.0" expl="postcondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="VC mergesort_rec.1" expl="postcondition" proved="true"> <goal name="VC mergesort_rec.1" expl="postcondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="13"/></proof>
...@@ -229,7 +229,7 @@ ...@@ -229,7 +229,7 @@
<proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="18"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="18"/></proof>
</goal> </goal>
<goal name="VC mergesort_rec.11" expl="precondition" proved="true"> <goal name="VC mergesort_rec.11" expl="precondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.15" steps="184"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="0.27" steps="308"/></proof>
</goal> </goal>
<goal name="VC mergesort_rec.12" expl="precondition" proved="true"> <goal name="VC mergesort_rec.12" expl="precondition" proved="true">
<proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="0" timelimit="5"><result status="valid" time="0.01" steps="22"/></proof>
...@@ -283,7 +283,7 @@ ...@@ -283,7 +283,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="53"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="53"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.11" expl="precondition" proved="true"> <goal name="VC bottom_up_mergesort.11" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="50"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="59"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.12" expl="precondition" proved="true"> <goal name="VC bottom_up_mergesort.12" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
...@@ -305,7 +305,7 @@ ...@@ -305,7 +305,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.17" expl="assertion" proved="true"> <goal name="VC bottom_up_mergesort.17" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.75" steps="490"/></proof> <proof prover="0"><result status="valid" time="0.75" steps="506"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.18" expl="assertion" proved="true"> <goal name="VC bottom_up_mergesort.18" expl="assertion" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
...@@ -319,7 +319,7 @@ ...@@ -319,7 +319,7 @@
<proof prover="0"><result status="valid" time="0.03" steps="42"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="42"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.18.3" expl="assertion" proved="true"> <goal name="VC bottom_up_mergesort.18.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="103"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="143"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.18.4" expl="assertion" proved="true"> <goal name="VC bottom_up_mergesort.18.4" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="27"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="27"/></proof>
...@@ -339,13 +339,13 @@ ...@@ -339,13 +339,13 @@
<proof prover="0"><result status="valid" time="0.01" steps="57"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="57"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.22" expl="loop invariant preservation" proved="true"> <goal name="VC bottom_up_mergesort.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof> <proof prover="0"><result status="valid" time="0.03" steps="72"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.23" expl="loop invariant preservation" proved="true"> <goal name="VC bottom_up_mergesort.23" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.24" expl="assertion" proved="true"> <goal name="VC bottom_up_mergesort.24" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.11" steps="177"/></proof> <proof prover="0"><result status="valid" time="0.11" steps="181"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.25" expl="loop variant decrease" proved="true"> <goal name="VC bottom_up_mergesort.25" expl="loop variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
...@@ -363,7 +363,7 @@ ...@@ -363,7 +363,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.30" expl="postcondition" proved="true"> <goal name="VC bottom_up_mergesort.30" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
</goal> </goal>
<goal name="VC bottom_up_mergesort.31" expl="postcondition" proved="true"> <goal name="VC bottom_up_mergesort.31" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
...@@ -373,12 +373,12 @@ ...@@ -373,12 +373,12 @@
</theory> </theory>
<theory name="NaturalMergesort" proved="true"> <theory name="NaturalMergesort" proved="true">
<goal name="VC find_run" expl="VC for find_run" proved="true"> <goal name="VC find_run" expl="VC for find_run" proved="true">
<proof prover="0"><result status="valid" time="0.13" steps="178"/></proof> <proof prover="0"><result status="valid" time="0.13" steps="167"/></proof>
</goal> </goal>
<goal name="VC natural_mergesort" expl="VC for natural_mergesort" proved="true"> <goal name="VC natural_mergesort" expl="VC for natural_mergesort" proved="true">
<transf name="split_goal_right" proved="true" > <transf name="split_goal_right" proved="true" >
<goal name="VC natural_mergesort.0" expl="postcondition" proved="true"> <goal name="VC natural_mergesort.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal> </goal>
<goal name="VC natural_mergesort.1" expl="postcondition" proved="true"> <goal name="VC natural_mergesort.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
...@@ -479,7 +479,7 @@ ...@@ -479,7 +479,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="37"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="37"/></proof>
</goal> </goal>
<goal name="VC natural_mergesort.30" expl="loop invariant preservation" proved="true"> <goal name="VC natural_mergesort.30" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="102"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="128"/></proof>
</goal> </goal>
<goal name="VC natural_mergesort.31" expl="loop invariant preservation" proved="true"> <goal name="VC natural_mergesort.31" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="39"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="39"/></proof>
...@@ -510,7 +510,7 @@ ...@@ -510,7 +510,7 @@
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof> <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal> </goal>
<goal name="VC naturalrec.1" expl="postcondition" proved="true"> <goal name="VC naturalrec.1" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal> </goal>
<goal name="VC naturalrec.2" expl="postcondition" proved="true"> <goal name="VC naturalrec.2" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
...@@ -565,7 +565,7 @@ ...@@ -565,7 +565,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="47"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="47"/></proof>
</goal> </goal>
<goal name="VC naturalrec.18" expl="precondition" proved="true"> <goal name="VC naturalrec.18" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="107"/></proof> <proof prover="0"><result status="valid" time="0.02" steps="136"/></proof>
</goal> </goal>
<goal name="VC naturalrec.19" expl="precondition" proved="true"> <goal name="VC naturalrec.19" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof> <proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5"> <why3session shape_version="6">
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="3" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file proved="true"> <file proved="true">
......
...@@ -168,12 +168,12 @@ module Sorted ...@@ -168,12 +168,12 @@ module Sorted
predicate le elt elt predicate le elt elt
predicate sorted_sub (a: array elt) (l u: int) = predicate sorted_sub (a: array elt) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2] forall i1 i2 : int. l <= i1 < i2 < u -> le a[i1] a[i2]
(** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)` (** `sorted_sub a l u` is true whenever the array segment `a(l..u-1)`
is sorted w.r.t order relation `le` *) is sorted w.r.t order relation `le` *)
predicate sorted (a: array elt) = predicate sorted (a: array elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2] forall i1 i2 : int. 0 <= i1 < i2 < length a -> le a[i1] a[i2]
(** `sorted a` is true whenever the array `a` is sorted w.r.t `le` *) (** `sorted a` is true whenever the array `a` is sorted w.r.t `le` *)
end 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