Jennisys/examples/Set.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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

class Set {
  var elems: set[int]

  constructor Empty()
    ensures elems = {}

  constructor Singleton(t: int)
    ensures elems = {t}

  constructor Sum(p: int, q: int)
    ensures elems = {p + q}

  constructor Double(p: int, q: int)
    requires p != q
    ensures elems = {p q}

  constructor Triple(p: int, q: int, r: int)
    requires p != q && q != r && r != p
    ensures elems = {p q r}
}

model Set {
  var root: SetNode

  frame
    root

  invariant
    root = null ==> elems = {}
    root != null ==> elems = root.elems
}

class SetNode {
  var elems: set[int]

  constructor Init(t: int)
    ensures elems = {t}

  constructor Double(p: int, q: int)
    requires p != q
    ensures elems = {p q}

  constructor Triple(p: int, q: int, r: int)
    requires p != q && q != r && r != p
    ensures elems = {p q r}
}

model SetNode {
  var data: int
  var left: SetNode
  var right: SetNode

  frame 
    left * right

  invariant
    elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})
    left != null  ==> forall e :: e in left.elems ==> e < data
    right != null ==> forall e :: e in right.elems ==> e > data
}