test-jcf.why 1.46 KB
Newer Older
1 2


3
theory List
4

5
  type list 'a = Nil | Cons 'a (list 'a)
6

7 8 9 10
  use import bool.Bool

  logic x : int = if true then 1 else 3

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
42

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
51

52 53
end

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
77

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78 79
(*
Local Variables: 
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's avatar
Jean-Christophe Filliâtre committed
81 82
End: 
*)
83