diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-12 10:38:14 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-12 10:38:14 -0800 |
| commit | 26d9a05b985859f3a0d089367b35f493cbff090b (patch) | |
| tree | 6afb399a018622db438f817ed36c17f30b165b85 /Test/dafny0/Predicates.dfy | |
| parent | aa1db181e9aa277a1cca3c7f3e54c0f2b0d19d41 (diff) | |
Dafny: handle refinement of nested tokens that come from SpliExpr (still need to deal with unsplit expressions, like quantifiers)
Diffstat (limited to 'Test/dafny0/Predicates.dfy')
| -rw-r--r-- | Test/dafny0/Predicates.dfy | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 334b3842..f7b6e07f 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -99,3 +99,36 @@ module AwareClient imports Tight { assert k == 4;
}
}
+
+// -------- Tricky refinement inheritance ----------------------------------------
+
+module Tricky_Base {
+ class Tree {
+ var x: int;
+ predicate Constrained
+ reads this;
+ {
+ x < 10
+ }
+ predicate Valid
+ reads this;
+ {
+ x < 100
+ }
+ method Init()
+ modifies this;
+ ensures Valid;
+ {
+ x := 20;
+ }
+ }
+}
+
+module Tricky_Full refines Tricky_Base {
+ class Tree {
+ predicate Valid
+ {
+ Constrained // this causes an error to be generated for the inherited Init
+ }
+ }
+}
|