diff options
| author |  leino <unknown> | 2015-06-30 23:42:57 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-06-30 23:42:57 -0700 |
| commit | 1697a133cababe66fef1fbf7a1ed9036255d8e68 (patch) | |
| tree | e91d749fad97fcb7471599e342c6ad823d58503b /Test/hofs/Requires.dfy | |
| parent | e7430a9b1d17ea92e986470e898d6b74fae3cea6 (diff) | |
Fixed bugs in encoding of preconditions of function values, Issue #84.
Diffstat (limited to 'Test/hofs/Requires.dfy')
| -rw-r--r-- | Test/hofs/Requires.dfy | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/Test/hofs/Requires.dfy b/Test/hofs/Requires.dfy new file mode 100644 index 00000000..68677b3e --- /dev/null +++ b/Test/hofs/Requires.dfy @@ -0,0 +1,82 @@ +// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+ test0(10);
+ test5(11);
+ test6(12);
+ test1();
+ test2();
+}
+
+predicate valid(x:int)
+{
+ x > 0
+}
+
+function ref1(y:int) : int
+ requires valid(y);
+{
+ y - 1
+}
+
+lemma assumption1()
+ ensures forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+{
+}
+
+method test0(a: int)
+{
+ if ref1.requires(a) {
+ // the precondition should suffice to let us call the method
+ ghost var b := ref1(a);
+ }
+}
+method test5(a: int)
+{
+ if valid(a) {
+ // valid(a) is the precondition of ref1
+ assert ref1.requires(a);
+ }
+}
+method test6(a: int)
+{
+ if ref1.requires(a) {
+ // the precondition of ref1 is valid(a)
+ assert valid(a);
+ }
+}
+
+method test1()
+{
+ if * {
+ assert forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+ } else {
+ assert forall a, b :: ref1.requires(a) && ref1.requires(b) && ref1(a) == ref1(b)
+ ==> a == b;
+ }
+}
+
+function {:opaque} ref2(y:int) : int // Now with an opaque attribute
+ requires valid(y);
+{
+ y - 1
+}
+
+lemma assumption2()
+ ensures forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+{
+ reveal_ref2();
+}
+
+method test2()
+{
+ assumption2();
+ if * {
+ assert forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+ } else {
+ assert forall a, b :: ref2.requires(a) && ref2.requires(b) && ref2(a) == ref2(b)
+ ==> a == b;
+ }
+}
|