diff options
author | Rustan Leino <unknown> | 2014-04-19 20:00:12 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2014-04-19 20:00:12 -0700 |
commit | b56d76455f4f692ae609cffd3c0916d05b55f9ee (patch) | |
tree | 360e5124015f14c360db76fe8861b7bc8b08a0c6 /Test/dafny0/Include.dfy | |
parent | f73fd1028aad4b84fc445c1ef6ee39b08ee252a4 (diff) |
Members included from different files are now internally marked with an IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features.
Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines).
Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.
Diffstat (limited to 'Test/dafny0/Include.dfy')
-rw-r--r-- | Test/dafny0/Include.dfy | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Test/dafny0/Include.dfy b/Test/dafny0/Include.dfy index a228194f..00458dc3 100644 --- a/Test/dafny0/Include.dfy +++ b/Test/dafny0/Include.dfy @@ -10,3 +10,22 @@ method test_include(z:int) var w := m_unproven(z);
assert w == 2*z;
}
+
+// and some refinement stuff, to make sure it works with includes
+module Concrete refines Abstract
+{
+ function method inc... // error: postcondition violation
+ {
+ x - 1
+ }
+ method M...
+ {
+ var y := G(x); // error: it is not know whether or not G(x) is non-negative, as required
+ if x < 68 {
+ return 70; // error
+ } else if 30 <= x { // this will always be true here
+ return x; // fine
+ }
+ ...;
+ }
+}
|