diff options
| author |  Bryan Parno <parno@microsoft.com> | 2013-12-13 18:09:21 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2013-12-13 18:09:21 -0800 |
| commit | 98d05fbc4c087744b44df9dd6ba5e34fbddfe4bb (patch) | |
| tree | 3a12e13786f0d2ea0bd4300fa443e238235dbceb /Test/dafny0/Compilation.dfy | |
| parent | 0cf321947991319a86adc6899b4015d19c21a188 (diff) | |
Add support for the :axiom attribute for ghost methods.
This suppresses compiler errors for ghost methods and functions without bodies.
Also changed the parser to complain about bodyless methods and functions
without bodies if /noCheating:1 is specified.
Diffstat (limited to 'Test/dafny0/Compilation.dfy')
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index 5120bf81..734cc3e6 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -148,3 +148,25 @@ class DigitsClass { }
}
+// Should not get errors about methods or functions with empty bodies
+// if they're marked with an :axiom attribute
+ghost method {:axiom} m_nobody() returns (y:int)
+ ensures y > 5;
+
+lemma {:axiom} l_nobody() returns (y:int)
+ ensures y > 5;
+
+function {:axiom} f_nobody():int
+ ensures f_nobody() > 5;
+
+// Make sure the lemma created for opaque functions doesn't produce compiler errors
+function {:opaque} hidden():int
+{
+ 7
+}
+
+method hidden_test()
+{
+ reveal_hidden();
+ assert hidden() == 7;
+}
|