alt-ergo-models.why 2.11 KB
Newer Older
1

2
theory T
3 4 5

  use import int.Int

6 7
  goal g_no_lab : forall x:int. x >= 42 -> x + 3 <= 50

Andrei Paskevich's avatar
Andrei Paskevich committed
8
  goal g_lab0 : forall x "model:0":int. ("model:cond" x >= 42) ->
9 10
    ("model:concl" x + 3 <= 50)

Andrei Paskevich's avatar
Andrei Paskevich committed
11
  goal g_lab1 : forall x "model:1":int. ("model:cond" x >= 42) ->
12 13
    ("model:concl" x + 3 <= 50)

MARCHE Claude's avatar
MARCHE Claude committed
14
  constant g : int
15

MARCHE Claude's avatar
MARCHE Claude committed
16
  goal g2_lab : forall x "model:0":int. ("model:concl" g >= x)
17

18 19 20

end

21
theory ModelInt
22

23
use import int.Int
24

25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
goal test0 : forall x "model:0":int. not (0 < x < 1)

goal test1 : forall x "model:0":int. not (0 <= x <= 1)

use import int.EuclideanDivision

goal test2 : forall x "model:0":int. div x x = 1

goal test_overflow:
  forall x "model:0" y "model:0" :  int.
     0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535

goal test_overflow2:
  forall x "model:0" y "model:0" :  int.
     -2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535

predicate is_int16 (x:int) = -65536 <= x <= 65535

goal test_overflow_int16:
  forall x "model:0" y "model:0" :  int.
     is_int16 x /\ is_int16 y -> is_int16 (x + y)

goal test_overflow_int16_alt:
  forall x "model:0" y "model:0" :  int.
Andrei Paskevich's avatar
Andrei Paskevich committed
49
      -65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
50

51 52
goal test_overflow_int16_bis:
  forall x "model:0" y "model:0" :  int.
Andrei Paskevich's avatar
Andrei Paskevich committed
53
     is_int16 x /\ is_int16 y /\
MARCHE Claude's avatar
MARCHE Claude committed
54
     ("model:cond1" 0 <= x) /\ (x <= y) -> is_int16 (x + y)
55 56 57 58 59 60 61 62 63 64 65

predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647

goal test_overflow_int32:
  forall x "model:0" y "model:0" :  int.
     is_int32 x /\ is_int32 y -> is_int32 (x + y)

goal test_overflow_int32_bis:
  forall x "model:0" y "model:0" :  int.
     is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)

MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69
goal test_overflow_int32_bis_inline:
  forall x "model:0" y "model:0" :  int.
     -2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647

70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
end

theory ModelReal

use import real.Real

goal test1 : forall x "model:0":real. not (0.0 < x < 1.0)

goal test2 : forall x "model:0":real. x/x=1.0

end

theory ModelArray

use import map.Map

Andrei Paskevich's avatar
Andrei Paskevich committed
86
goal t1 : forall t "model:0" :map int int, i "model:0" : int.
87
   get (set t 0 42) i = get t i
88 89

end
90 91