diff options
author | 2011-07-11 13:52:58 -0700 | |
---|---|---|
committer | 2011-07-11 13:52:58 -0700 | |
commit | 776eb757b0e4b7b98ea9c7ca9bcee002eaf6bee2 (patch) | |
tree | ccc366f1ab563cd471c5560aab0a529801f62f8d /Jennisys/examples | |
parent | dbb1fbe420eddf778da724c5eec6549ce068c28d (diff) |
- added Set.jen example
- fixed implementation for sets
- generalized unification rules
- added command line options
- removed the "Exact" active pattern for strings (the same thing is already supported by F#)
- added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST
Diffstat (limited to 'Jennisys/examples')
-rw-r--r-- | Jennisys/examples/Set.jen | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen new file mode 100644 index 00000000..5626babb --- /dev/null +++ b/Jennisys/examples/Set.jen @@ -0,0 +1,53 @@ +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} +} + +model Set { + var root: SetNode + + frame + root * root.elems[*] + + 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} +} + +model SetNode { + var data: int + var left: SetNode + var right: SetNode + + frame + data * left * right + + invariant + left = null && right = null ==> elems = {data} + 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 +} |