blob: e31613bdbe169b13ee75d6e32663b77395361ce8 (
plain)
1
2
3
4
5
6
7
8
9
10
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
42
43
44
|
interface Number {
var num: int
constructor Init(p: int)
ensures num = p
constructor Double(p: int)
ensures num = 2*p
constructor Sum(a: int, b: int)
ensures num = a + b
constructor Min2(a: int, b: int)
ensures a < b ==> num = a
ensures a >= b ==> num = b
constructor Min22(a: int, b: int)
ensures num in {a b}
ensures num <= a && num <= b
constructor Min3(a: int, b: int, c: int)
ensures num in {a b c}
ensures num <= a && num <= b && num <= c
constructor Min32(a: int, b: int, c: int)
ensures num in {a b c}
ensures forall x :: x in {a b c} ==> num <= x
constructor MinSum(a: int, b: int, c: int)
ensures num in {a+b a+c b+c}
ensures num <= a+b && num <= b+c && num <= a+c
constructor Min4(a: int, b: int, c: int, d: int)
ensures num in {a b c d}
ensures forall x :: x in {a b c d} ==> num <= x
constructor Abs(a: int)
ensures num in {a (-a)} && num >= 0
}
datamodel Number {
}
|
