diff options
author | Rustan Leino <leino@microsoft.com> | 2012-01-10 16:45:24 -0800 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 16:45:24 -0800 |
commit | 11a0520f5fc3890358accace772c7a5f26c19c72 (patch) | |
tree | fb77274458b982f36170a2c4c7c53f7aba6b5b05 /Test/dafny0/Predicates.dfy | |
parent | 3be3e9a226ee0defb514da6fe136ce7cadf9e17c (diff) |
Dafny: allow class-member declarations at top level of any module (not just the default module); these go into the (new) default class of each module
Diffstat (limited to 'Test/dafny0/Predicates.dfy')
-rw-r--r-- | Test/dafny0/Predicates.dfy | 32 |
1 files changed, 14 insertions, 18 deletions
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 2583ef19..334b3842 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -79,27 +79,23 @@ module Tight refines Loose { }
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
- }
+ 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;
- }
+ method Main() {
+ var n := new MyNumber.Init();
+ assert n.N == 0;
+ n.Inc();
+ n.Inc();
+ var k := n.Get();
+ assert k == 4;
}
}
|