diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 16:19:10 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 16:19:10 -0800 |
| commit | 3be3e9a226ee0defb514da6fe136ce7cadf9e17c (patch) | |
| tree | 40fefdd0b69ec16d46e54531be71aa33a7d3f5d2 /Test/dafny0/Predicates.dfy | |
| parent | 17d1562bae394856c24f09a2dac9f7404c5dd759 (diff) | |
Dafny: added test case for refinement and predicates (and fixed a parsing bug)
Diffstat (limited to 'Test/dafny0/Predicates.dfy')
| -rw-r--r-- | Test/dafny0/Predicates.dfy | 74 |
1 files changed, 74 insertions, 0 deletions
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 76666ef0..2583ef19 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -29,3 +29,77 @@ module B refines A { }
}
}
+
+// ------------------------------------------------
+
+module Loose {
+ class MyNumber {
+ var N: int;
+ ghost var Repr: set<object>;
+ predicate Valid
+ reads this, Repr;
+ {
+ this in Repr && null !in Repr &&
+ 0 <= N
+ }
+ constructor Init()
+ modifies this;
+ ensures Valid && fresh(Repr - {this});
+ {
+ N, Repr := 0, {this};
+ }
+ method Inc()
+ requires Valid;
+ modifies Repr;
+ ensures old(N) < N;
+ ensures Valid && fresh(Repr - old(Repr));
+ {
+ N := N + 2;
+ }
+ method Get() returns (n: int)
+ requires Valid;
+ ensures n == N;
+ {
+ n := N;
+ }
+ }
+}
+
+module Tight refines Loose {
+ class MyNumber {
+ predicate Valid
+ {
+ N % 2 == 0
+ }
+ constructor Init()
+ ensures N == 0;
+ method Inc()
+ ensures N == old(N) + 2;
+ }
+}
+
+module UnawareClient imports Loose {
+ class Client {
+ method Main() {
+ var n := new MyNumber.Init();
+ assert n.N == 0; // error: this is not known
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 4; // error: this is not known
+ }
+ }
+}
+
+module AwareClient imports Tight {
+ class Client {
+ method Main() {
+ var n := new MyNumber.Init();
+ assert n.N == 0;
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 4;
+ }
+ }
+}
|