Fixed bugs in encoding of preconditions of function values, Issue #84.

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