Commit 0ee8c94c authored by Andrei Paskevich's avatar Andrei Paskevich

Merge recent changes into the merged 'new_system'

parents a949118f 2a4fe549
# Why version
VERSION=0.86+git
VERSION=0.90+git
......@@ -191,8 +191,8 @@ goods examples/bts
goods examples/tests
goods examples/tests-provers
goods examples/check-builtin
goods examples/logic
goods examples
goods examples/logic
goods examples/foveoos11-cm
goods examples/hoare_logic
goods examples/vacid_0_binary_heaps "-L examples/vacid_0_binary_heaps"
......
......@@ -108,7 +108,7 @@
%BEGIN LATEX
\begin{LARGE}
%END LATEX
Version \whyversion{}, February 2016
Version \whyversion{}, Month? 2016
%BEGIN LATEX
\end{LARGE}
%END LATEX
......@@ -141,7 +141,7 @@ $^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
\bigskip
%END LATEX
\textcopyright 2010-2015 University Paris-Sud, CNRS, Inria
\textcopyright 2010-2016 University Paris-Sud, CNRS, Inria
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
......@@ -263,6 +263,21 @@ Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.
\chapter{Release Notes}
\section{Release Notes for version 0.90: syntax changes w.r.t. 0.87}
\begin{center}
\begin{tabular}{|c|c|}
\hline
0.87 & 0.90 \\
\hline
\texttt{'L:} & \texttt{label L in} \\
\texttt{at !x 'L} & \texttt{!x at L} \\
\verb|\|\texttt{ x. t} & \texttt{fun x -> t} \\
\texttt{type t model ...} & \texttt{type t = private ... } \\
\hline
\end{tabular}
\end{center}
\section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
The syntax of \whyml programs changed in release 0.80.
......
......@@ -2,31 +2,74 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="f062b1e05a91602624b37c4b34762555" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="49"/></proof>
<theory name="AddListRec" sum="f1b4c4e0923c97bb07f0497e41cca3dd" expanded="true">
<goal name="VC sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="VC sum.1" expl="1. postcondition">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sum.2" expl="2. variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC sum.3" expl="3. postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC sum.4" expl="4. postcondition">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC main" expl="VC for main">
<transf name="split_goal_wp">
<goal name="VC main.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="AddListImp" sum="7ac8c0163d88693d0911255c23bfb93d" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<theory name="AddListImp" sum="e8c88c18c52faab3c58cf2482eb150fd" expanded="true">
<goal name="VC sum" expl="VC for sum">
<transf name="split_goal_wp">
<goal name="VC sum.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="VC sum.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC sum.3" expl="3. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sum.4" expl="4. loop variant decrease">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC sum.5" expl="5. loop invariant preservation">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC sum.6" expl="6. loop variant decrease">
<proof prover="3"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="VC sum.7" expl="7. unreachable point">
<proof prover="3"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<goal name="VC main" expl="VC for main">
<transf name="split_goal_wp">
<goal name="VC main.1" expl="1. assertion">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main.2" expl="2. assertion">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
<?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="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="AddListRec" sum="d0925178b08b43ca97d60c4da19b85cc" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="1f63599ecd6b1d6b1c6113dfada8e75b" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -26,7 +26,8 @@ module Algo63
ensures { permut_sub (old a) a m (n+1) }
let v = a[i] in
a[i] <- a[j];
a[j] <- v
a[j] <- v;
assert { exchange (old a) a i j }
val random (m n: int) : int ensures { m <= result <= n }
......
This diff is collapsed.
<?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.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../algo63.mlw" expanded="true">
<theory name="Algo63" sum="194369664eddb4417ee380157f3a70d4" expanded="true">
<goal name="VC exchange" expl="VC for exchange">
<transf name="split_goal_wp">
<goal name="VC exchange.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC exchange.2" expl="2. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC exchange.3" expl="3. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC exchange.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC exchange.5" expl="5. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="30"/></proof>
</goal>
<goal name="VC exchange.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC exchange.7" expl="7. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
</transf>
</goal>
<goal name="VC partition_" expl="VC for partition_">
<transf name="split_goal_wp">
<goal name="VC partition_.1" expl="1. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="VC partition_.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="VC partition_.3" expl="3. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="VC partition_.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC partition_.5" expl="5. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC partition_.6" expl="6. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.03" steps="27"/></proof>
</goal>
<goal name="VC partition_.7" expl="7. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="VC partition_.8" expl="8. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC partition_.9" expl="9. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="VC partition_.10" expl="10. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC partition_.11" expl="11. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="VC partition_.12" expl="12. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="VC partition_.13" expl="13. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="VC partition_.14" expl="14. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="VC partition_.15" expl="15. variant decrease">
<proof prover="0"><result status="valid" time="0.04" steps="87"/></proof>
</goal>
<goal name="VC partition_.16" expl="16. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC partition_.17" expl="17. precondition">
<proof prover="0"><result status="valid" time="0.06" steps="128"/></proof>
</goal>
<goal name="VC partition_.18" expl="18. precondition">
<proof prover="0"><result status="valid" time="1.93" steps="780"/></proof>
</goal>
<goal name="VC partition_.19" expl="19. precondition">
<proof prover="2"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="VC partition_.20" expl="20. precondition">
<proof prover="0"><result status="valid" time="0.08" steps="129"/></proof>
</goal>
<goal name="VC partition_.21" expl="21. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="55"/></proof>
</goal>
<goal name="VC partition_.22" expl="22. postcondition">
<proof prover="0"><result status="valid" time="0.31" steps="588"/></proof>
</goal>
<goal name="VC partition_.23" expl="23. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="57"/></proof>
</goal>
<goal name="VC partition_.24" expl="24. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
</goal>
<goal name="VC partition_.25" expl="25. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="52"/></proof>
</goal>
<goal name="VC partition_.26" expl="26. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="142"/></proof>
</goal>
<goal name="VC partition_.27" expl="27. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="142"/></proof>
</goal>
<goal name="VC partition_.28" expl="28. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC partition_.29" expl="29. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC partition_.30" expl="30. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC partition_.31" expl="31. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC partition_.32" expl="32. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="0"/></proof>
</goal>
<goal name="VC partition_.33" expl="33. assertion">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC partition_.34" expl="34. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC partition_.35" expl="35. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="VC partition_.36" expl="36. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="39"/></proof>
</goal>
<goal name="VC partition_.37" expl="37. postcondition">
<proof prover="0"><result status="valid" time="0.22" steps="673"/></proof>
</goal>
<goal name="VC partition_.38" expl="38. postcondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="VC partition_.39" expl="39. postcondition">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="1.85"/></proof>
</goal>
<goal name="VC partition_.40" expl="40. postcondition">
<proof prover="1"><result status="valid" time="0.11"/></proof>
<proof prover="2"><result status="valid" time="0.79"/></proof>
</goal>
</transf>
</goal>
<goal name="VC partition" expl="VC for partition" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC partition.1" expl="1. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC partition.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC partition.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="VC partition.4" expl="4. postcondition" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="18.04" steps="455"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -10,13 +10,16 @@ module Bag
forall x: 'a. b1 x = b2 x
constant empty : bag 'a =
\ _. 0
fun _ -> 0
val empty () : bag 'a
ensures { result = empty }
function add (e: 'a) (b: bag 'a) : bag 'a =
\ x. if x = e then b x + 1 else b x
fun x -> if x = e then b x + 1 else b x
function remove (e: 'a) (b: bag 'a) : bag 'a =
\ x. if x = e then b x - 1 else b x
fun x -> if x = e then b x - 1 else b x
end
......@@ -25,7 +28,7 @@ module BagSpec
use import int.Int
use import Bag
type t 'a model {
type t 'a = private {
mutable size: int;
mutable contents: bag 'a;
}
......@@ -52,30 +55,34 @@ module ResizableArraySpec
use import map.Map
use map.Const
type rarray 'a model { mutable length: int; mutable data: map int 'a }
type rarray 'a = private { mutable length: int; mutable data: map int 'a }
function ([]) (r: rarray 'a) (i: int) : 'a = Map.get r.data i
function ([<-]) (r: rarray ~'a) (i: int) (v: 'a) : rarray 'a =
{ r with data = Map.set r.data i v }
val length (r: rarray ~'a) : int
val function ([<-]) (r: rarray 'a) (i: int) (v: 'a) : rarray 'a
ensures { result.length = r.length }
ensures { result.data = Map.set r.data i v }
(***
val length (r: rarray 'a) : int
ensures { result = r.length }
*)
val make (len: int) (dummy: ~'a) : rarray 'a
val make (len: int) (dummy: 'a) : rarray 'a
requires { 0 <= len }
ensures { result.length = len }
ensures { result.data = Const.const dummy }
val ([]) (r: rarray ~'a) (i: int) : 'a
val ([]) (r: rarray 'a) (i: int) : 'a
requires { 0 <= i < r.length }
ensures { result = r[i] }
val ([]<-) (r: rarray ~'a) (i: int) (v: 'a) : unit
val ([]<-) (r: rarray 'a) (i: int) (v: 'a) : unit
requires { 0 <= i < r.length }
writes { r.data }
ensures { r = (old r)[i <- v] }
val resize (r: rarray ~'a) (len: int) : unit
val resize (r: rarray 'a) (len: int) : unit
requires { 0 <= len }
writes { r.length, r.data }
ensures { r.length = len }
......@@ -94,24 +101,24 @@ module BagImpl
use null.Null
function numof (r: rarray (Null.t 'a)) (x: 'a) (l u: int) : int =
NumOf.numof (\i. (Map.get r.R.data i).Null.v = Null.Value x) l u
NumOf.numof (fun i -> (Map.get r.R.data i).Null.v = Null.Value x) l u
type t 'a = {
mutable size: int;
data: rarray (Null.t 'a);
mutable ghost contents: bag 'a;
}
invariant { 0 <= self.size = self.data.length }
invariant { forall i: int. 0 <= i < self.size ->
not (Null.is_null self.data[i]) }
invariant { forall x: 'a. self.contents x = numof self.data x 0 self.size }
invariant { 0 <= size = data.length }
invariant { forall i: int. 0 <= i < size ->
not (Null.is_null data[i]) }
invariant { forall x: 'a. contents x = numof data x 0 size }
let create () : t 'a
ensures { result.size = 0 }
ensures { result.contents == Bag.empty }
=
let null = Null.create_null () : Null.t 'a in
{ size = 0; data = make 0 null; contents = Bag.empty }
{ size = 0; data = make 0 null; contents = Bag.empty () }
let clear (t: t 'a) : unit
ensures { t.size = 0 }
......@@ -119,7 +126,7 @@ module BagImpl
=
resize t.data 0;
t.size <- 0;
t.contents <- Bag.empty
t.contents <- Bag.empty ()
let add (t: t 'a) (x: 'a) : unit
ensures { t.size = old t.size + 1 }
......
......@@ -88,6 +88,7 @@ end
module BinarySearchInt32
use import int.Int
use import mach.int.Int32
use import ref.Ref
use import mach.array.Array32
......
This diff is collapsed.
<?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.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="2f41cacfb96e90ff7c4f9a1031a4da0c" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
<goal name="VC binary_search.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="VC binary_search.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC binary_search.4" expl="4. assertion">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="VC binary_search.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC binary_search.6" expl="6. index in array bounds">
<proof prover="0"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="VC binary_search.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="VC binary_search.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.08" steps="50"/></proof>
</goal>
<goal name="VC binary_search.9" expl="9. loop variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC binary_search.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="VC binary_search.11" expl="11. exceptional postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="1c7344cbdd4fa3ee18d3bebf0c89856b" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="1. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
<goal name="VC binary_search.2" expl="2. loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC binary_search.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC binary_search.4" expl="4. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="VC binary_search.5" expl="5. index in array bounds">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC binary_search.6" expl="6. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
</goal>
<goal name="VC binary_search.7" expl="7. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC binary_search.8" expl="8. loop variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC binary_search.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC binary_search.10" expl="10. exceptional postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="badc1b8bf6577b29c30d0160c2ba5ef3" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="1. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="68"/></proof>
</goal>
<goal name="VC binary_search.2" expl="2. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="69"/></proof>
</goal>
<goal name="VC binary_search.3" expl="3. integer overflow">
<proof prover="0"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC binary_search.4" expl="4. loop invariant init">
<proof prover="0"><result status="valid" time="0.04" steps="70"/></proof>
</goal>
<goal name="VC binary_search.5" expl="5. loop invariant init">
<proof prover="0"><result status="valid" time="0.03" steps="73"/></proof>
</goal>
<goal name="VC binary_search.6" expl="6. integer overflow">
<proof prover="0"><result status="valid" time="0.03" steps="74"/></proof>
</goal>
<goal name="VC binary_search.7" expl="7. integer overflow">
<proof prover="0"><result status="valid" time="0.06" steps="125"/></proof>
</goal>
<goal name="VC binary_search.8" expl="8. division by zero">
<proof prover="0"><result status="valid" time="0.03" steps="75"/></proof>
</goal>
<goal name="VC binary_search.9" expl="9. integer overflow">
<proof prover="0"><result status="valid" time="0.21" steps="151"/></proof>
</goal>
<goal name="VC binary_search.10" expl="10. integer overflow">
<proof prover="0"><result status="valid" time="0.76" steps="425"/></proof>
</goal>
<goal name="VC binary_search.11" expl="11. assertion">
<proof prover="0"><result status="valid" time="0.11" steps="110"/></proof>
</goal>
<goal name="VC binary_search.12" expl="12. index in array bounds">
<proof prover="0"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="VC binary_search.13" expl="13. integer overflow">
<proof prover="0"><result status="valid" time="0.03" steps="81"/></proof>
</goal>
<goal name="VC binary_search.14" expl="14. integer overflow">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC binary_search.15" expl="15. index in array bounds">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
<goal name="VC binary_search.16" expl="16. integer overflow">
<proof prover="0"><result status="valid" time="0.03" steps="82"/></proof>
</goal>
<goal name="VC binary_search.17" expl="17. integer overflow">
<proof prover="0"><result status="valid" time="0.78" steps="205"/></proof>
</goal>
<goal name="VC binary_search.18" expl="18. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.21" steps="289"/></proof>
</goal>
<goal name="VC binary_search.19" expl="19. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC binary_search.20" expl="20. loop variant decrease">
<proof prover="0"><result status="valid" time="1.03" steps="1277"/></proof>
</goal>
<goal name="VC binary_search.21" expl="21. postcondition">
<proof prover="0"><result status="valid" time="0.04" steps="117"/></proof>
</goal>
<goal name="VC binary_search.22" expl="22. exceptional postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -4,38 +4,38 @@
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>