summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-06-30 23:42:57 -0700
committerGravatar leino <unknown>2015-06-30 23:42:57 -0700
commit1697a133cababe66fef1fbf7a1ed9036255d8e68 (patch)
treee91d749fad97fcb7471599e342c6ad823d58503b /Test
parente7430a9b1d17ea92e986470e898d6b74fae3cea6 (diff)
Fixed bugs in encoding of preconditions of function values, Issue #84.
Diffstat (limited to 'Test')
-rw-r--r--Test/hofs/Naked.dfy10
-rw-r--r--Test/hofs/Naked.dfy.expect8
-rw-r--r--Test/hofs/Requires.dfy82
-rw-r--r--Test/hofs/Requires.dfy.expect5
-rw-r--r--Test/hofs/Simple.dfy.expect5
5 files changed, 95 insertions, 15 deletions
diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
index fa99377f..d23eb507 100644
--- a/Test/hofs/Naked.dfy
+++ b/Test/hofs/Naked.dfy
@@ -19,17 +19,17 @@ module Functions {
module Requires {
function t(x: nat): nat
- requires !t.requires(x);
+ requires !t.requires(x); // error: use of naked function in its own SCC
{ x }
function g(x: nat): nat
- requires !(g).requires(x);
+ requires !(g).requires(x); // error: use of naked function in its own SCC
{ x }
- function g2(x: int): int { h(x) }
-
+ function D(x: int): int // used so termination errors don't mask other errors
+ function g2(x: int): int decreases D(x) { h(x) } // error: precondition violation
function h(x: int): int
- requires !g2.requires(x);
+ requires !g2.requires(x); // error: use of naked function in its own SCC
{ x }
}
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index b4dfc561..514952a1 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -21,11 +21,7 @@ Execution trace:
Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
Execution trace:
(0,0): anon0
-Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
-Naked.dfy(29,30): Error: possible violation of function precondition
+Naked.dfy(30,45): Error: possible violation of function precondition
Naked.dfy(32,14): Related location
Execution trace:
(0,0): anon0
@@ -47,4 +43,4 @@ Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possibl
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 1 verified, 12 errors
+Dafny program verifier finished with 2 verified, 11 errors
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;
+ }
+}
diff --git a/Test/hofs/Requires.dfy.expect b/Test/hofs/Requires.dfy.expect
new file mode 100644
index 00000000..b9a40d66
--- /dev/null
+++ b/Test/hofs/Requires.dfy.expect
@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 20 verified, 0 errors
+Program compiled successfully
+Running...
+
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 1a1027ae..e2f16ef3 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -20,13 +20,10 @@ Execution trace:
Simple.dfy(61,10): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Simple.dfy(61,18): Error: assertion violation
-Execution trace:
- (0,0): anon0
Simple.dfy(73,10): Error: assertion violation
Execution trace:
(0,0): anon0
Simple.dfy(72,38): anon5_Else
Simple.dfy(73,38): anon6_Else
-Dafny program verifier finished with 14 verified, 7 errors
+Dafny program verifier finished with 14 verified, 6 errors