diff options
| author |  Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-20 19:25:04 +0300 |
|---|---|---|
| committer | Reza Ahmadi <reza.ahmadi@uta.fi> | 2014-07-20 19:25:04 +0300 |
| commit | d10e53aa085cbd95198d9797bb247c6ba3a34145 (patch) | |
| tree | 171dfd34431c8bf49ef38f7dd0c49a57ed0e69b1 /Test/dafny0/Trait | |
| parent | 129744b09404197d1f84481601edd51d0d104bd4 (diff) | |
added one more test.
Diffstat (limited to 'Test/dafny0/Trait')
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride3.dfy | 17 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride3.dfy.expect | 2 |
2 files changed, 18 insertions, 1 deletions
diff --git a/Test/dafny0/Trait/TraitOverride3.dfy b/Test/dafny0/Trait/TraitOverride3.dfy index 467ad333..6a5fa59f 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy +++ b/Test/dafny0/Trait/TraitOverride3.dfy @@ -57,3 +57,20 @@ class C1 extends P1 {
}
+
+trait TT
+{
+ static function method M(a:int, b:int) : int
+ ensures M(a,b) == a + b;
+ {
+ a + b
+ }
+}
+
+class CC extends TT
+{
+ method Testing(a:int,b:int)
+ {
+ assert (TT.M(a,b) == a + b);
+ }
+}
diff --git a/Test/dafny0/Trait/TraitOverride3.dfy.expect b/Test/dafny0/Trait/TraitOverride3.dfy.expect index 73727958..9d7e625f 100644 --- a/Test/dafny0/Trait/TraitOverride3.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride3.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 21 verified, 0 errors
+Dafny program verifier finished with 25 verified, 0 errors
|