diff options
Diffstat (limited to 'Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy')
| -rw-r--r-- | Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy | 233 |
1 files changed, 0 insertions, 233 deletions
diff --git a/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy b/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy deleted file mode 100644 index 3f1e6b4b..00000000 --- a/Jennisys/Jennisys/examples/mod/jennisys-synth_Number.dfy +++ /dev/null @@ -1,233 +0,0 @@ -class Number {
- ghost var Repr: set<object>;
- ghost var num: int;
-
-
- 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 Double(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num == 2 * p;
- {
- this.num := 2 * p;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Init(p: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num == p;
- {
- this.num := p;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Sum(a: int, b: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num == a + b;
- {
- this.num := a + b;
- // repr stuff
- this.Repr := {this};
- }
-
-
- method Abs(a: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a, -a};
- ensures num >= 0;
- {
- if (a >= 0) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := -a;
- // repr stuff
- this.Repr := {this};
- }
- }
-
-
- method Min4(a: int, b: int, c: int, d: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a, b, c, d};
- ensures (forall x :: x in {a, b, c, d} ==> num <= x);
- {
- if (a <= b && (a <= c && a <= d)) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- if (d <= a && (d <= b && d <= c)) {
- this.num := d;
- // repr stuff
- this.Repr := {this};
- } else {
- if (c <= a && (c <= b && c <= d)) {
- this.num := c;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b;
- // repr stuff
- this.Repr := {this};
- }
- }
- }
- }
-
-
- method MinSum(a: int, b: int, c: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a + b, a + c, b + c};
- ensures num <= a + b;
- ensures num <= b + c;
- ensures num <= a + c;
- {
- if (a + b <= b + c && a + b <= a + c) {
- this.num := a + b;
- // repr stuff
- this.Repr := {this};
- } else {
- if (a + c <= a + b && a + c <= b + c) {
- this.num := a + c;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b + c;
- // repr stuff
- this.Repr := {this};
- }
- }
- }
-
-
- method Min32(a: int, b: int, c: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a, b, c};
- ensures (forall x :: x in {a, b, c} ==> num <= x);
- {
- if (a <= b && a <= c) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- if (c <= a && c <= b) {
- this.num := c;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b;
- // repr stuff
- this.Repr := {this};
- }
- }
- }
-
-
- method Min3(a: int, b: int, c: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a, b, c};
- ensures num <= a;
- ensures num <= b;
- ensures num <= c;
- {
- if (a <= b && a <= c) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- if (c <= a && c <= b) {
- this.num := c;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b;
- // repr stuff
- this.Repr := {this};
- }
- }
- }
-
-
- method Min22(a: int, b: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures num in {a, b};
- ensures num <= a;
- ensures num <= b;
- {
- if (a <= b) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b;
- // repr stuff
- this.Repr := {this};
- }
- }
-
-
- method Min2(a: int, b: int)
- modifies this;
- ensures fresh(Repr - {this});
- ensures Valid();
- ensures a < b ==> num == a;
- ensures a >= b ==> num == b;
- {
- if (a >= b ==> a == b) {
- this.num := a;
- // repr stuff
- this.Repr := {this};
- } else {
- this.num := b;
- // repr stuff
- this.Repr := {this};
- }
- }
-
-}
-
-
|