diff options
| author |  Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-20 16:51:54 +0300 |
|---|---|---|
| committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-20 16:51:54 +0300 |
| commit | 7e04037cabe8b39eab697171f1086f74fbbb7159 (patch) | |
| tree | 278f3be0ffcd26afb4ac1575878e4f18fbc92702 /Test/dafny0/Trait | |
| parent | 18f9f3e8e20c4c7c302a7e6042ffbce2dde82cdc (diff) | |
- fixed an issue regarding including ghost functions in the compiled interface
- added one more test
Diffstat (limited to 'Test/dafny0/Trait')
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride3.dfy | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy index 498a0a6b..d602bffb 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -25,4 +25,23 @@ class C extends J var a:int := 100;
assert a==100;
}
-}
\ No newline at end of file +}
+
+trait t
+{
+ function f(s2:int):int
+ ensures f(s2) > 0;
+ //requires s != null && s.Length > 1;
+ //reads s, s2;
+}
+
+class c extends t
+{
+ function f(s3:int):int
+ ensures f(s3) > 1;
+ //requires s0 != null && s0.Length > (0);
+ //reads s0;
+ {
+ 2
+ }
+}
|