From 8fba5ba566b28bd012ac5d4485df65308dc338a1 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 26 May 2011 23:40:33 -0700 Subject: Dafny: * fixed ghost/non-ghost story for breaks and returns * changed compilation/translation to always use goto's to implement Dafny's breaks * introduced "break break" statements --- Test/dafny1/Substitution.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/dafny1/Substitution.dfy') diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index d3e0e82e..11c8c878 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -99,7 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) } } -static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq, v: int, val: int) +static ghost method LemmaSeq(parent: Expression, q: seq, v: int, val: int) requires (forall a :: a in q ==> a < parent); ensures |SubstSeq(parent, q, v, val)| == |q|; ensures (forall k :: 0 <= k && k < |q| ==> -- cgit v1.2.3