diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-26 23:40:33 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-26 23:40:33 -0700 |
| commit | 8fba5ba566b28bd012ac5d4485df65308dc338a1 (patch) | |
| tree | 23287b3b10cb9c70ac9ee1f6256075a425759020 /Test/dafny1/Substitution.dfy | |
| parent | b649899e20acf38aa8bcf041a55fbd3613b809bf (diff) | |
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
Diffstat (limited to 'Test/dafny1/Substitution.dfy')
| -rw-r--r-- | Test/dafny1/Substitution.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
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<Expression>, v: int, val: int)
+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, 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| ==>
|