Source/Jennisys/examples/oopsla12/IntSet.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

interface IntSet {
  var elems: set[int]             

  constructor Singleton(x: int)
    elems := {x}

  constructor Dupleton(x: int, y: int)
    requires x != y
    elems := {x y}

  method Find(x: int) returns (ret: bool)
    ret := x in elems
}

datamodel IntSet {
  var data: int
  var left: IntSet
  var right: IntSet
  
  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 ==> data < e)
}