binary search added to the nightly bench

parent 4991a657
...@@ -158,7 +158,6 @@ why.conf ...@@ -158,7 +158,6 @@ why.conf
/examples/programs/vstte10_aqueue/ /examples/programs/vstte10_aqueue/
/examples/programs/insertion_sort_list/ /examples/programs/insertion_sort_list/
/examples/programs/mergesort_list/ /examples/programs/mergesort_list/
/examples/programs/binary_search/
/examples/programs/same_fringe/ /examples/programs/same_fringe/
/examples/programs/quicksort/ /examples/programs/quicksort/
/examples/programs/algo63/ /examples/programs/algo63/
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/binary_search/why3session.xml">
<file name="../binary_search.mlw" verified="true" expanded="true">
<theory name="M" verified="true" expanded="true">
<goal name="WP_parameter binary_search" expl="correctness of parameter binary_search" sum="19c8c227fa34ac77ac920a032e72d19f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
</theory>
</file>
</why3session>
...@@ -330,10 +330,11 @@ module M2 ...@@ -330,10 +330,11 @@ module M2
let old_next = !next in let old_next = !next in
let old_p = !p in let old_p = !p in
let q = ref null in let q = ref null in
label Init:
while !p <> null do while !p <> null do
invariant { is_list !next !p /\ is_list !next !q invariant { is_list !next !p /\ is_list !next !q
/\ sep_list_list !next !p !q /\ /\ sep_list_list !next !p !q /\
reverse (model (old !next) (old_p)) = reverse (model (at !next Init) (old_p)) =
(reverse (model !next !p)) ++ (model !next !q)} (reverse (model !next !p)) ++ (model !next !q)}
let tmp = get !next !p in let tmp = get !next !p in
let bak_next = !next in let bak_next = !next in
......
o pas de old dans les invariants
o e <- e o e <- e
o {| e with x1 = e1; ...; xn = en |} o {| e with x1 = e1; ...; xn = en |}
......
...@@ -1181,6 +1181,8 @@ and itriple gl env (p, e, q) = ...@@ -1181,6 +1181,8 @@ and itriple gl env (p, e, q) =
let rec ty_effect ef ty = match ty.ty_node with let rec ty_effect ef ty = match ty.ty_node with
| Ty.Tyvar _ -> | Ty.Tyvar _ ->
ef ef
| Ty.Tyapp (ts, _) when ts_equal ts ts_arrow ->
ef
| Ty.Tyapp (ts, tyl) -> | Ty.Tyapp (ts, tyl) ->
let mt = get_mtsymbol ts in let mt = get_mtsymbol ts in
let rl = regions_tyapp ts mt.mt_regions tyl in let rl = regions_tyapp ts mt.mt_regions tyl in
......
...@@ -46,20 +46,6 @@ let test_all_1 () = ...@@ -46,20 +46,6 @@ let test_all_1 () =
(!x >= 0 && not (!x = 0) || !x >= 1) (!x >= 0 && not (!x = 0) || !x >= 1)
{ result=True <-> !x>=1 } { result=True <-> !x>=1 }
(* from Cesar Munoz's CD3D *)
logic d : int
parameter vx : ref int
parameter vy : ref int
parameter sq : x:int -> {} int { result = x*x }
let test_cd3d () =
{ true }
if !vx=0 && !vy=0 && sq !vx + sq !vy < sq d then 1 else 2
{ result=1 -> !vx=0 and !vy=0 }
end end
(* (*
...@@ -70,6 +56,7 @@ End: ...@@ -70,6 +56,7 @@ End:
(*** (***
module TestArray module TestArray
......
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