From 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 11 Aug 2014 14:57:27 -0700
Subject: Add higher-order-functions and some other goodies

  * The reads clause now needs to be self framing.

  * The requires clause now needs to be framed by the reads clause.

  * There are one-shot lambdas, with a single arrow, but they will probably be
    removed.

  * There is a {:heapQuantifier} attribute to quantifiers, but they will
    probably be removed.

  * Add smart handling of type variables

  * Add < and > for datatype & type parameter
---
 Test/hofs/ReadsReads.dfy | 59 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 Test/hofs/ReadsReads.dfy

(limited to 'Test/hofs/ReadsReads.dfy')

diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy
new file mode 100644
index 00000000..bc80713d
--- /dev/null
+++ b/Test/hofs/ReadsReads.dfy
@@ -0,0 +1,59 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function MyReadsOk(f : A -> B, a : A) : set<object>
+  reads f.reads(a);
+{
+  f.reads(a)
+}
+
+function MyReadsOk2(f : A -> B, a : A) : set<object>
+  reads f.reads(a);
+{
+  (f.reads)(a)
+}
+
+function MyReadsOk3(f : A -> B, a : A) : set<object>
+  reads (f.reads)(a);
+{
+  f.reads(a)
+}
+
+function MyReadsOk4(f : A -> B, a : A) : set<object>
+  reads (f.reads)(a);
+{
+  (f.reads)(a)
+}
+
+function MyReadsBad(f : A -> B, a : A) : set<object>
+{
+  f.reads(a)
+}
+
+function MyReadsBad2(f : A -> B, a : A) : set<object>
+{
+  (f.reads)(a)
+}
+
+function MyReadsOk'(f : A -> B, a : A, o : object) : bool
+  reads f.reads(a);
+{
+  o in f.reads(a)
+}
+
+function MyReadsBad'(f : A -> B, a : A, o : object) : bool
+{
+  o in f.reads(a)
+}
+
+function MyRequiresOk(f : A -> B, a : A) : bool
+  reads f.reads(a);
+{
+  f.requires(a)
+}
+
+function MyRequiresBad(f : A -> B, a : A) : bool
+{
+  f.requires(a)
+}
+
-- 
cgit v1.2.3