test-claude.why 1.41 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
   goal Test1: 2+2 = 4
MARCHE Claude's avatar
MARCHE Claude committed
10 11 12

   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
   goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)

MARCHE Claude's avatar
MARCHE Claude committed
21
   goal Test7: 0 = 2 and 2 = 3 and 4 = 5 and 6 = 7
MARCHE Claude's avatar
MARCHE Claude committed
22

MARCHE Claude's avatar
MARCHE Claude committed
23
   goal Test8: 2+2=4 and 3+3=6
24

25 26 27 28
   axiom A : 1 = 2

   goal Test9: 2+2=5 and 3+3=8

MARCHE Claude's avatar
db  
MARCHE Claude committed
29 30
end

31 32 33 34 35 36 37 38 39 40
theory TestSplit

  logic aa int

  logic bb int

  goal G : aa 0 /\ bb 1 -> false

end

MARCHE Claude's avatar
db  
MARCHE Claude committed
41 42 43
theory TestDiv

   use import int.Int
MARCHE Claude's avatar
MARCHE Claude committed
44 45 46 47 48 49 50 51 52 53 54 55
   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
56 57
end

58 59 60 61 62 63 64 65 66 67
theory TestList

  use import int.Int
  use import list.List

  logic x : list int

(*
  goal Test1: 
     match x with 
MARCHE Claude's avatar
MARCHE Claude committed
68
     | Nil -> 1 = 0 and 2 = 3
69 70 71 72 73 74 75
     | Cons _ Nil -> 4 = 5 and 6 = 7
     | Cons _ _ -> 8 = 9 /\ 10 = 11
     end  
*)

end  

MARCHE Claude's avatar
MARCHE Claude committed
76

MARCHE Claude's avatar
db  
MARCHE Claude committed
77 78
theory TestReal

79
   use import real.Real
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82

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

83 84
   use import real.Abs

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

MARCHE Claude's avatar
db  
MARCHE Claude committed
87 88 89 90
end

theory TestFloat

91 92 93 94 95
   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
96 97
end

MARCHE Claude's avatar
MARCHE Claude committed
98

MARCHE Claude's avatar
MARCHE Claude committed
99