diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
| commit | b0b61083adb4b427974c772658cdc744da23f42b (patch) | |
| tree | ca08e2f2f4d9b62583177e8a0a0691eb8f353dee /Test/dafny0/Answer | |
| parent | 8eb077dfd8515f26dc58754334d52f9c44a73e0c (diff) | |
Support for copredicates and prefix predicates in comethods.
(Missing from the co support are (prefix) equalities of codatatypes,
various restrictions on the use of co/prefix-predicates, and tactic
support for applying the (prefix-)induction automatically.)
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 072339b3..97e7c870 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1342,17 +1342,31 @@ CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this conte CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)
13 resolution/type errors detected in CoResolution.dfy
+-------------------- CoPrefix.dfy --------------------
+CoPrefix.dfy(61,7): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+CoPrefix.dfy(74,7): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Then
+CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path.
+CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold.
+CoPrefix.dfy(101,17): Related location: Related location
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 17 verified, 3 errors
+
-------------------- CoinductiveProofs.dfy --------------------
CoinductiveProofs.dfy(26,12): Error: assertion violation
CoinductiveProofs.dfy(10,17): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(33,1): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(32,11): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(10,17): Related location: Related location
-Execution trace:
- (0,0): anon0
CoinductiveProofs.dfy(56,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(55,11): Related location: This is the postcondition that might not hold.
CoinductiveProofs.dfy(51,3): Related location: Related location
@@ -1380,16 +1394,14 @@ Execution trace: (0,0): anon0
CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.
CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(1,24): Related location: Related location
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 31 verified, 9 errors
+Dafny program verifier finished with 32 verified, 8 errors
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
|