From a8161c0e52d9c1743679091c36f64e925723d607 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Jul 2014 20:50:08 -0700 Subject: Added type synonyms. (No support yet for these in refinements.) --- Test/dafny0/ResolutionErrors.dfy | 59 +++++++++++++++++++++++++++++++++ Test/dafny0/ResolutionErrors.dfy.expect | 17 +++++++++- Test/dafny0/TypeSynonyms.dfy | 46 +++++++++++++++++++++++++ Test/dafny0/TypeSynonyms.dfy.expect | 2 ++ 4 files changed, 123 insertions(+), 1 deletion(-) create mode 100644 Test/dafny0/TypeSynonyms.dfy create mode 100644 Test/dafny0/TypeSynonyms.dfy.expect (limited to 'Test/dafny0') diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 137aa92c..823fbe29 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -983,3 +983,62 @@ module TypeArgumentCount { var c: C; // error: too many type arguments } } + +// --- Type synonyms --- + +module BadTypeSynonyms { + datatype List = Nil | Cons(T, List) + type BadSyn0 = List // error: must have at least one type parameter + type BadSyn1 = badName // error: badName does not denote a type + type BadSyn2 = List // error: X does not denote a type + type BadSyn2 = int // error: repeated name +} + +// --- cycles --- + +module CycleError0 { + type A = A // error: cycle: A -> A +} +module CycleError1 { + type A = B // error: cycle: A -> B -> A + type B = A +} +module CycleError2 { + type A = B // error: cycle: A -> B -> A + type B = set +} +module Good0 { + type A = (B, D) + type B = C + class C { + var a: A; // this is fine + } + datatype D = Make(A, B, C) // this is fine, too +} +module CycleError3 { + type A = B // error: cycle: A -> B -> A + type B = C + class C { } +} +module CycleError4 { + type A = B // error: cycle: A -> B -> A + type B = Dt + datatype Dt = Make(T) +} + +// --- attributes in top-level declarations --- + +iterator {:myAttribute x} Iter() { // error: x does not refer to anything +} + +class {:myAttribute x} C { // error: x does not refer to anything +} + +datatype {:myAttribute x} Dt = Blue // error: x does not refer to anything + +type {:myAttribute x} Something // error: x does not refer to anything + +type {:myAttribute x} Synonym = int // error: x does not refer to anything + +module {:myAttribute x} Modulette { // error: x does not refer to anything +} diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 4075ff29..820465db 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -56,6 +56,16 @@ ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements ( ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement) ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3 ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C +ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2 +ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List +ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?) +ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?) +ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A +ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A +ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x ResolutionErrors.dfy(429,2): Error: More than one default constructor ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts @@ -84,6 +94,11 @@ ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can b ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x) +ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x +ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x +ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x +ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x +ResolutionErrors.dfy(1041,19): Error: unresolved identifier: x ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3) ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3) @@ -147,4 +162,4 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real) ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int) ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat) -149 resolution/type errors detected in ResolutionErrors.dfy +164 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/TypeSynonyms.dfy b/Test/dafny0/TypeSynonyms.dfy new file mode 100644 index 00000000..4bec5253 --- /dev/null +++ b/Test/dafny0/TypeSynonyms.dfy @@ -0,0 +1,46 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type MyType = int + +type Int = int + +type PairaBools = (bool, bool) + +datatype List = Nil | Cons(T, List) + +type Synonym0 = List + +type Synonym1 = List // type argument of List filled in automatically + +type Synonym2 = List + +type Synonym3 = Synonym4 + +type Synonym4 = Synonym2 + +type Synonym5 = List + +function Plus(x: Int, y: int): Int +{ + x + y +} + +method Next(s: Synonym1) returns (u: Synonym1) +{ + match s + case Nil => u := Nil; + case Cons(_, tail) => u := tail; +} + +method Add(t: W, s: Synonym1) returns (u: Synonym1) +{ + u := Cons(t, Nil); +} + +function Skip(s: Synonym3): Synonym0 +{ + match s + case Nil => Nil + case Cons(_, tail) => tail +} diff --git a/Test/dafny0/TypeSynonyms.dfy.expect b/Test/dafny0/TypeSynonyms.dfy.expect new file mode 100644 index 00000000..4ef2de53 --- /dev/null +++ b/Test/dafny0/TypeSynonyms.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 6 verified, 0 errors -- cgit v1.2.3