Commit e7c044ae authored by MARCHE Claude's avatar MARCHE Claude

two more tests in execution bench

parent 7d58836e
......@@ -135,6 +135,8 @@ execute examples/same_fringe.mlw SameFringe.bench
execute examples/vstte12_combinators.mlw Combinators.test_SKK
execute examples/selection_sort.mlw SelectionSort.bench
execute examples/insertion_sort.mlw InsertionSort.bench
execute examples/quicksort.mlw Quicksort.bench
execute examples/conjugate.mlw Test.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 local let rec
......
......@@ -4,7 +4,7 @@
Author: Jean-Christophe Filliatre (CNRS)
A partition of an integer n is a wy of writing n as a sum of positive
A partition of an integer n is a way of writing n as a sum of positive
integers. For instance 7 = 3 + 2 + 2 + 1. Such a partition can be
displayed as a Ferrer diagram:
......@@ -94,6 +94,29 @@ module Conjugate
end
module Test
use import int.Int
use import array.Array
use import Conjugate
let test () ensures { result.length >= 4 } =
let a = make 5 0 in
a[0] <- 3; a[1] <- 2; a[2] <- 2; a[3] <- 1;
conjugate a
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = test () in
if a[0] <> 4 then raise BenchFailure;
if a[1] <> 3 then raise BenchFailure;
if a[2] <> 1 then raise BenchFailure;
if a[3] <> 0 then raise BenchFailure
end
(*
Original C code from SCHUR
......
This diff is collapsed.
......@@ -37,4 +37,31 @@ module Quicksort
ensures { sorted t /\ permut (old t) t }
quick_rec t 0 (length t - 1)
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
quicksort a;
a
let test2 () ensures { result.length = 8 } =
let a = make 8 0 in
a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
quicksort a;
a
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = test2 () in
if a[0] <> -5 then raise BenchFailure;
if a[1] <> 6 then raise BenchFailure;
if a[2] <> 17 then raise BenchFailure;
if a[3] <> 42 then raise BenchFailure;
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure
end
......@@ -138,6 +138,10 @@ Theorem WP_parameter_quick_rec : forall (t:Z) (t1:(@map.Map.map Z _ Z _))
Z _ Z _)), ((0%Z <= t)%Z /\ ((sorted_sub t5 o1 (r + 1%Z)%Z) /\
(map.MapPermut.permut_sub t4 t5 o1 (r + 1%Z)%Z))) -> ((sorted_sub t5 l
(r + 1%Z)%Z) /\ (map.MapPermut.permut_sub t1 t5 l (r + 1%Z)%Z)))))))).
(* Why3 intros t t1 l r (h1,(h2,h3)) h4 (h5,h6) v h7 m t2
(h8,(h9,(h10,(h11,(h12,h13))))) (h14,((h15,h16),(h17,h18))) t3
(h19,h20) o (h21,h22) t4 (h23,(h24,h25)) o1 (h26,h27) t5
(h28,(h29,h30)). *)
intros n t1 l r.
intros (_, (hl, hr)) hlr hl2 v hlr2.
intros m t2 (inv1, (inv2, (inv3, (inv4, inv5)))).
......@@ -291,4 +295,3 @@ apply permut_weakening with (m+1)%Z (r+1)%Z; auto.
omega.
Qed.
This diff is collapsed.
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