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;
+  }
+}