blob: f9b17f7432e0fcadec6340f85e01da5b66446f8a (
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
|
interface NumberMethods {
method Double(p: int) returns (ret: int)
ensures ret = 2*p
method Sum(a: int, b: int) returns (ret: int)
ensures ret = a + b
method Min2(a: int, b: int) returns (ret: int)
ensures a < b ==> ret = a
ensures a >= b ==> ret = b
method Min22(a: int, b: int) returns (ret: int)
ensures ret in {a b}
ensures ret <= a && ret <= b
method Min3(a: int, b: int, c: int) returns (ret: int)
ensures ret in {a b c}
ensures ret <= a && ret <= b && ret <= c
method Min32(a: int, b: int, c: int) returns (ret: int)
ensures ret in {a b c}
ensures forall x :: x in {a b c} ==> ret <= x
method MinSum(a: int, b: int, c: int) returns (ret: int)
ensures ret in {a+b a+c b+c}
ensures ret <= a+b && ret <= b+c && ret <= a+c
method Min4(a: int, b: int, c: int, d: int) returns (ret: int)
ensures ret in {a b c d}
ensures forall x :: x in {a b c d} ==> ret <= x
method Abs(a: int) returns (ret: int)
ensures ret in {a (-a)} && ret >= 0
}
datamodel NumberMethods {
}
|
