test-claude.why 1.26 KB
Newer Older
MARCHE Claude's avatar
db  
MARCHE Claude committed
1
theory TestInt
MARCHE Claude's avatar
MARCHE Claude committed
2 3 4

   use import int.Int

MARCHE Claude's avatar
MARCHE Claude committed
5 6
   goal Test0 : true

MARCHE Claude's avatar
MARCHE Claude committed
7
   goal Test0_5 : true -> false
MARCHE Claude's avatar
MARCHE Claude committed
8

MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12
   goal Test1: 2+2 = 4

   goal Test2: forall x:int. x*x >= 0

MARCHE Claude's avatar
MARCHE Claude committed
13
   goal Test3: 1<>0 
14 15 16 17 18

   goal Test4: 1=2 -> 3=4 

   goal Test5: forall x:int. x <> 0 -> x*x > 0

19 20 21
   goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)

   goal Test7: 0 = 1 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25

(*
   goal Test8: 3+3=7
*)
26

MARCHE Claude's avatar
db  
MARCHE Claude committed
27 28 29 30 31
end

theory TestDiv

   use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35 36 37 38 39 40 41 42 43
   use int.EuclideanDivision

   goal EDiv1: EuclideanDivision.div 1 2 = 0

   goal EDiv2: EuclideanDivision.div (-1) 2 = -1

   use int.ComputerDivision

   goal CDiv1: ComputerDivision.div 1 2 = 0

   goal CDiv2: ComputerDivision.div (-1) 2 = 0

MARCHE Claude's avatar
db  
MARCHE Claude committed
44 45
end

MARCHE Claude's avatar
MARCHE Claude committed
46

MARCHE Claude's avatar
db  
MARCHE Claude committed
47 48
theory TestReal

49
   use import real.Real
MARCHE Claude's avatar
MARCHE Claude committed
50 51 52

   goal Real1: forall x:real. x <> 0.0 -> x*x <> 0.0

53 54
   use import real.Abs

MARCHE Claude's avatar
MARCHE Claude committed
55
   goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
56

MARCHE Claude's avatar
db  
MARCHE Claude committed
57 58 59 60
end

theory TestFloat

61 62 63 64 65
   use import floating_point.Rounding
   use floating_point.Single

   lemma Round_single_01: Single.round NearestTiesToEven 0.1 = 0x0.199999Ap0

MARCHE Claude's avatar
MARCHE Claude committed
66 67
end

MARCHE Claude's avatar
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69

MARCHE Claude's avatar
MARCHE Claude committed
70 71 72 73 74 75 76
theory TestList

  use import int.Int
  use import list.List

  logic x : list int

MARCHE Claude's avatar
MARCHE Claude committed
77
(*
MARCHE Claude's avatar
MARCHE Claude committed
78 79 80 81 82 83
  goal Test1: 
     match x with 
     | Nil -> 1 = 0 /\ 2 = 3
     | Cons _ Nil -> 4 = 5 and 6 = 7
     | Cons _ _ -> 8 = 9 /\ 10 = 11
     end  
MARCHE Claude's avatar
MARCHE Claude committed
84
*)
MARCHE Claude's avatar
MARCHE Claude committed
85

MARCHE Claude's avatar
d  
MARCHE Claude committed
86
end