diff options
| author |  rustanleino <unknown> | 2011-03-26 01:58:19 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-26 01:58:19 +0000 |
| commit | dceef1d90bfc91be2ab309107d3947ce1b3667eb (patch) | |
| tree | 3806f7b91544ac3db868f0afb17c535d42f502a8 /Test/dafny0/Answer | |
| parent | a42f800cad7918d42349914a4b8f0d58d95d6531 (diff) | |
Dafny: compile quantifiers
Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction
Dafny: split expressions when proving function postconditions
Boogie and BVD: updated copyright year ranges
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index c33cf851..b1e12099 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -295,7 +295,7 @@ Execution trace: Definedness.dfy(208,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(231,30): Error: possible violation of function postcondition
+Definedness.dfy(231,46): Error: possible violation of function postcondition
Execution trace:
(0,0): anon0
(0,0): anon5_Else
@@ -321,7 +321,7 @@ Execution trace: (0,0): anon13_Else
(0,0): anon7
(0,0): anon9
-FunctionSpecifications.dfy(40,18): Error: possible violation of function postcondition
+FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon12_Else
(0,0): anon15_Else
@@ -399,6 +399,16 @@ Execution trace: Dafny program verifier finished with 8 verified, 2 errors
+-------------------- NonGhostQuantifiers.dfy --------------------
+NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
+NonGhostQuantifiers.dfy(57,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
+NonGhostQuantifiers.dfy(61,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(71,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(86,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
+NonGhostQuantifiers.dfy(94,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
+NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+7 resolution/type errors detected in NonGhostQuantifiers.dfy
+
-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
|