From 5b3dcd0c09a7ea8a34e7f5e4b8800015b3b07e96 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Wed, 1 Jul 2015 12:37:54 -0700 Subject: Add the ability to specify how much "fuel" a function should have, i.e., how many times Z3 is permitted to unfold it's definition. The new {:fuel} annotation can be added to the function itself, it which case it will apply to all uses of that function, or it can overridden within the scope of a module, function, method, iterator, calc, forall, while, assert, or assume. The general format is: {:fuel functionName,lowFuel,highFuel} When applied as an annotation to the function itself, omit functionName. If highFuel is omitted, it defaults to lowFuel + 1. The default fuel setting for recursive functions is 1,2. Setting the fuel higher, say, to 3,4, will give more unfoldings, which may make some proofs go through with less programmer assistance (e.g., with fewer assert statements), but it may also increase verification time, so use it with care. Setting the fuel to 0,0 is similar to making the definition opaque, except when used with all literal arguments. --- Test/dafny4/Circ.dfy | 2 ++ 1 file changed, 2 insertions(+) (limited to 'Test/dafny4/Circ.dfy') diff --git a/Test/dafny4/Circ.dfy b/Test/dafny4/Circ.dfy index e7609195..d110c05c 100644 --- a/Test/dafny4/Circ.dfy +++ b/Test/dafny4/Circ.dfy @@ -16,6 +16,7 @@ function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) } colemma BlinkZipProperty() ensures zip(zeros(), ones()) == blink(); { + BlinkZipProperty(); } // ----- Thue-Morse sequence ----- @@ -75,6 +76,7 @@ colemma FProperty(s: Stream) // def. zip Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail))); } + FProperty(s.tail); } // The fix-point theorem now follows easily. -- cgit v1.2.3