Source/Jennisys/examples/Simple.jen


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

interface Simple {
 var a: int
 
 method Inc(p: int)
   a := old(a) + p   
   
 method Init(n: int)
   a := n
   
 method Max(x: int, y: int)
   ensures x < y ==> a = y
   ensures x >= y ==> a = x
   
 
 method Max2(x: int, y: int)
   ensures a = x || a = y
   ensures forall t :: t in {x y} ==> a >= t
   
 method Max3__mod__(x: int, y: int)
   ensures a in {x y}
   ensures forall t :: t in {x y} ==> a >= t   
   
 method MaxAll__mod__(x: seq[int])
   ensures a in x
   ensures forall t :: t in x ==> a >= t
}

datamodel Simple {
 var c: int
 invariant a = c
}