Commit f1ce3da3 authored by MARCHE Claude's avatar MARCHE Claude

interp: more examples

parent c4bd1d01
......@@ -130,15 +130,23 @@ execute examples/same_fringe.mlw SameFringe.bench
# execute examples/same_fringe.mlw --exec SameFringe.test5
# fails: "let" are cloned as "val"
# execute examples/same_fringe.mlw --exec Test.test1
execute examples/vstte12_combinators.mlw Combinators.test_SKK
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
# fails: needs support for "val" without code (how to do it?)
# examples/vacid_0_sparse_array.mlw --exec Harness.bench
# fails: needs support for let rec
# examples/knuth_prime_numbers.mlw --exec PrimeNumbers.bench
execute examples/vstte10_max_sum.mlw TestCase.test_case
execute examples/verifythis_fm2012_LRS.mlw LCP_test.bench
# fails: assert failure on (regions = []) in Mlw_interp.to_program_value
# examples/verifythis_fm2012_LRS.mlw --exec SuffixArray_test.bench
# fails: needs support for Array.copy
# examples/verifythis_PrefixSumRec.mlw --exec PrefixSumRec.bench
# fails: assert failure in Mreg.merge
# examples/queens.mlw --exec NQueensBits.test8
# fails: assert failure in Mreg.merge
# examples/vstte10_queens.mlw --exec NQueens.test8
echo ""
echo "=== Checking drivers ==="
......
......@@ -164,7 +164,7 @@ end
(* 2. More realistic code with bitwise operations **************************)
(***
(***)
theory BitwiseArithmetic
......@@ -236,13 +236,13 @@ module NQueensBits
val min_elt (x: int) : int
requires { x <> 0 } ensures { result = min_elt (bits x) }
val col: ref solution (* solution under construction *)
val k : ref int (* current row in the current solution *)
val ghost col: ref solution (* solution under construction *)
val ghost k : ref int (* current row in the current solution *)
val sol: ref solutions (* all solutions *)
val s : ref int (* next slot for a solution = number of solutions *)
val ghost sol: ref solutions (* all solutions *)
val ghost s : ref int (* next slot for a solution = number of solutions *)
let rec t (a b c: int) variant { cardinal (bits a) } =
let rec t (a b c: int) variant { cardinal (bits a) }
requires { 0 <= !k /\ !k + cardinal (bits a) = n /\ !s >= 0 /\
(forall i: int. mem i (bits a) <->
(0<=i<n /\ forall j: int. 0 <= j < !k -> !col[j] <> i)) /\
......@@ -300,6 +300,11 @@ module NQueensBits
solution u <-> (exists i: int. 0 <= i < result /\ eq_sol u !sol[i]) }
= t (~(~0 << q)) 0 0
let test8 () requires { size=32 /\ n = 8 } =
s := 0; k := 0;
queens 8
end
***)
(***)
This diff is collapsed.
......@@ -180,6 +180,7 @@ module PrefixSumRec
(** {2 A simple test} *)
let test_harness () =
let a = make 8 0 in
(* needed for the precondition of compute_sums *)
......@@ -196,4 +197,23 @@ module PrefixSumRec
assert { a[6] = 16 };
assert { a[7] = 22 }
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = make 8 0 in
(* needed for the precondition of compute_sums *)
assert { power 2 3 = a.length };
a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
compute_sums a;
if a[0] <> 0 then raise BenchFailure;
if a[1] <> 3 then raise BenchFailure;
if a[2] <> 4 then raise BenchFailure;
if a[3] <> 11 then raise BenchFailure;
if a[4] <> 11 then raise BenchFailure;
if a[5] <> 15 then raise BenchFailure;
if a[6] <> 16 then raise BenchFailure;
if a[7] <> 22 then raise BenchFailure
end
......@@ -58,7 +58,9 @@ module TestCase
use import array.Array
use import array.ArraySum
let test_case () =
exception BenchFailure
let test_case () raises { BenchFailure -> true } =
let n = 10 in
let a = make n 0 in
a[0] <- 9;
......@@ -73,6 +75,9 @@ module TestCase
a[9] <- 6;
let (s, m) = max_sum a n in
assert { s = 45 };
assert { m = 10 }
assert { m = 10 };
(* bench of --exec *)
if s <> 45 then raise BenchFailure;
if m <> 10 then raise BenchFailure
end
......@@ -100,4 +100,15 @@ module NQueens
raises { Solution -> solution board n }
= bt_queens board n 0
exception BenchFailure
let test8 () raises { BenchFailure -> true } =
let a = Array.make 8 0 in
try
queens a 8;
raise BenchFailure
with Solution -> a
end
end
......@@ -7,14 +7,18 @@
version="0.95.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
id="3"
name="Coq"
version="8.4pl2"/>
<prover
id="3"
id="4"
name="Z3"
version="3.2"/>
<file
......@@ -124,7 +128,7 @@
<label
name="expl:VC for check_is_consistent"/>
<proof
prover="1"
prover="2"
timelimit="20"
memlimit="0"
obsolete="false"
......@@ -141,7 +145,7 @@
expanded="true"
shape="asolutionV1V2IasolutionV0V2Iaeq_boardV0V1V2Iainfix =alengthV0alengthV1F">
<proof
prover="2"
prover="3"
timelimit="20"
memlimit="0"
edited="vstte10_queens_NQueens_solution_eq_board_1.v"
......@@ -150,7 +154,7 @@
<result status="valid" time="1.31"/>
</proof>
<proof
prover="3"
prover="4"
timelimit="8"
memlimit="1000"
obsolete="false"
......@@ -170,7 +174,7 @@
<label
name="expl:VC for bt_queens"/>
<proof
prover="1"
prover="2"
timelimit="20"
memlimit="0"
obsolete="false"
......@@ -198,6 +202,26 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test8"
locfile="../vstte10_queens.mlw"
loclnum="106" loccnumb="6" loccnume="11"
expl="VC for test8"
sum="0bec3c08db525ae6261cf1b30528173a"
proved="true"
expanded="true"
shape="ainfix &gt;=c8c0">
<label
name="expl:VC for test8"/>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
</file>
</why3session>
......@@ -82,6 +82,16 @@ module Combinators
end
end
exception BenchFailure
constant i : term = App (App S K) K
let test_SKK () raises { BenchFailure -> true } =
let t = reduction (App i i) in
if t <> i then raise BenchFailure;
let t = reduction (App (App (App (App K K) K) K) K) in
if t <> K then raise BenchFailure
(* an irreducible term is a value *)
lemma reducible_or_value:
......
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