test-jcf.why 1.46 KB
 Jean-Christophe Filliâtre committed Feb 09, 2010 1 2 `````` `````` Jean-Christophe Filliatre committed Dec 13, 2010 3 ``````theory List `````` Jean-Christophe Filliâtre committed Oct 07, 2010 4 `````` `````` Jean-Christophe Filliatre committed Dec 13, 2010 5 `````` type list 'a = Nil | Cons 'a (list 'a) `````` Jean-Christophe Filliâtre committed Oct 26, 2010 6 `````` `````` Jean-Christophe Filliatre committed Dec 15, 2010 7 8 9 10 `````` use import bool.Bool logic x : int = if true then 1 else 3 `````` Jean-Christophe Filliatre committed Dec 13, 2010 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 ``````end theory Length use import int.Int use import List logic length (l : list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end lemma Length_nonnegative : forall l:list 'a. length(l) >= 0 end theory Sorted use import List use import int.Int inductive sorted (l : list int) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:int. sorted (Cons x Nil) | Sorted_Two : forall x y : int, l : list int. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end `````` Jean-Christophe Filliâtre committed Oct 26, 2010 42 `````` `````` Jean-Christophe Filliatre committed Dec 13, 2010 43 44 45 46 47 48 49 50 ``````theory Order type t logic (<=) t t axiom Le_refl : forall x : t. x <= x axiom Le_asym : forall x y : t. x <= y -> y <= x -> x = y axiom Le_trans: forall x y z : t. x <= y -> y <= z -> x <= z `````` Jean-Christophe Filliâtre committed Oct 07, 2010 51 `````` `````` Jean-Christophe Filliâtre committed May 28, 2010 52 53 ``````end `````` Jean-Christophe Filliatre committed Dec 13, 2010 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 ``````theory SortedGen use import List clone import Order as O inductive sorted (l : list t) = | Sorted_Nil : sorted Nil | Sorted_One : forall x:t. sorted (Cons x Nil) | Sorted_Two : forall x y : t, l : list t. x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l)) end theory SortedIntList use import int.Int clone SortedGen with type O.t = int, logic O.(<=) = (<=) end `````` Francois Bobot committed Mar 22, 2010 77 `````` `````` Jean-Christophe Filliâtre committed Feb 26, 2010 78 79 ``````(* Local Variables: `````` Jean-Christophe Filliâtre committed May 17, 2010 80 ``````compile-command: "cd ..; bin/why.opt -D drivers/simplify.drv tests/test-jcf.why && bin/why.opt -P simplify tests/test-jcf.why" `````` Jean-Christophe Filliâtre committed Feb 26, 2010 81 82 ``````End: *) `````` 83