new example sorted_list added to the nightly bench

parent b6a894c5
(* find a value in a sorted list *)
(* Find a value in a sorted list of integers *)
module M
module FindInSortedList
use import int.Int
use import list.Mem
use import list.Sorted
(* FIXME *)
lemma Nil_not_Cons : forall x:int, l:list int. Nil <> Cons x l
lemma Sorted_not_mem:
forall x y : int, l : list int.
x < y -> sorted (Cons y l) -> not mem x (Cons y l)
......@@ -25,6 +22,6 @@ end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/sorted_list"
compile-command: "unset LANG; make -C ../.. examples/programs/sorted_list.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/programs/sorted_list/why3session.xml">
<file name="../sorted_list.mlw" verified="true" expanded="true">
<theory name="WP FindInSortedList" verified="true" expanded="true">
<goal name="Sorted_not_mem" sum="5dcf03a0a17c4718b901c38b0a6f0223" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter find" expl="correctness of parameter find" sum="7627fe49ea6a4b3b1337ea365f8df02e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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