diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 101 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 89 | ||||
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 74 | ||||
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 25 | ||||
| -rw-r--r-- | Test/dafny0/ModulesCycle.dfy | 35 | ||||
| -rw-r--r-- | Test/dafny0/Predicates.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny0/Refinement.dfy | 5 |
8 files changed, 197 insertions, 144 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7510363a..85958099 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -703,8 +703,8 @@ Execution trace: Dafny program verifier finished with 7 verified, 1 error
-------------------- ModulesCycle.dfy --------------------
-ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
-ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+ModulesCycle.dfy(3,9): Error: module T does not exist
+ModulesCycle.dfy(6,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B
2 resolution/type errors detected in ModulesCycle.dfy
-------------------- Modules0.dfy --------------------
@@ -714,55 +714,47 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)
-Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
-Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
-Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
-Modules0.dfy(256,13): Error: unresolved identifier: X
-Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(299,16): Error: member R does not exist in class B
-Modules0.dfy(299,6): Error: expected method call, found expression
-Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
-Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
-Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
-Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
-Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp
-Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
-Modules0.dfy(332,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts
-Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context
-Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context
-36 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
+Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
+Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
+Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(221,8): Error: new can be applied only to reference types (got X)
+Modules0.dfy(230,13): Error: The name does not exist in the given module
+Modules0.dfy(240,13): Error: unresolved identifier: X
+Modules0.dfy(241,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget a module import?)
+Modules0.dfy(280,12): Error: new can be applied only to reference types (got D)
+Modules0.dfy(283,25): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(284,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(284,6): Error: expected method call, found expression
+Modules0.dfy(285,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(285,6): Error: expected method call, found expression
+Modules0.dfy(307,24): Error: Undeclared module name: Q_Imp (did you forget a module import?)
+Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
+28 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
-Modules1.dfy(74,16): Error: assertion violation
+Modules1.dfy(75,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(86,16): Error: assertion violation
+Modules1.dfy(88,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(88,14): Error: assertion violation
+Modules1.dfy(90,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(53,3): Error: decreases expression must be bounded below by 0
Execution trace:
(0,0): anon0
-Modules1.dfy(58,3): Error: failure to decrease termination measure
+Modules1.dfy(59,3): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
@@ -1441,19 +1433,19 @@ Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this retur Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(179,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(180,5): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(112,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(176,9): Related location: Related location
+Refinement.dfy(177,9): Related location: Related location
Execution trace:
(0,0): anon0
-Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(184,5): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(120,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(176,9): Related location: Related location
+Refinement.dfy(177,9): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Refinement.dfy(189,7): Error: assertion violation
+Refinement.dfy(190,7): Error: assertion violation
Refinement.dfy[IncorrectConcrete](128,24): Related location: Related location
Execution trace:
(0,0): anon0
@@ -1535,24 +1527,24 @@ Predicates.dfy[B](17,15): Related location: This is the postcondition that might Predicates.dfy(28,9): Related location: Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(84,16): Error: assertion violation
+Predicates.dfy(85,16): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy(88,14): Error: assertion violation
+Predicates.dfy(89,14): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy[Tricky_Full](121,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Tricky_Full](120,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(131,7): Related location: Related location
-Predicates.dfy[Tricky_Full](111,9): Related location: Related location
+Predicates.dfy[Tricky_Full](123,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Tricky_Full](122,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(133,7): Related location: Related location
+Predicates.dfy[Tricky_Full](113,9): Related location: Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(159,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy(158,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(161,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy(160,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Predicates.dfy[Q1](149,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Q1](148,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy[Q1](151,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Q1](150,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
@@ -1583,9 +1575,10 @@ Execution trace: Dafny program verifier finished with 30 verified, 2 errors
-------------------- LiberalEquality.dfy --------------------
+LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)
LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)
-2 resolution/type errors detected in LiberalEquality.dfy
+3 resolution/type errors detected in LiberalEquality.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy new file mode 100644 index 00000000..251b2e2f --- /dev/null +++ b/Test/dafny0/EqualityTypes.dfy @@ -0,0 +1,89 @@ +module A {
+ datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);
+ datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);
+
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T>(x: Inferred<T>)
+ }
+}
+
+module B refines A {
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T(==)>(x: Inferred<T>)
+ }
+}
+
+// ----------------------------
+
+module C {
+ type X(==);
+ type Y(==);
+}
+
+module D refines C {
+ class X { }
+ datatype Y = Red | Green | Blue;
+}
+
+module E refines C {
+ codatatype X = Next(int, X); // error: X requires equality and codatatypes don't got it
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green(X) | Blue;
+}
+
+module F refines C {
+ datatype X<T> = Nil | Cons(T, X<T>); // error: not allowed to add a type parameter to type X
+ class Y<T> { } // error: not allowed to add a type parameter to type Y
+}
+
+module G refines C {
+ datatype X = Nil | Next(Z, X); // error: X does not support equality
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green | Blue;
+}
+
+// ----------------------------
+
+module H {
+ datatype Dt<T> = Nil | Cons(T, Dt);
+
+ datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);
+ datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);
+ datatype BulkyListAuxAux<T> = GoBack(BulkyList);
+
+ codatatype Stream<T> = Next(head: T, tail: Stream<T>);
+
+ method M<T(==)>(x: T)
+ { }
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ { if x == y then 5 else 7 } // this equality is allowed
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // fine
+
+ method Caller0(b: BulkyList, y: int) {
+ match (b) {
+ case Nothing =>
+ case Wrapper(t, bla) =>
+ var u;
+ if (y < 100) { u := t; }
+ // The following call is allowed, because it will be inferred that
+ // 'u' is of a type that supports equality
+ M(u);
+ }
+ }
+ method Caller1(d: Dt) {
+ match (d) {
+ case Nil =>
+ case Cons(t, rest) =>
+ M(t); // error: t may be of a type that does not support equality
+ }
+ }
+ method Caller2(co: Stream) {
+ var d := Cons(co, Nil);
+ Caller1(d); // case in point for the error in Caller1
+ }
+}
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy index 3dc52c80..b9b4629b 100644 --- a/Test/dafny0/LiberalEquality.dfy +++ b/Test/dafny0/LiberalEquality.dfy @@ -15,7 +15,7 @@ class Test<T> { }
method m1<T, U>(t: T, u: U)
- requires t != u;
+ requires t != u; // Cannot compare type parameters (can only compare reference types that could be the same)
{
}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 80ac7eef..273c88de 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -23,46 +23,26 @@ module N { class T { }
}
-module U imports N { // fine, despite the fact that a class is called U,
- // since module names are in their own name space
+module U {
+ module NN = N;
}
-module UU imports N, U, N, N { // duplicates are allowed
-}
-
-module N_left imports N { }
-module N_right imports N { }
-module Diamond imports N_left, N_right { // this imports N.T twice, but that's okay
-}
-module A imports N, M { // Note, this has the effect of importing two different T's,
- // but that's okay as long as the module doesn't try to access
- // one of them
+module A { // Note, this has the effect of importing two different T's,
+ // but that's okay as long as the module doesn't try to access
+ // one of them
+ module MM = M;
+ module NN = N;
class X {
- var t: T; // error: use of the ambiguous name T
- function F(x: T): // error: use of the ambiguous name T
- T // error: use of the ambiguous name T
+ var t: MM.T; // error: use of the ambiguous name T
+ function F(x: MM.T): // error: use of the ambiguous name T
+ MM.T // error: use of the ambiguous name T
{ x }
- method M(x: T) // error: use of the ambiguous name T
- returns (y: T) // error: use of the ambiguous name T
+ method M(x: NN.T) // error: use of the ambiguous name T
+ returns (y: NN.T) // error: use of the ambiguous name T
}
}
-module A' imports N, M {
- method M()
- { var g := new T; } // error: use of the ambiguous name T
-}
-module B0 imports A {
- class BadUse {
- var b0: T; // error: T is not directly accessible
- }
-}
-
-module B1 imports A, N {
- class GoodUse {
- var b1: T; // fine
- }
-}
// --------------- calls
@@ -76,9 +56,10 @@ module X0 { }
}
-module X1 imports X0 {
+module X1 {
+ module X0' = X0;
class MyClass1 {
- method Down(x0: MyClass0) {
+ method Down(x0: X0'.MyClass0) {
x0.Down();
}
method Up(x2: MyClass2) { // error: class MyClass2 is not in scope
@@ -86,7 +67,7 @@ module X1 imports X0 { }
}
-module X2 imports X0, X1, YY {
+module X2 {
class MyClass2 {
method Down(x1: MyClass1, x0: MyClass0) {
x1.Down(x0);
@@ -231,9 +212,10 @@ module ATr { }
}
-module BTr imports ATr {
+module BTr {
+ module A = ATr;
class Y {
- method N() returns (x: X)
+ method N() returns (x: A.X)
ensures x != null;
{
x := new X;
@@ -241,15 +223,17 @@ module BTr imports ATr { }
}
-module CTr imports BTr {
+module CTr {
+ module B = BTr;
class Z {
- var b: Y; // fine
- var a: X; // error: imports don't reach name X explicitly
+ var b: B.Y; // fine
+ var a: B.X; // error: imports don't reach name X explicitly
}
}
-module CTs imports BTr {
+module CTs {
+ module B = BTr;
method P() {
- var y := new Y;
+ var y := new B.Y;
var x := y.N(); // this is allowed and will correctly infer the type of x to
// be X, but X could not have been mentioned explicitly
var q := x.M();
@@ -285,7 +269,9 @@ module NonLocalB { }
}
-module Local imports NonLocalA, NonLocalB {
+module Local {
+ module AA = NonLocalA;
+ module BB = NonLocalB;
class MyClass {
method MyMethod()
{
@@ -317,7 +303,7 @@ module Q_Imp { }
}
-module Q_M imports Q_Imp {
+module Q_M {
method MyMethod(root: Q_Imp.Node, S: set<Node>)
requires root in S; // error: the element type of S does not agree with the type of root
{
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index e8a88749..6fd8560e 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -1,6 +1,7 @@ -module A imports B {
+module A {
+ module B = Babble;
class X {
- function Fx(z: Z): int
+ function Fx(z: B.Z): int
requires z != null;
decreases 5, 4, 3;
{ z.G() } // fine; this goes to a different module
@@ -17,7 +18,7 @@ method MyMethod() { } var MyField: int;
-module B {
+module Babble {
class Z {
method K() { }
function G(): int
@@ -78,14 +79,15 @@ module A_Visibility { }
}
-module B_Visibility imports A_Visibility {
+module B_Visibility {
+ module A = A_Visibility;
method Main() {
var y;
- if (C.P(y)) {
+ if (A.C.P(y)) {
assert 0 <= y; // this much is known of C.P
assert 2 <= y; // error
} else {
- assert C.P(8); // error: C.P cannot be established outside the declaring module
+ assert A.C.P(8); // error: C.P cannot be established outside the declaring module
}
}
}
@@ -99,13 +101,14 @@ module Q_Imp { }
}
-module Q_M imports Q_Imp {
- method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)
+module Q_M {
+ module Q = Q_Imp;
+ method MyMethod(root: Q.Node, S: set<Q.Node>)
requires root in S;
{
- var i := new Q_Imp.Node;
- var j := new Node;
+ var i := new Q.Node;
+ var j := new Q.Node;
assert i != j; // fine
- var q := new Q_Imp.Klassy.Init();
+ var q := new Q.Klassy.Init();
}
}
diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy index a7f1caa2..15cad8e8 100644 --- a/Test/dafny0/ModulesCycle.dfy +++ b/Test/dafny0/ModulesCycle.dfy @@ -1,33 +1,12 @@ -module M {
- class T { }
- class U { }
-}
-
-module N {
-}
-
-module U imports N {
-}
-
-module V imports T { // error: T is not a module
-}
-module A imports B, M {
- class Y { }
+module V {
+ module t = T; // error: T is not visible (and isn't even a module)
}
-module B imports N, M {
- class X { }
+module A {
+ module B = C;
}
-module G imports A, M, A, H, B { // error: cycle in import graph
-}
-
-module H imports A, N, I {
-}
-
-module I imports J {
-}
-
-module J imports G, M {
-}
+module C {
+ module D = A;
+}
\ No newline at end of file diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 146129b5..8857482f 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -78,9 +78,10 @@ module Tight refines Loose { }
}
-module UnawareClient imports Loose {
+module UnawareClient {
+ module L = Loose;
method Main0() {
- var n := new MyNumber.Init();
+ var n := new L.MyNumber.Init();
assert n.N == 0; // error: this is not known
n.Inc();
n.Inc();
@@ -89,9 +90,10 @@ module UnawareClient imports Loose { }
}
-module AwareClient imports Tight {
+module AwareClient {
+ module T = Tight;
method Main1() {
- var n := new MyNumber.Init();
+ var n := new T.MyNumber.Init();
assert n.N == 0;
n.Inc();
n.Inc();
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index da7f0ac2..2c2fc52b 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -155,10 +155,11 @@ module Concrete refines Abstract { } } -module Client imports Concrete { +module Client { + module C = Concrete; class TheClient { method Main() { - var n := new MyNumber.Init(); + var n := new C.MyNumber.Init(); n.Inc(); n.Inc(); var k := n.Get(); |