diff options
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 136 |
1 files changed, 64 insertions, 72 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bf3ba197..5cfee29d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -46,16 +46,9 @@ class MyClass<T, U> { }
}
-datatype List<T> {
- Nil;
- Cons(T, List<T>);
-}
+datatype List<T> = Nil | Cons(T, List<T>);
-datatype WildData {
- Something;
- JustAboutAnything(bool, myName: set<int>, int, WildData);
- More(List<int>);
-}
+datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>);
class C {
var w: WildData;
@@ -65,7 +58,7 @@ class C { Dafny program verifier finished with 0 verified, 0 errors
-------------------- TypeTests.dfy --------------------
-TypeTests.dfy(95,9): Error: sorry, cannot instantiate collection type with a subrange type
+TypeTests.dfy(84,9): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)
TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)
TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)
@@ -73,21 +66,20 @@ TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, g TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
-TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-TypeTests.dfy(64,6): Error: Duplicate local-variable name: z
-TypeTests.dfy(66,6): Error: Duplicate local-variable name: x
-TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
-TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
-TypeTests.dfy(79,17): Error: member F in class C does not refer to a method
-TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments
-TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
-TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
-TypeTests.dfy(96,9): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(97,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-TypeTests.dfy(98,8): Error: sorry, cannot instantiate 'array' type with a subrange type
-22 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
+TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(53,6): Error: Duplicate local-variable name: z
+TypeTests.dfy(55,6): Error: Duplicate local-variable name: x
+TypeTests.dfy(58,8): Error: Duplicate local-variable name: x
+TypeTests.dfy(61,6): Error: Duplicate local-variable name: y
+TypeTests.dfy(68,17): Error: member F in class C does not refer to a method
+TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
+TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
+TypeTests.dfy(79,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
+TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type
+TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type
+21 resolution/type errors detected in TypeTests.dfy
-------------------- NatTypes.dfy --------------------
NatTypes.dfy(7,5): Error: value assigned to a nat must be non-negative
@@ -114,16 +106,16 @@ NatTypes.dfy(54,16): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(71,16): Error: assertion violation
+NatTypes.dfy(68,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(89,16): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(86,16): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(104,45): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(101,45): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
@@ -192,14 +184,14 @@ Execution trace: (0,0): anon6
(0,0): anon14_Then
(0,0): anon11
-SmallTests.dfy(272,24): Error BP5002: A precondition for this call might not hold.
-SmallTests.dfy(250,30): Related location: This is the precondition that might not hold.
+SmallTests.dfy(271,24): Error BP5002: A precondition for this call might not hold.
+SmallTests.dfy(249,30): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
- SmallTests.dfy(267,19): anon3_Else
+ SmallTests.dfy(266,19): anon3_Else
(0,0): anon2
-SmallTests.dfy(307,3): Error BP5003: A postcondition might not hold on this return path.
-SmallTests.dfy(301,11): Related location: This is the postcondition that might not hold.
+SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.
+SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon18_Else
@@ -379,7 +371,7 @@ Execution trace: Dafny program verifier finished with 23 verified, 34 errors
-------------------- FunctionSpecifications.dfy --------------------
-FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition
+FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition
Execution trace:
(0,0): anon10_Else
(0,0): anon11_Else
@@ -387,13 +379,13 @@ Execution trace: (0,0): anon13_Else
(0,0): anon7
(0,0): anon9
-FunctionSpecifications.dfy(40,24): Error: possible violation of function postcondition
+FunctionSpecifications.dfy(37,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon12_Else
(0,0): anon15_Else
(0,0): anon16_Then
(0,0): anon11
-FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(50,11): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon9_Then
@@ -557,10 +549,10 @@ Modules0.dfy(187,12): Error: match source expression 'l' has already been used a 13 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
-Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
Execution trace:
(0,0): anon0
-Modules1.dfy(61,3): Error: failure to decrease termination measure
+Modules1.dfy(58,3): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
@@ -755,57 +747,57 @@ Execution trace: Dafny program verifier finished with 18 verified, 10 errors
-------------------- Termination.dfy --------------------
-Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(100,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(103,3): anon7_LoopHead
+ Termination.dfy(100,3): anon7_LoopHead
(0,0): anon7_LoopBody
- Termination.dfy(103,3): anon8_Else
+ Termination.dfy(100,3): anon8_Else
(0,0): anon3
- Termination.dfy(103,3): anon9_Else
+ Termination.dfy(100,3): anon9_Else
(0,0): anon5
-Termination.dfy(111,3): Error: cannot prove termination; try supplying a decreases clause for the loop
+Termination.dfy(108,3): Error: cannot prove termination; try supplying a decreases clause for the loop
Execution trace:
(0,0): anon0
- Termination.dfy(111,3): anon9_LoopHead
+ Termination.dfy(108,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(111,3): anon10_Else
+ Termination.dfy(108,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(111,3): anon12_Else
+ Termination.dfy(108,3): anon12_Else
(0,0): anon7
-Termination.dfy(120,3): Error: decreases expression might not decrease
+Termination.dfy(117,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(120,3): anon9_LoopHead
+ Termination.dfy(117,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(120,3): anon10_Else
+ Termination.dfy(117,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(120,3): anon12_Else
+ Termination.dfy(117,3): anon12_Else
(0,0): anon7
-Termination.dfy(121,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
+Termination.dfy(118,17): Error: decreases expression must be bounded below by 0 at end of loop iteration
Execution trace:
(0,0): anon0
- Termination.dfy(120,3): anon9_LoopHead
+ Termination.dfy(117,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(120,3): anon10_Else
+ Termination.dfy(117,3): anon10_Else
(0,0): anon11_Then
(0,0): anon5
- Termination.dfy(120,3): anon12_Else
+ Termination.dfy(117,3): anon12_Else
(0,0): anon7
-Termination.dfy(249,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(246,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(289,3): Error: decreases expression might not decrease
+Termination.dfy(286,3): Error: decreases expression might not decrease
Execution trace:
(0,0): anon0
- Termination.dfy(289,3): anon10_LoopHead
+ Termination.dfy(286,3): anon10_LoopHead
(0,0): anon10_LoopBody
- Termination.dfy(289,3): anon11_Else
- Termination.dfy(289,3): anon12_Else
+ Termination.dfy(286,3): anon11_Else
+ Termination.dfy(286,3): anon12_Else
(0,0): anon13_Else
(0,0): anon8
@@ -818,20 +810,20 @@ Execution trace: DTypes.dfy(53,18): Error: assertion violation
Execution trace:
(0,0): anon0
-DTypes.dfy(123,13): Error: assertion violation
-DTypes.dfy(94,3): Related location: Related location
+DTypes.dfy(117,13): Error: assertion violation
+DTypes.dfy(89,30): Related location: Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(129,13): Error: assertion violation
-DTypes.dfy(93,3): Related location: Related location
+DTypes.dfy(123,13): Error: assertion violation
+DTypes.dfy(89,20): Related location: Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(139,12): Error: assertion violation
-DTypes.dfy(134,6): Related location: Related location
-DTypes.dfy(93,3): Related location: Related location
+DTypes.dfy(133,12): Error: assertion violation
+DTypes.dfy(128,6): Related location: Related location
+DTypes.dfy(89,20): Related location: Related location
Execution trace:
(0,0): anon0
-DTypes.dfy(160,12): Error: assertion violation
+DTypes.dfy(154,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -883,7 +875,7 @@ Execution trace: Dafny program verifier finished with 33 verified, 5 errors
-------------------- Datatypes.dfy --------------------
-Datatypes.dfy(82,20): Error: assertion violation
+Datatypes.dfy(79,20): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon20_Else
@@ -897,11 +889,11 @@ Execution trace: Dafny program verifier finished with 17 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
-TypeAntecedents.dfy(34,13): Error: assertion violation
+TypeAntecedents.dfy(32,13): Error: assertion violation
Execution trace:
(0,0): anon0
-TypeAntecedents.dfy(60,1): Error BP5003: A postcondition might not hold on this return path.
-TypeAntecedents.dfy(59,15): Related location: This is the postcondition that might not hold.
+TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this return path.
+TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon15_Then
@@ -913,7 +905,7 @@ Execution trace: (0,0): anon20_Then
(0,0): anon21_Then
(0,0): anon14
-TypeAntecedents.dfy(68,16): Error: assertion violation
+TypeAntecedents.dfy(63,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon15_Else
|