diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
| commit | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (patch) | |
| tree | d9cc893bc1289d8ad09b21f6a2242d31fa51ef70 /Test/dafny0/OpaqueFunctions.dfy | |
| parent | 129ab22811996b4b46cfbcc6eb3f4b97a95f5416 (diff) | |
Make reveal axioms from opaque functions quantify over layers
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index 3b591ef2..d00e1246 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -159,7 +159,62 @@ module M1 refines M0 { function{:opaque} id<A>(x : A):A { x }
+method id_ok()
+{
+ reveal_id();
+ assert id(1) == 1;
+}
+
+method id_fail()
+{
+ assert id(1) == 1;
+}
+
datatype Box<A> = Bx(A)
function{:opaque} id_box(x : Box):Box { x }
+method box_ok()
+{
+ reveal_id();
+ assert id(Bx(1)) == Bx(1);
+}
+
+method box_fail()
+{
+ assert id(Bx(1)) == Bx(1);
+}
+
+// ------------------------- opaque and layer quantifiers
+
+module LayerQuantifiers
+{
+ function{:opaque} f(x:nat) : bool { if x == 0 then true else f(x-1) }
+
+ method rec_should_ok()
+ {
+ reveal_f();
+ assert f(1);
+ }
+
+ method rec_should_fail()
+ {
+ assert f(1);
+ }
+
+ method rec_should_unroll_ok(one : int)
+ requires one == 1;
+ {
+ reveal_f();
+ // this one should have enough fuel
+ assert f(one + one);
+ }
+
+ method rec_should_unroll_fail(one : int)
+ requires one == 1;
+ {
+ reveal_f();
+ // this one does not have enough fuel
+ assert f(one + one + one);
+ }
+}
|