From 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 Mon Sep 17 00:00:00 2001 From: Dan Rosén 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/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy index 75a7822e..c752bd38 100644 --- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy +++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy @@ -91,7 +91,7 @@ class Tree { function method IsEmpty(): bool requires Valid(); - reads Repr; + reads this, Repr; ensures IsEmpty() <==> Contents == []; { left == this -- cgit v1.2.3