diff options
| -rw-r--r-- | Jennisys/FixpointSolver.fs | 57 | ||||
| -rw-r--r-- | Jennisys/Options.fs | 2 | ||||
| -rw-r--r-- | Jennisys/PipelineUtils.fs | 3 | ||||
| -rw-r--r-- | Jennisys/examples/DList.jen | 24 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/BHeap.jen | 34 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/BHeap_synth.dfy | 220 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/DList.jen | 40 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/DList_synth.dfy | 154 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/IntSet.jen | 30 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/IntSet_synth.dfy | 130 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/List.jen | 29 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/List_synth.dfy | 146 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/Math.jen | 20 | ||||
| -rw-r--r-- | Jennisys/examples/oopsla12/Math_synth.dfy | 105 |
14 files changed, 942 insertions, 52 deletions
diff --git a/Jennisys/FixpointSolver.fs b/Jennisys/FixpointSolver.fs index b2ce1fac..1ca3b057 100644 --- a/Jennisys/FixpointSolver.fs +++ b/Jennisys/FixpointSolver.fs @@ -150,26 +150,26 @@ let rec ComputeClosure heapInst expandExprFunc premises = let FindMatches expr except premises =
//Logger.TraceLine ("finding matches for: " + (PrintExpr 0 expr) + "; #premises = " + (Set.count premises |> sprintf "%i"))
let okToUnifyFunc = fun (varName: string) -> varName.StartsWith("$")
- let matches =
- premises |> Set.toList
- |> List.choose (function BinaryExpr(_,"=",lhs,rhs) ->
- if lhs = expr && not (rhs = except) then
- Some(rhs)
- elif rhs = expr && not (lhs = except) then
- Some(lhs)
- else
- if expr = TrueLiteral then
- None
- else
- match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with
- | Some(unifs) -> Some(ApplyUnifs unifs rhs)
- | None ->
- match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with
- | Some(unifs) -> Some(ApplyUnifs unifs lhs)
- | None -> None
- | _ -> None)
- //Logger.TraceLine (sprintf "Number of matches for %s: %i" (PrintExpr 0 expr) (List.length matches))
- matches
+ if expr = TrueLiteral then
+ []
+ else
+ let matches =
+ premises |> Set.toList
+ |> List.choose (function BinaryExpr(_,"=",lhs,rhs) ->
+ if lhs = expr && not (rhs = except) then
+ Some(rhs)
+ elif rhs = expr && not (lhs = except) then
+ Some(lhs)
+ else
+ match SelectiveUnifyImplies okToUnifyFunc lhs expr LTR Map.empty with
+ | Some(unifs) -> Some(ApplyUnifs unifs rhs)
+ | None ->
+ match SelectiveUnifyImplies okToUnifyFunc rhs expr LTR Map.empty with
+ | Some(unifs) -> Some(ApplyUnifs unifs lhs)
+ | None -> None
+ | _ -> None)
+ //Logger.TraceLine (sprintf "Number of matches for %s: %i" (PrintExpr 0 expr) (List.length matches))
+ matches
let MySetAdd expr set =
let x = Printer.PrintExpr 0 expr
@@ -216,7 +216,7 @@ let rec ComputeClosure heapInst expandExprFunc premises = let BinaryInCombiner lhs rhs =
// distribute the "in" operation if possible
- let __fff lhs rhs =
+ let rec __fff lhs rhs =
//Logger.TraceLine ("In fff for " + (PrintExpr 0 lhs) + " and " + (PrintExpr 0 rhs))
let binInExpr = BinaryIn lhs rhs
// match rhs with
@@ -244,7 +244,8 @@ let rec ComputeClosure heapInst expandExprFunc premises = | BoolLiteral(true) -> [opt1]
| _ -> match EvalFull heapInst opt2 with
| BoolLiteral(true) -> [opt2]
- | _ -> [BinaryOr (BinaryIn lhs l)(BinaryIn lhs r)]
+ | _ -> Utils.ListCombine BinaryOr (__fff lhs l) (__fff lhs r)
+ //[BinaryOr (BinaryIn lhs l)(BinaryIn lhs r)]
| SequenceExpr(elist) ->
let len = elist |> List.length
if len = 0 then
@@ -256,8 +257,9 @@ let rec ComputeClosure heapInst expandExprFunc premises = let lst0Val = EvalFull heapInst elist.[0]
if lhsVal = lst0Val then
[BinaryEq lhs elist.[0]]
- else
- [BinaryIn lhs (SequenceExpr(elist |> List.tail))]
+ else
+ __fff lhs (SequenceExpr(elist |> List.tail))
+ //[BinaryIn lhs (SequenceExpr(elist |> List.tail))]
| SetExpr(elist) ->
let evalElist = elist |> List.map (EvalFull heapInst)
let evalLhs = EvalFull heapInst lhs
@@ -296,7 +298,8 @@ let rec ComputeClosure heapInst expandExprFunc premises = let lhsVal = EvalFull heapInst lhs
let lst0Val = EvalFull heapInst elist.[0]
[BinaryNeq lhs elist.[0]] @
- [BinaryNotIn lhs (SequenceExpr(elist |> List.tail))]
+ __fff lhs (SequenceExpr(elist |> List.tail))
+ //[BinaryNotIn lhs (SequenceExpr(elist |> List.tail))]
| _ -> [binNotInExpr]
__fff lhs rhs
@@ -358,8 +361,8 @@ let rec ComputeClosure heapInst expandExprFunc premises = // TODO: iterate only 3 times, instead of to full closure
let p1 = iterOnceFunc premises
let p2 = p1 |> iterOnceFunc
- let p3 = p2 |> iterOnceFunc
- p3
+ //let p3 = p2 |> iterOnceFunc
+ p2
// let premises' = iterOnceFunc premises
// if premises' = premises then
// premises'
diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs index 41ad91e5..fe640f48 100644 --- a/Jennisys/Options.fs +++ b/Jennisys/Options.fs @@ -110,7 +110,7 @@ let defaultConfig: Config = { verifySolutions = true;
checkUnifications = false;
genRepr = true;
- genMod = true;
+ genMod = false;
timeout = 0;
numLoopUnrolls = 2;
recursiveValid = true;
diff --git a/Jennisys/PipelineUtils.fs b/Jennisys/PipelineUtils.fs index 7d0b3e55..a87d442f 100644 --- a/Jennisys/PipelineUtils.fs +++ b/Jennisys/PipelineUtils.fs @@ -7,6 +7,8 @@ module PipelineUtils
+open Logger
+
let dafnyScratchSuffix = "scratch"
let dafnyVerifySuffix = "verify"
let dafnyUnifSuffix = "unif"
@@ -24,6 +26,7 @@ let CreateEmptyModelFile modelFile = /// the resulting model to the given "modelFile"
// =======================================================
let RunDafny inputFile modelFile =
+ //TraceLine "\n@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Running Dafny @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@"
CreateEmptyModelFile modelFile
async {
use proc = new System.Diagnostics.Process()
diff --git a/Jennisys/examples/DList.jen b/Jennisys/examples/DList.jen index 47c74dc1..43337ca8 100644 --- a/Jennisys/examples/DList.jen +++ b/Jennisys/examples/DList.jen @@ -1,27 +1,3 @@ -interface DList[T] {
- var list: seq[T]
-
- constructor Empty()
- ensures list = []
-
- constructor Singleton(t: T)
- ensures list = [t]
-
- constructor Double(p: T, q: T)
- ensures list = [p q]
-}
-
-datamodel DList[T] {
- var root: DNode[T]
-
- frame
- root
-
- invariant
- root = null ==> |list| = 0
- root != null ==> list = root.list
-}
-
interface DNode[T] {
var list: seq[T]
diff --git a/Jennisys/examples/oopsla12/BHeap.jen b/Jennisys/examples/oopsla12/BHeap.jen new file mode 100644 index 00000000..41ebec85 --- /dev/null +++ b/Jennisys/examples/oopsla12/BHeap.jen @@ -0,0 +1,34 @@ +interface BHeap {
+ var elems: set[int]
+
+ constructor Singleton(x: int)
+ elems := {x}
+
+ constructor Dupleton(a: int, b: int)
+ requires a != b
+ elems := {a b}
+
+ constructor Tripleton(x: int, y: int, z: int)
+ requires x != y && y != z && z != x
+ elems := {x y z}
+
+ method Find(n: int) returns (ret: bool)
+ ret := n in elems
+}
+
+datamodel BHeap {
+ var data: int
+ var left: BHeap
+ var right: BHeap
+
+ 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
+ left = null ==> right = null
+ left != null && right = null ==> left.elems = {left.data}
+}
\ No newline at end of file diff --git a/Jennisys/examples/oopsla12/BHeap_synth.dfy b/Jennisys/examples/oopsla12/BHeap_synth.dfy new file mode 100644 index 00000000..addba4ae --- /dev/null +++ b/Jennisys/examples/oopsla12/BHeap_synth.dfy @@ -0,0 +1,220 @@ +class BHeap {
+ ghost var Repr: set<object>;
+ ghost var elems: set<int>;
+
+ var data: int;
+ var left: BHeap;
+ var right: BHeap;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&
+ (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&
+ (left != null ==> (forall e :: e in left.elems ==> e < data)) &&
+ (right != null ==> (forall e :: e in right.elems ==> e < data)) &&
+ (left == null ==> right == null) &&
+ (left != null && right == null ==> left.elems == {left.data})
+ }
+
+ function Valid(): bool
+ reads *;
+ decreases Repr;
+ {
+ this.Valid_self() &&
+ (left != null ==> left.Valid()) &&
+ (right != null ==> right.Valid()) &&
+ (left != null ==> left.Valid_self()) &&
+ (right != null ==> right.Valid_self()) &&
+ (left != null && left.left != null ==> left.left.Valid_self()) &&
+ (left != null && left.right != null ==> left.right.Valid_self()) &&
+ (right != null && right.left != null ==> right.left.Valid_self()) &&
+ (right != null && right.right != null ==> right.right.Valid_self())
+ }
+
+
+ method Dupleton(a: int, b: int)
+ modifies this;
+ requires a != b;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {a, b};
+ {
+ if (b < a) {
+ var gensym71 := new BHeap;
+ var gensym73 := new BHeap;
+ this.data := a;
+ this.elems := {b, a};
+ this.left := gensym73;
+ this.right := gensym71;
+ gensym71.data := b;
+ gensym71.elems := {b};
+ gensym71.left := null;
+ gensym71.right := null;
+ gensym73.data := b;
+ gensym73.elems := {b};
+ gensym73.left := null;
+ gensym73.right := null;
+
+ // repr stuff
+ gensym71.Repr := {gensym71};
+ gensym73.Repr := {gensym73};
+ this.Repr := ({this} + {gensym73}) + {gensym71};
+ // assert repr objects are valid (helps verification)
+ assert gensym71.Valid() && gensym73.Valid();
+ } else {
+ var gensym71 := new BHeap;
+ var gensym73 := new BHeap;
+ this.data := b;
+ this.elems := {a, b};
+ this.left := gensym73;
+ this.right := gensym71;
+ gensym71.data := a;
+ gensym71.elems := {a};
+ gensym71.left := null;
+ gensym71.right := null;
+ gensym73.data := a;
+ gensym73.elems := {a};
+ gensym73.left := null;
+ gensym73.right := null;
+
+ // repr stuff
+ gensym71.Repr := {gensym71};
+ gensym73.Repr := {gensym73};
+ this.Repr := ({this} + {gensym73}) + {gensym71};
+ // assert repr objects are valid (helps verification)
+ assert gensym71.Valid() && gensym73.Valid();
+ }
+ }
+
+
+ method Find(n: int) returns (ret: bool)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == (n in elems);
+ decreases Repr;
+ {
+ if (this.left == null) {
+ ret := n == this.data;
+ } else {
+ if (this.right != null) {
+ var x_10 := this.left.Find(n);
+ var x_11 := this.right.Find(n);
+ ret := (n == this.data || x_10) || x_11;
+ } else {
+ var x_12 := this.left.Find(n);
+ ret := n == this.data || x_12;
+ }
+ }
+ }
+
+
+ method Singleton(x: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x};
+ {
+ this.data := x;
+ this.elems := {x};
+ this.left := null;
+ this.right := null;
+
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Tripleton(x: int, y: int, z: int)
+ modifies this;
+ requires x != y;
+ requires y != z;
+ requires z != x;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x, y, z};
+ {
+ if (z < y && x < y) {
+ var gensym75 := new BHeap;
+ var gensym77 := new BHeap;
+ this.data := y;
+ this.elems := {z, x, y};
+ this.left := gensym77;
+ this.right := gensym75;
+ gensym75.data := x;
+ gensym75.elems := {x};
+ gensym75.left := null;
+ gensym75.right := null;
+ gensym77.data := z;
+ gensym77.elems := {z};
+ gensym77.left := null;
+ gensym77.right := null;
+
+ // repr stuff
+ gensym75.Repr := {gensym75};
+ gensym77.Repr := {gensym77};
+ this.Repr := ({this} + {gensym77}) + {gensym75};
+ // assert repr objects are valid (helps verification)
+ assert gensym75.Valid() && gensym77.Valid();
+ } else {
+ if (x < z) {
+ var gensym75 := new BHeap;
+ var gensym77 := new BHeap;
+ this.data := z;
+ this.elems := {x, y, z};
+ this.left := gensym77;
+ this.right := gensym75;
+ gensym75.data := x;
+ gensym75.elems := {x};
+ gensym75.left := null;
+ gensym75.right := null;
+ gensym77.data := y;
+ gensym77.elems := {y};
+ gensym77.left := null;
+ gensym77.right := null;
+
+ // repr stuff
+ gensym75.Repr := {gensym75};
+ gensym77.Repr := {gensym77};
+ this.Repr := ({this} + {gensym77}) + {gensym75};
+ // assert repr objects are valid (helps verification)
+ assert gensym75.Valid() && gensym77.Valid();
+ } else {
+ var gensym75 := new BHeap;
+ var gensym77 := new BHeap;
+ this.data := x;
+ this.elems := {z, y, x};
+ this.left := gensym77;
+ this.right := gensym75;
+ gensym75.data := y;
+ gensym75.elems := {y};
+ gensym75.left := null;
+ gensym75.right := null;
+ gensym77.data := z;
+ gensym77.elems := {z};
+ gensym77.left := null;
+ gensym77.right := null;
+
+ // repr stuff
+ gensym75.Repr := {gensym75};
+ gensym77.Repr := {gensym77};
+ this.Repr := ({this} + {gensym77}) + {gensym75};
+ // assert repr objects are valid (helps verification)
+ assert gensym75.Valid() && gensym77.Valid();
+ }
+ }
+ }
+
+}
+
+
diff --git a/Jennisys/examples/oopsla12/DList.jen b/Jennisys/examples/oopsla12/DList.jen new file mode 100644 index 00000000..7e087f95 --- /dev/null +++ b/Jennisys/examples/oopsla12/DList.jen @@ -0,0 +1,40 @@ +interface DList[T] {
+ var list: seq[T]
+
+ invariant
+ |list| > 0
+
+ constructor Init(t: T)
+ list := [t]
+
+ constructor Double(p: T, q: T)
+ list := [p q]
+
+ method List() returns (ret: seq[T])
+ ret := list
+
+ method Size() returns (ret: int)
+ ret := |list|
+
+ method Get(idx: int) returns (ret: T)
+ requires 0 <= idx && idx < |list|
+ ret := list[idx]
+
+ method Find(n: T) returns (ret: bool)
+ ret := n in list
+}
+
+datamodel DList[T] {
+ var data: T
+ var next: DList[T]
+ var prev: DList[T]
+
+ frame
+ next
+
+ invariant
+ next = null ==> list = [data]
+ next != null ==> (list = [data] + next.list
+ && next.prev = this)
+ prev != null ==> prev.next = this
+}
\ No newline at end of file diff --git a/Jennisys/examples/oopsla12/DList_synth.dfy b/Jennisys/examples/oopsla12/DList_synth.dfy new file mode 100644 index 00000000..897a6de0 --- /dev/null +++ b/Jennisys/examples/oopsla12/DList_synth.dfy @@ -0,0 +1,154 @@ +class DList<T> {
+ ghost var Repr: set<object>;
+ ghost var list: seq<T>;
+
+ var data: T;
+ var next: DList<T>;
+ var prev: DList<T>;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&
+ (next != null ==> list == [data] + next.list && next.prev == this) &&
+ (prev != null ==> prev.next == this) &&
+ (|list| > 0)
+ }
+
+ function Valid(): bool
+ reads *;
+ decreases Repr;
+ {
+ this.Valid_self() &&
+ (next != null ==> next.Valid()) &&
+ (next != null ==> next.Valid_self()) &&
+ (next != null && next.next != null ==> next.next.Valid_self())
+ }
+
+
+ method Double(p: T, q: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p, q];
+ ensures list[0] == p;
+ ensures list[1] == q;
+ ensures |list| == 2;
+ {
+ var gensym71 := new DList<T>;
+ this.data := p;
+ this.list := [p, q];
+ this.next := gensym71;
+ this.prev := null;
+ gensym71.data := q;
+ gensym71.list := [q];
+ gensym71.next := null;
+ gensym71.prev := this;
+
+ // repr stuff
+ this.Repr := {this} + {gensym71};
+ gensym71.Repr := {gensym71};
+ // assert repr objects are valid (helps verification)
+ assert gensym71.Valid();
+ }
+
+
+ method Find(n: T) returns (ret: bool)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == (n in list);
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := n == this.data;
+ } else {
+ var x_5 := this.next.Find(n);
+ ret := n == this.data || x_5;
+ }
+ }
+
+
+ method Get(idx: int) returns (ret: T)
+ requires Valid();
+ requires 0 <= idx;
+ requires idx < |list|;
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == list[idx];
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := this.data;
+ } else {
+ if (idx == 0) {
+ ret := this.data;
+ } else {
+ var x_6 := this.next.Get(idx - 1);
+ ret := x_6;
+ }
+ }
+ }
+
+
+ method Init(t: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [t];
+ ensures list[0] == t;
+ ensures |list| == 1;
+ {
+ this.data := t;
+ this.list := [t];
+ this.next := null;
+ this.prev := null;
+
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method List() returns (ret: seq<T>)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == list;
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := [this.data];
+ } else {
+ var x_7 := this.next.List();
+ ret := [this.data] + x_7;
+ }
+ }
+
+
+ method Size() returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == |list|;
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := 1;
+ } else {
+ var x_8 := this.next.Size();
+ ret := 1 + x_8;
+ }
+ }
+
+}
+
+
diff --git a/Jennisys/examples/oopsla12/IntSet.jen b/Jennisys/examples/oopsla12/IntSet.jen new file mode 100644 index 00000000..4800371e --- /dev/null +++ b/Jennisys/examples/oopsla12/IntSet.jen @@ -0,0 +1,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)
+}
\ No newline at end of file diff --git a/Jennisys/examples/oopsla12/IntSet_synth.dfy b/Jennisys/examples/oopsla12/IntSet_synth.dfy new file mode 100644 index 00000000..55523e79 --- /dev/null +++ b/Jennisys/examples/oopsla12/IntSet_synth.dfy @@ -0,0 +1,130 @@ +class IntSet {
+ ghost var Repr: set<object>;
+ ghost var elems: set<int>;
+
+ var data: int;
+ var left: IntSet;
+ var right: IntSet;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (left != null ==> left in Repr && left.Repr <= Repr && this !in left.Repr) &&
+ (right != null ==> right in Repr && right.Repr <= Repr && this !in right.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (elems == ({data} + (if left != null then left.elems else {})) + (if right != null then right.elems else {})) &&
+ (left != null ==> (forall e :: e in left.elems ==> e < data)) &&
+ (right != null ==> (forall e :: e in right.elems ==> data < e))
+ }
+
+ function Valid(): bool
+ reads *;
+ decreases Repr;
+ {
+ this.Valid_self() &&
+ (left != null ==> left.Valid()) &&
+ (right != null ==> right.Valid()) &&
+ (left != null ==> left.Valid_self()) &&
+ (right != null ==> right.Valid_self()) &&
+ (left != null && left.left != null ==> left.left.Valid_self()) &&
+ (left != null && left.right != null ==> left.right.Valid_self()) &&
+ (right != null && right.left != null ==> right.left.Valid_self()) &&
+ (right != null && right.right != null ==> right.right.Valid_self())
+ }
+
+
+ method Dupleton(x: int, y: int)
+ modifies this;
+ requires x != y;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x, y};
+ {
+ if (x < y) {
+ var gensym73 := new IntSet;
+ this.data := x;
+ this.elems := {x, y};
+ this.left := null;
+ this.right := gensym73;
+ gensym73.data := y;
+ gensym73.elems := {y};
+ gensym73.left := null;
+ gensym73.right := null;
+
+ // repr stuff
+ gensym73.Repr := {gensym73};
+ this.Repr := {this} + {gensym73};
+ // assert repr objects are valid (helps verification)
+ assert gensym73.Valid();
+ } else {
+ var gensym73 := new IntSet;
+ this.data := y;
+ this.elems := {y, x};
+ this.left := null;
+ this.right := gensym73;
+ gensym73.data := x;
+ gensym73.elems := {x};
+ gensym73.left := null;
+ gensym73.right := null;
+
+ // repr stuff
+ gensym73.Repr := {gensym73};
+ this.Repr := {this} + {gensym73};
+ // assert repr objects are valid (helps verification)
+ assert gensym73.Valid();
+ }
+ }
+
+
+ method Find(x: int) returns (ret: bool)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == (x in elems);
+ decreases Repr;
+ {
+ if (this.left != null && this.right != null) {
+ var x_13 := this.left.Find(x);
+ var x_14 := this.right.Find(x);
+ ret := (x == this.data || x_13) || x_14;
+ } else {
+ if (this.left != null) {
+ var x_15 := this.left.Find(x);
+ ret := x == this.data || x_15;
+ } else {
+ if (this.right != null) {
+ var x_16 := this.right.Find(x);
+ ret := x == this.data || x_16;
+ } else {
+ ret := x == this.data;
+ }
+ }
+ }
+ }
+
+
+ method Singleton(x: int)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures elems == {x};
+ {
+ this.data := x;
+ this.elems := {x};
+ this.left := null;
+ this.right := null;
+
+ // repr stuff
+ this.Repr := {this};
+ }
+
+}
+
+
diff --git a/Jennisys/examples/oopsla12/List.jen b/Jennisys/examples/oopsla12/List.jen new file mode 100644 index 00000000..10a70050 --- /dev/null +++ b/Jennisys/examples/oopsla12/List.jen @@ -0,0 +1,29 @@ +interface List[T] {
+ var list: seq[T]
+ invariant |list| > 0
+
+ constructor Singleton(t: T)
+ list := [t]
+ constructor Dupleton(p: T, q: T)
+ list := [p q]
+ method Elems() returns (ret: seq[T])
+ ret := list
+ method Get(idx: int) returns (ret: T)
+ requires 0 <= idx && idx < |list|
+ ret := list[idx]
+ method Find(n: T) returns (ret: bool)
+ ret := n in list
+ method Size() returns (ret: int)
+ ret := |list|
+}
+
+datamodel List[T] {
+ var data: T
+ var next: List[T]
+
+ frame next
+
+ invariant
+ next = null ==> list = [data]
+ next != null ==> list = [data] + next.list
+}
\ No newline at end of file diff --git a/Jennisys/examples/oopsla12/List_synth.dfy b/Jennisys/examples/oopsla12/List_synth.dfy new file mode 100644 index 00000000..5cbfa10e --- /dev/null +++ b/Jennisys/examples/oopsla12/List_synth.dfy @@ -0,0 +1,146 @@ +class List<T> {
+ ghost var Repr: set<object>;
+ ghost var list: seq<T>;
+
+ var data: T;
+ var next: List<T>;
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr &&
+ (next != null ==> next in Repr && next.Repr <= Repr && this !in next.Repr)
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ (next == null ==> (list == [data] && list[0] == data) && |list| == 1) &&
+ (next != null ==> list == [data] + next.list) &&
+ (|list| > 0)
+ }
+
+ function Valid(): bool
+ reads *;
+ decreases Repr;
+ {
+ this.Valid_self() &&
+ (next != null ==> next.Valid()) &&
+ (next != null ==> next.Valid_self()) &&
+ (next != null && next.next != null ==> next.next.Valid_self())
+ }
+
+
+ method Dupleton(p: T, q: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [p, q];
+ ensures list[0] == p;
+ ensures list[1] == q;
+ ensures |list| == 2;
+ {
+ var gensym71 := new List<T>;
+ gensym71.Singleton(q);
+ this.data := p;
+ this.list := [p, q];
+ this.next := gensym71;
+
+ // repr stuff
+ this.Repr := {this} + this.next.Repr;
+ // assert repr objects are valid (helps verification)
+ assert gensym71.Valid();
+ }
+
+
+ method Elems() returns (ret: seq<T>)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == list;
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := [this.data];
+ } else {
+ var x_5 := this.next.Elems();
+ ret := [this.data] + x_5;
+ }
+ }
+
+
+ method Find(n: T) returns (ret: bool)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == (n in list);
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := n == this.data;
+ } else {
+ var x_6 := this.next.Find(n);
+ ret := n == this.data || x_6;
+ }
+ }
+
+
+ method Get(idx: int) returns (ret: T)
+ requires Valid();
+ requires 0 <= idx;
+ requires idx < |list|;
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == list[idx];
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := this.data;
+ } else {
+ if (idx == 0) {
+ ret := this.data;
+ } else {
+ var x_7 := this.next.Get(idx - 1);
+ ret := x_7;
+ }
+ }
+ }
+
+
+ method Singleton(t: T)
+ modifies this;
+ ensures fresh(Repr - {this});
+ ensures Valid();
+ ensures list == [t];
+ ensures list[0] == t;
+ ensures |list| == 1;
+ {
+ this.data := t;
+ this.list := [t];
+ this.next := null;
+
+ // repr stuff
+ this.Repr := {this};
+ }
+
+
+ method Size() returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret == |list|;
+ decreases Repr;
+ {
+ if (this.next == null) {
+ ret := 1;
+ } else {
+ var x_8 := this.next.Size();
+ ret := 1 + x_8;
+ }
+ }
+
+}
+
+
diff --git a/Jennisys/examples/oopsla12/Math.jen b/Jennisys/examples/oopsla12/Math.jen new file mode 100644 index 00000000..0cc772b3 --- /dev/null +++ b/Jennisys/examples/oopsla12/Math.jen @@ -0,0 +1,20 @@ +interface Math {
+ method Min2(a: int, b: int) returns (ret: int)
+ ensures a < b ==> ret = a
+ ensures a >= b ==> ret = b
+
+ method Min3Sum(a: int, b: int, c: int)
+ returns (ret: int)
+ ensures ret in {a+b a+c b+c}
+ ensures forall x :: x in {a+b a+c b+c} ==> ret <= x
+
+ 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 Math {}
\ No newline at end of file diff --git a/Jennisys/examples/oopsla12/Math_synth.dfy b/Jennisys/examples/oopsla12/Math_synth.dfy new file mode 100644 index 00000000..68893b3d --- /dev/null +++ b/Jennisys/examples/oopsla12/Math_synth.dfy @@ -0,0 +1,105 @@ +class Math {
+ ghost var Repr: set<object>;
+
+
+ function Valid_repr(): bool
+ reads *;
+ {
+ this in Repr &&
+ null !in Repr
+ }
+
+ function Valid_self(): bool
+ reads *;
+ {
+ Valid_repr() &&
+ true
+ }
+
+ function Valid(): bool
+ reads *;
+ {
+ this.Valid_self() &&
+ true
+ }
+
+
+ method Abs(a: int) returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret in {a, -a};
+ ensures ret >= 0;
+ {
+ if (a >= 0) {
+ ret := a;
+ } else {
+ ret := -a;
+ }
+ }
+
+
+ method Min2(a: int, b: int) returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures a < b ==> ret == a;
+ ensures a >= b ==> ret == b;
+ {
+ if (a < b) {
+ ret := a;
+ } else {
+ ret := b;
+ }
+ }
+
+
+ method Min3Sum(a: int, b: int, c: int) returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret in {a + b, a + c, b + c};
+ ensures ret <= a + b;
+ ensures ret <= a + c;
+ ensures ret <= b + c;
+ {
+ if (a + b <= a + c && a + b <= b + c) {
+ ret := a + b;
+ } else {
+ if (b + c <= a + c) {
+ ret := b + c;
+ } else {
+ ret := a + c;
+ }
+ }
+ }
+
+
+ method Min4(a: int, b: int, c: int, d: int) returns (ret: int)
+ requires Valid();
+ ensures fresh(Repr - old(Repr));
+ ensures Valid();
+ ensures ret in {a, b, c, d};
+ ensures ret <= a;
+ ensures ret <= b;
+ ensures ret <= c;
+ ensures ret <= d;
+ {
+ if ((a <= b && a <= c) && a <= d) {
+ ret := a;
+ } else {
+ if (d <= b && d <= c) {
+ ret := d;
+ } else {
+ if (c <= b) {
+ ret := c;
+ } else {
+ ret := b;
+ }
+ }
+ }
+ }
+
+}
+
+
|