summaryrefslogtreecommitdiff
path: root/Source/Jennisys/examples/NumberMethods.jen
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 {

}