diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 126 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 90 | ||||
| -rw-r--r-- | Source/Dafny/DafnyMain.cs | 7 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 597 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 58 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 322 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 222 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem1-SumMax.dfy | 4 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem2-Invert.dfy | 4 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 24 | ||||
| -rw-r--r-- | Test/dafny0/Array.dfy | 36 | ||||
| -rw-r--r-- | Test/dafny0/MultiDimArray.dfy | 91 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny1/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny1/MatrixFun.dfy | 59 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 1 | ||||
| -rw-r--r-- | Test/vacid0/LazyInitArray.dfy | 8 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 2 | ||||
| -rw-r--r-- | Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 4 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 2 | ||||
| -rw-r--r-- | Util/vim/syntax/dafny.vim | 2 |
25 files changed, 1054 insertions, 639 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index ad4dcbae..476a6bd9 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -207,7 +207,6 @@ axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): Datatype type ClassName;
const unique class.int: ClassName;
const unique class.bool: ClassName;
-const unique class.object: ClassName;
const unique class.set: ClassName;
const unique class.seq: ClassName;
@@ -273,9 +272,6 @@ function DeclType<T>(Field T) returns (ClassName); // -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
-function Array#Length(ref, int): int;
-axiom (forall r: ref, dim: int :: 0 <= Array#Length(r, dim));
-
procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
modifies $Heap;
ensures $HeapSucc(old($Heap), $Heap);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 8845593c..560c0aea 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -10,7 +10,6 @@ //--------------------------------------------------------------------------*/
using System.Collections.Generic;
-using System.Diagnostics.Contracts;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
@@ -21,7 +20,8 @@ COMPILER Dafny /*--------------------------------------------------------------------------*/
-static List<ModuleDecl/*!*/>/*!*/ theModules = new List<ModuleDecl/*!*/>();
+static List<ModuleDecl/*!*/> theModules;
+static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
@@ -71,17 +71,17 @@ Contract.Ensures(Contract.Result<Expression>() != null); /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
- return Parse(s, filename, modules);
+ return Parse(s, filename, modules, builtIns);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
- return Parse(s, filename, modules);
+ return Parse(s, filename, modules, builtIns);
}
}
}
@@ -92,12 +92,14 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules) {
+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
List<ModuleDecl/*!*/> oldModules = theModules;
theModules = modules;
+ BuiltIns oldBuiltIns = builtIns;
+ theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
@@ -105,6 +107,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Parser parser = new Parser(scanner, errors);
parser.Parse();
theModules = oldModules;
+ theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
@@ -112,6 +115,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
+ posDigit = "123456789".
special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
@@ -123,13 +127,27 @@ CHARACTERS quote = '"'.
nondigit = letter + special.
+ idchar = nondigit + digit.
nonquote = letter + digit + space + glyph.
+ /* exclude the characters in 'array' */
+ nondigitMinusA = nondigit - 'a'.
+ idcharMinusA = idchar - 'a'.
+ idcharMinusR = idchar - 'r'.
+ idcharMinusY = idchar - 'y'.
+ idcharMinusPosDigit = idchar - posDigit.
/*------------------------------------------------------------------------*/
TOKENS
- ident = nondigit {nondigit | digit}.
+ ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
+ | 'a' [ idcharMinusR {idchar} ] /* if char 0 is an 'a', then either there is no char 1 or char 1 is not an 'r' */
+ | 'a' 'r' [ idcharMinusR {idchar} ] /* etc. */
+ | 'a' 'r' 'r' [ idcharMinusA {idchar} ]
+ | 'a' 'r' 'r' 'a' [ idcharMinusY {idchar} ]
+ | 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
+ | 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}.
digits = digit {digit}.
+ arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
string = quote {nonquote} quote.
COMMENTS FROM "/*" TO "*/" NESTED
@@ -495,11 +513,15 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> List<Type/*!*/>/*!*/ gt;
.)
( "object" (. tok = t; ty = new ObjectType(); .)
- | "array" (. tok = t; gt = new List<Type/*!*/>(); .)
+ | arrayToken (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
- ty = UserDefinedType.ArrayType(tok, 1, gt[0]);
+ int dims = 1;
+ if (tok.val.Length != 5) {
+ dims = int.Parse(tok.val.Substring(5));
+ }
+ ty = theBuiltIns.ArrayType(dims, gt[0], true);
.)
| Ident<out tok> (. gt = new List<Type/*!*/>(); .)
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
@@ -690,7 +712,7 @@ OneStmt<out Statement/*!*/ s> AssignStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ lhs;
- Expression rhs;
+ List<Expression> rhs;
Type ty;
s = dummyStmt;
.)
@@ -698,26 +720,34 @@ AssignStmt<out Statement/*!*/ s> ":=" (. x = t; .)
AssignRhs<out rhs, out ty> (. if (ty == null) {
Contract.Assert(rhs != null);
- s = new AssignStmt(x, lhs, rhs);
+ Contract.Assert(rhs.Count == 1);
+ s = new AssignStmt(x, lhs, rhs[0]);
} else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
- s = new AssignStmt(x, lhs, ty, new List<Expression>(new Expression[] { rhs }));
+ s = new AssignStmt(x, lhs, ty, rhs);
}
.)
";"
.
-AssignRhs<out Expression e, out Type ty>
-/* ensures e != null || ty != null; */
-= (. IToken/*!*/ x; Expression/*!*/ ee; Type/*!*/ tt;
- e = null; ty = null;
+AssignRhs<.out List<Expression> ee, out Type ty.>
+/* ensures ee != null || ty != null; */
+/* ensures ee != null ==> 1 <= ee.Count; */
+/* ensures ty == null ==> 1 == ee.Count; */
+= (. IToken/*!*/ x; Expression/*!*/ e;
+ ee = null; ty = null;
.)
- ( "new" TypeAndToken<out x, out tt> (. ty = tt; .)
- [ "[" Expression<out ee> "]" (. e = ee; .)
+ ( "new" TypeAndToken<out x, out ty>
+ [ "[" Expression<out e> (. ee = new List<Expression>(); ee.Add(e); .)
+ { "," Expression<out e> (. ee.Add(e); .)
+ }
+ "]" (. // make sure an array class with this dimensionality exists
+ UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, Type.Int, true);
+ .)
]
- | Expression<out ee> (. e = ee; .)
- ) (. if (e == null && ty == null) { e = dummyExpr; } .)
+ | Expression<out e> (. ee = new List<Expression>(); ee.Add(e); .)
+ ) (. if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); } .)
.
HavocStmt<out Statement/*!*/ s>
@@ -744,7 +774,7 @@ VarDeclStmts<.List<Statement/*!*/>/*!*/ ss.> IdentTypeRhs<out VarDecl/*!*/ d, bool isGhost>
= (. Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
- Expression rhs = null; Type newType = null;
+ List<Expression> rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
.)
Ident<out id>
@@ -754,12 +784,13 @@ IdentTypeRhs<out VarDecl/*!*/ d, bool isGhost> AssignRhs<out rhs, out newType>
]
(. if (newType == null && rhs != null) {
- optionalRhs = new ExprRhs(rhs);
+ Contract.Assert(rhs.Count == 1);
+ optionalRhs = new ExprRhs(rhs[0]);
} else if (newType != null) {
if (rhs == null) {
optionalRhs = new TypeRhs(newType);
} else {
- optionalRhs = new TypeRhs(newType, new List<Expression>(new Expression[] { rhs }));
+ optionalRhs = new TypeRhs(newType, rhs);
}
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
@@ -1174,6 +1205,7 @@ IdentOrFuncExpression<out Expression/*!*/ e> SelectOrCallSuffix<ref Expression/*!*/ e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
+ List<Expression> multipleIndices = null;
bool func = false;
.)
( "."
@@ -1185,29 +1217,41 @@ SelectOrCallSuffix<ref Expression/*!*/ e> | "[" (. x = t; .)
( Expression<out ee> (. e0 = ee; .)
- [ ".." (. anyDots = true; .)
+ ( ".." (. anyDots = true; .)
[ Expression<out ee> (. e1 = ee; .)
]
| ":="
Expression<out ee> (. e1 = ee; .)
- ]
- | ".." Expression<out ee> (. anyDots = true; e1 = ee; .)
- ) (. if (!anyDots && e0 == null) {
- /* a parsing error occurred */
- e0 = dummyExpr;
- }
- Contract.Assert(anyDots || e0 != null);
- if (anyDots) {
- Contract.Assert(e0 != null || e1 != null);
- e = new SeqSelectExpr(x, false, e, e0, e1);
- } else if (e1 == null) {
- Contract.Assert(e0 != null);
- e = new SeqSelectExpr(x, true, e, e0, null);
- } else {
- Contract.Assert(e0 != null);
- e = new SeqUpdateExpr(x, e, e0, e1);
+ | { "," Expression<out ee> (. if (multipleIndices == null) {
+ multipleIndices = new List<Expression>();
+ multipleIndices.Add(e0);
}
+ multipleIndices.Add(ee);
.)
+ }
+ )
+ | ".." Expression<out ee> (. anyDots = true; e1 = ee; .)
+ )
+ (. if (multipleIndices != null) {
+ e = new MultiSelectExpr(x, e, multipleIndices);
+ } else {
+ if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
+ Contract.Assert(anyDots || e0 != null);
+ if (anyDots) {
+ Contract.Assert(e0 != null || e1 != null);
+ e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ Contract.Assert(e0 != null);
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ Contract.Assert(e0 != null);
+ e = new SeqUpdateExpr(x, e, e0, e1);
+ }
+ }
+ .)
"]"
)
.
@@ -1322,7 +1366,7 @@ Idents<.List<string/*!*/>/*!*/ ids.> Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t; .)
- .
+ .
Nat<out BigInteger n>
=
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 8451dd67..f21a5b3e 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -20,11 +20,62 @@ namespace Microsoft.Dafny { public readonly string Name;
public readonly List<ModuleDecl/*!*/>/*!*/ Modules;
- public Program(string name, [Captured] List<ModuleDecl/*!*/>/*!*/ modules) {
+ public readonly BuiltIns BuiltIns;
+ public Program(string name, [Captured] List<ModuleDecl/*!*/>/*!*/ modules, [Captured] BuiltIns builtIns) {
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(modules));
Name = name;
Modules = modules;
+ BuiltIns = builtIns;
+ }
+ }
+
+ public class BuiltIns
+ {
+ public readonly ModuleDecl SystemModule = new ModuleDecl(Token.NoToken, "_System", new List<string>(), null);
+ Dictionary<int, ClassDecl/*!*/> arrayTypeDecls = new Dictionary<int, ClassDecl>();
+
+ public BuiltIns() {
+ // create class 'object'
+ ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
+ SystemModule.TopLevelDecls.Add(obj);
+ // add one-dimensional arrays, since they may arise during type checking
+ UserDefinedType tmp = ArrayType(1, Type.Int, true);
+ }
+
+ public UserDefinedType ArrayType(int dims, Type arg) {
+ return ArrayType(dims, arg, false);
+ }
+ public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
+ Contract.Requires(1 <= dims);
+ Contract.Requires(arg != null);
+ Contract.Ensures(Contract.Result<UserDefinedType>() != null);
+
+ List<Type/*!*/> typeArgs = new List<Type/*!*/>();
+ typeArgs.Add(arg);
+ UserDefinedType udt = new UserDefinedType(Token.NoToken, ArrayClassName(dims), typeArgs);
+ if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
+ ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
+ for (int d = 0; d < dims; d++) {
+ string name = dims == 1 ? "Length" : "Length" + d;
+ Field len = new Field(Token.NoToken, name, false, false, Type.Int, null);
+ len.EnclosingClass = arrayClass; // resolve here
+ arrayClass.Members.Add(len);
+ }
+ arrayTypeDecls.Add(dims, arrayClass);
+ SystemModule.TopLevelDecls.Add(arrayClass);
+ }
+ udt.ResolvedClass = arrayTypeDecls[dims];
+ return udt;
+ }
+
+ public static string ArrayClassName(int dims) {
+ Contract.Requires(1 <= dims);
+ if (dims == 1) {
+ return "array";
+ } else {
+ return "array" + dims;
+ }
}
}
@@ -197,7 +248,6 @@ namespace Microsoft.Dafny { Contract.Invariant(tok != null);
Contract.Invariant(cce.NonNullElements(Name));
Contract.Invariant(cce.NonNullElements(TypeArgs));
- Contract.Invariant(ArrayTypeDecls != null);
}
public readonly IToken tok;
@@ -208,24 +258,6 @@ namespace Microsoft.Dafny { public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public static UserDefinedType ArrayType(IToken tok, int dims, Type arg) {
- Contract.Requires(tok != null);
- Contract.Requires(1 <= dims);
- Contract.Requires(arg != null);
- Contract.Ensures(Contract.Result<UserDefinedType>() != null);
-
- List<Type/*!*/> typeArgs = new List<Type/*!*/>();
- typeArgs.Add(arg);
- UserDefinedType udt = new UserDefinedType(tok, "array" + dims, typeArgs);
- if (!ArrayTypeDecls.ContainsKey(dims)) {
- ArrayTypeDecls.Add(dims, new ArrayClassDecl(dims, _systemModule));
- }
- udt.ResolvedClass = ArrayTypeDecls[dims];
- return udt;
- }
- public static Dictionary<int, ClassDecl/*!*/> ArrayTypeDecls = new Dictionary<int,ClassDecl>();
- static readonly ModuleDecl _systemModule = new ModuleDecl(Token.NoToken, "_System", new List<string>(), null);
-
public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -587,7 +619,6 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Members));
}
-
public ClassDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module,
List<TypeParameter/*!*/>/*!*/ typeArgs, [Captured] List<MemberDecl/*!*/>/*!*/ members, Attributes attributes)
: base(tok, name, module, typeArgs, attributes) {
@@ -644,7 +675,7 @@ namespace Microsoft.Dafny { public class ArrayClassDecl : ClassDecl {
public readonly int Dims;
public ArrayClassDecl(int dims, ModuleDecl module)
- : base(Token.NoToken, "array" + dims, module,
+ : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module,
new List<TypeParameter>(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}),
new List<MemberDecl>(), null)
{
@@ -728,7 +759,6 @@ namespace Microsoft.Dafny { Contract.Requires(EnclosingClass != null);
Contract.Ensures(Contract.Result<string>() != null);
-
return EnclosingClass.Name + "." + Name;
}
}
@@ -736,21 +766,28 @@ namespace Microsoft.Dafny { public class Field : MemberDecl {
public readonly bool IsGhost;
+ public readonly bool IsMutable;
public readonly Type Type;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Type != null);
}
-
public Field(IToken tok, string name, bool isGhost, Type type, Attributes attributes)
+ : this(tok, name, isGhost, true, type, attributes) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
+ }
+
+ public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
IsGhost = isGhost;
+ IsMutable = isMutable;
Type = type;
-
}
}
@@ -1292,7 +1329,6 @@ namespace Microsoft.Dafny { void ObjectInvariant() {
Contract.Invariant(Lhs != null);
Contract.Invariant(Rhs != null);
-
}
public AssignStmt(IToken tok, Expression lhs, Expression rhs)
@@ -1302,7 +1338,6 @@ namespace Microsoft.Dafny { Contract.Requires(rhs != null);
this.Lhs = lhs;
this.Rhs = new ExprRhs(rhs);
-
}
public AssignStmt(IToken tok, Expression lhs, Type type)
: base(tok) { // alloc statement
@@ -1311,7 +1346,6 @@ namespace Microsoft.Dafny { Contract.Requires(type != null);
this.Lhs = lhs;
this.Rhs = new TypeRhs(type);
-
}
public AssignStmt(IToken tok, Expression lhs, Type type, List<Expression> arrayDimensions)
: base(tok) { // array alloc statement
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 893d3b90..a18ea938 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -21,6 +21,7 @@ namespace Microsoft.Dafny { Contract.Requires(fileNames != null);
program = null;
List<ModuleDecl> modules = new List<ModuleDecl>();
+ BuiltIns builtIns = new BuiltIns();
foreach (string dafnyFileName in fileNames){
Contract.Assert(dafnyFileName != null);
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
@@ -34,7 +35,7 @@ namespace Microsoft.Dafny { int errorCount;
try
{
- errorCount = Dafny.Parser.Parse(dafnyFileName, modules);
+ errorCount = Dafny.Parser.Parse(dafnyFileName, modules, builtIns);
if (errorCount != 0)
{
return string.Format("{0} parse errors detected in {1}", errorCount, dafnyFileName);
@@ -46,7 +47,7 @@ namespace Microsoft.Dafny { }
}
- program = new Program(programName, modules);
+ program = new Program(programName, modules, builtIns);
if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {
string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;
@@ -63,7 +64,7 @@ namespace Microsoft.Dafny { if (Bpl.CommandLineOptions.Clo.NoResolve || Bpl.CommandLineOptions.Clo.NoTypecheck) { return null; }
- Dafny.Resolver r = new Dafny.Resolver();
+ Dafny.Resolver r = new Dafny.Resolver(program);
r.ResolveProgram(program);
if (r.ErrorCount != 0) {
return string.Format("{0} resolution/type errors detected in {1}", r.ErrorCount, programName);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index d6a7712d..6577e993 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1,5 +1,4 @@ using System.Collections.Generic;
-using System.Diagnostics.Contracts;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
@@ -19,7 +18,8 @@ public class Parser { public const int _EOF = 0;
public const int _ident = 1;
public const int _digits = 2;
- public const int _string = 3;
+ public const int _arrayToken = 3;
+ public const int _string = 4;
public const int maxT = 103;
const bool T = true;
@@ -33,7 +33,8 @@ public class Parser { public Token/*!*/ la; // lookahead token
int errDist = minErrDist;
-static List<ModuleDecl/*!*/>/*!*/ theModules = new List<ModuleDecl/*!*/>();
+static List<ModuleDecl/*!*/> theModules;
+static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
@@ -83,17 +84,17 @@ Contract.Ensures(Contract.Result<Expression>() != null); /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List<string>());
- return Parse(s, filename, modules);
+ return Parse(s, filename, modules, builtIns);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List<string>());
- return Parse(s, filename, modules);
+ return Parse(s, filename, modules, builtIns);
}
}
}
@@ -104,12 +105,14 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules) {
+public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ modules, BuiltIns builtIns) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(modules));
List<ModuleDecl/*!*/> oldModules = theModules;
theModules = modules;
+ BuiltIns oldBuiltIns = builtIns;
+ theBuiltIns = builtIns;
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
@@ -117,6 +120,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Parser parser = new Parser(scanner, errors);
parser.Parse();
theModules = oldModules;
+ theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
@@ -211,21 +215,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
while (StartOf(1)) {
- if (la.kind == 4) {
+ if (la.kind == 5) {
Get();
attrs = null; theImports = new List<string/*!*/>();
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 5) {
+ if (la.kind == 6) {
Get();
Idents(theImports);
}
module = new ModuleDecl(id, id.val, theImports, attrs);
- Expect(6);
- while (la.kind == 8 || la.kind == 13) {
- if (la.kind == 8) {
+ Expect(7);
+ while (la.kind == 9 || la.kind == 14) {
+ if (la.kind == 9) {
ClassDecl(module, out c);
module.TopLevelDecls.Add(c);
} else {
@@ -234,11 +238,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
}
theModules.Add(module);
- Expect(7);
- } else if (la.kind == 8) {
+ Expect(8);
+ } else if (la.kind == 9) {
ClassDecl(defaultModule, out c);
defaultModule.TopLevelDecls.Add(c);
- } else if (la.kind == 13) {
+ } else if (la.kind == 14) {
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
} else {
@@ -263,9 +267,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
void Attribute(ref Attributes attrs) {
- Expect(6);
- AttributeBody(ref attrs);
Expect(7);
+ AttributeBody(ref attrs);
+ Expect(8);
}
void Ident(out IToken/*!*/ x) {
@@ -278,7 +282,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! IToken/*!*/ id;
Ident(out id);
ids.Add(id.val);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out id);
ids.Add(id.val);
@@ -295,24 +299,24 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! IToken optionalId = null;
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
- Expect(8);
- while (la.kind == 6) {
+ Expect(9);
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericParameters(typeArgs);
}
- if (la.kind == 9) {
+ if (la.kind == 10) {
Get();
Ident(out idRefined);
optionalId = idRefined;
}
- Expect(6);
+ Expect(7);
while (StartOf(2)) {
ClassMemberDecl(members);
}
- Expect(7);
+ Expect(8);
if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
else
@@ -328,19 +332,19 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();
- Expect(13);
- while (la.kind == 6) {
+ Expect(14);
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericParameters(typeArgs);
}
- Expect(6);
- while (la.kind == 1 || la.kind == 6) {
+ Expect(7);
+ while (la.kind == 1 || la.kind == 7) {
DatatypeMemberDecl(ctors);
}
- Expect(7);
+ Expect(8);
dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
@@ -350,11 +354,11 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
- while (la.kind == 10 || la.kind == 11 || la.kind == 12) {
- if (la.kind == 10) {
+ while (la.kind == 11 || la.kind == 12 || la.kind == 13) {
+ if (la.kind == 11) {
Get();
mmod.IsGhost = true;
- } else if (la.kind == 11) {
+ } else if (la.kind == 12) {
Get();
mmod.IsStatic = true;
} else {
@@ -362,15 +366,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! mmod.IsUnlimited = true;
}
}
- if (la.kind == 15) {
+ if (la.kind == 16) {
FieldDecl(mmod, mm);
} else if (la.kind == 37) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 9 || la.kind == 22) {
+ } else if (la.kind == 10 || la.kind == 23) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else if (la.kind == 17) {
+ } else if (la.kind == 18) {
CouplingInvDecl(mmod, mm);
} else SynErr(104);
}
@@ -378,15 +382,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id;
- Expect(20);
+ Expect(21);
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
}
- Expect(21);
+ Expect(22);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -394,21 +398,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- Expect(15);
+ Expect(16);
if (mmod.IsUnlimited) { SemErr(t, "fields cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- Expect(14);
+ Expect(15);
}
void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) {
@@ -425,30 +429,30 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! bool isFunctionMethod = false;
Expect(37);
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, false, formals);
- Expect(19);
+ Expect(20);
Type(out returnType);
- if (la.kind == 14) {
+ if (la.kind == 15) {
Get();
- while (la.kind == 26 || la.kind == 28 || la.kind == 38) {
+ while (la.kind == 27 || la.kind == 29 || la.kind == 38) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(3)) {
- while (la.kind == 26 || la.kind == 28 || la.kind == 38) {
+ while (la.kind == 27 || la.kind == 29 || la.kind == 38) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
@@ -473,28 +477,28 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Statement/*!*/ bb; BlockStmt body = null;
bool isRefinement = false;
- if (la.kind == 22) {
+ if (la.kind == 23) {
Get();
- } else if (la.kind == 9) {
+ } else if (la.kind == 10) {
Get();
isRefinement = true;
} else SynErr(106);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, true, ins);
- if (la.kind == 23) {
+ if (la.kind == 24) {
Get();
Formals(false, true, outs);
}
- if (la.kind == 14) {
+ if (la.kind == 15) {
Get();
while (StartOf(4)) {
MethodSpec(req, mod, ens, dec);
@@ -522,24 +526,24 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Expression/*!*/ e;
parseVarScope.PushMarker();
- Expect(17);
+ Expect(18);
if (mmod.IsUnlimited) { SemErr(t, "coupling invariants cannot be declared 'unlimited'"); }
if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
ids.Add(id); parseVarScope.Push(id.val, id.val);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out id);
ids.Add(id); parseVarScope.Push(id.val, id.val);
}
- Expect(18);
+ Expect(19);
Expression(out e);
- Expect(14);
+ Expect(15);
mm.Add(new CouplingInvariant(ids, e, attrs));
parseVarScope.PopMarker();
@@ -552,42 +556,42 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<Formal/*!*/> formals = new List<Formal/*!*/>();
- while (la.kind == 6) {
+ while (la.kind == 7) {
Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
- if (la.kind == 29) {
+ if (la.kind == 30) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
- Expect(14);
+ Expect(15);
}
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(29);
+ Expect(30);
if (StartOf(6)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost)); parseVarScope.Push(name, name);
}
}
- Expect(30);
+ Expect(31);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
Ident(out id);
- Expect(19);
+ Expect(20);
Type(out ty);
}
@@ -613,7 +617,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
if (allowGhost) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
@@ -629,7 +633,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
Ident(out id);
- if (la.kind == 19) {
+ if (la.kind == 20) {
Get();
Type(out ty);
optType = ty;
@@ -642,12 +646,12 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; isGhost = false;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
isGhost = true;
}
TypeAndToken(out id, out ty);
- if (la.kind == 19) {
+ if (la.kind == 20) {
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
@@ -670,13 +674,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 31) {
+ if (la.kind == 32) {
Get();
tok = t;
- } else if (la.kind == 32) {
+ } else if (la.kind == 33) {
Get();
tok = t; ty = new IntType();
- } else if (la.kind == 33) {
+ } else if (la.kind == 34) {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -685,7 +689,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
ty = new SetType(gt[0]);
- } else if (la.kind == 34) {
+ } else if (la.kind == 35) {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -694,24 +698,24 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! }
ty = new SeqType(gt[0]);
- } else if (la.kind == 1 || la.kind == 35 || la.kind == 36) {
+ } else if (la.kind == 1 || la.kind == 3 || la.kind == 36) {
ReferenceType(out tok, out ty);
} else SynErr(109);
}
void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(29);
- if (la.kind == 1 || la.kind == 10) {
+ Expect(30);
+ if (la.kind == 1 || la.kind == 11) {
GIdentType(allowGhosts, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
GIdentType(allowGhosts, out id, out ty, out isGhost);
formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); parseVarScope.Push(id.val, id.val);
}
}
- Expect(30);
+ Expect(31);
}
void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
@@ -719,38 +723,38 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false;
- if (la.kind == 24) {
+ if (la.kind == 25) {
Get();
if (StartOf(8)) {
FrameExpression(out fe);
mod.Add(fe);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
FrameExpression(out fe);
mod.Add(fe);
}
}
- Expect(14);
- } else if (la.kind == 25 || la.kind == 26 || la.kind == 27) {
- if (la.kind == 25) {
+ Expect(15);
+ } else if (la.kind == 26 || la.kind == 27 || la.kind == 28) {
+ if (la.kind == 26) {
Get();
isFree = true;
}
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
Expression(out e);
- Expect(14);
+ Expect(15);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 27) {
+ } else if (la.kind == 28) {
Get();
Expression(out e);
- Expect(14);
+ Expect(15);
ens.Add(new MaybeFreeExpression(e, isFree));
} else SynErr(110);
- } else if (la.kind == 28) {
+ } else if (la.kind == 29) {
Get();
Expressions(decreases);
- Expect(14);
+ Expect(15);
} else SynErr(111);
}
@@ -759,12 +763,12 @@ List<Expression/*!*/>/*!*/ decreases) { List<Statement/*!*/> body = new List<Statement/*!*/>();
parseVarScope.PushMarker();
- Expect(6);
+ Expect(7);
x = t;
while (StartOf(9)) {
Stmt(body);
}
- Expect(7);
+ Expect(8);
block = new BlockStmt(x, body);
parseVarScope.PopMarker();
}
@@ -784,7 +788,7 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e;
Expression(out e);
args.Add(e);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Expression(out e);
args.Add(e);
@@ -793,15 +797,15 @@ List<Expression/*!*/>/*!*/ decreases) { void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(20);
+ Expect(21);
Type(out ty);
gt.Add(ty);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(21);
+ Expect(22);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -809,22 +813,26 @@ List<Expression/*!*/>/*!*/ decreases) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 35) {
+ if (la.kind == 36) {
Get();
tok = t; ty = new ObjectType();
- } else if (la.kind == 36) {
+ } else if (la.kind == 3) {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
if (gt.Count != 1) {
SemErr("array type expects exactly one type argument");
}
- ty = UserDefinedType.ArrayType(tok, 1, gt[0]);
+ int dims = 1;
+ if (tok.val.Length != 5) {
+ dims = int.Parse(tok.val.Substring(5));
+ }
+ ty = theBuiltIns.ArrayType(dims, gt[0], true);
} else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type/*!*/>();
- if (la.kind == 20) {
+ if (la.kind == 21) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
@@ -834,39 +842,39 @@ List<Expression/*!*/>/*!*/ decreases) { void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 26) {
+ if (la.kind == 27) {
Get();
Expression(out e);
- Expect(14);
+ Expect(15);
reqs.Add(e);
} else if (la.kind == 38) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
}
}
- Expect(14);
- } else if (la.kind == 28) {
+ Expect(15);
+ } else if (la.kind == 29) {
Get();
Expressions(decreases);
- Expect(14);
+ Expect(15);
} else SynErr(113);
}
void FunctionBody(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
- Expect(6);
+ Expect(7);
if (la.kind == 41) {
MatchExpression(out e);
} else if (StartOf(8)) {
Expression(out e);
} else SynErr(114);
- Expect(7);
+ Expect(8);
}
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
@@ -912,18 +920,18 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(42);
x = t; parseVarScope.PushMarker();
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(30);
+ Expect(31);
}
Expect(43);
Expression(out body);
@@ -933,14 +941,14 @@ List<Expression/*!*/>/*!*/ decreases) { void Stmt(List<Statement/*!*/>/*!*/ ss) {
Contract.Requires(cce.NonNullElements(ss)); Statement/*!*/ s;
- while (la.kind == 6) {
+ while (la.kind == 7) {
BlockStmt(out s);
ss.Add(s);
}
if (StartOf(11)) {
OneStmt(out s);
ss.Add(s);
- } else if (la.kind == 10 || la.kind == 15) {
+ } else if (la.kind == 11 || la.kind == 16) {
VarDeclStmts(ss);
} else SynErr(117);
}
@@ -966,7 +974,7 @@ List<Expression/*!*/>/*!*/ decreases) { PrintStmt(out s);
break;
}
- case 1: case 29: case 95: case 96: {
+ case 1: case 30: case 95: case 96: {
AssignStmt(out s);
break;
}
@@ -998,7 +1006,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
x = t;
Ident(out id);
- Expect(19);
+ Expect(20);
s = new LabelStmt(x, id.val);
break;
}
@@ -1009,14 +1017,14 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
label = id.val;
}
- Expect(14);
+ Expect(15);
s = new BreakStmt(x, label);
break;
}
case 46: {
Get();
x = t;
- Expect(14);
+ Expect(15);
s = new ReturnStmt(x);
break;
}
@@ -1026,19 +1034,19 @@ List<Expression/*!*/>/*!*/ decreases) { void VarDeclStmts(List<Statement/*!*/>/*!*/ ss) {
Contract.Requires(cce.NonNullElements(ss)); VarDecl/*!*/ d; bool isGhost = false;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
isGhost = true;
}
- Expect(15);
+ Expect(16);
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
}
- Expect(14);
+ Expect(15);
}
void AssertStmt(out Statement/*!*/ s) {
@@ -1046,7 +1054,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(60);
x = t;
Expression(out e);
- Expect(14);
+ Expect(15);
s = new AssertStmt(x, e);
}
@@ -1055,7 +1063,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(61);
x = t;
Expression(out e);
- Expect(14);
+ Expect(15);
s = new AssumeStmt(x, e);
}
@@ -1064,7 +1072,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(62);
x = t;
Expression(out e);
- Expect(14);
+ Expect(15);
s = new UseStmt(x, e);
}
@@ -1076,19 +1084,19 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
AttributeArg(out arg);
args.Add(arg);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
AttributeArg(out arg);
args.Add(arg);
}
- Expect(14);
+ Expect(15);
s = new PrintStmt(x, args);
}
void AssignStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ lhs;
- Expression rhs;
+ List<Expression> rhs;
Type ty;
s = dummyStmt;
@@ -1098,14 +1106,15 @@ List<Expression/*!*/>/*!*/ decreases) { AssignRhs(out rhs, out ty);
if (ty == null) {
Contract.Assert(rhs != null);
- s = new AssignStmt(x, lhs, rhs);
+ Contract.Assert(rhs.Count == 1);
+ s = new AssignStmt(x, lhs, rhs[0]);
} else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
} else {
- s = new AssignStmt(x, lhs, ty, new List<Expression>(new Expression[] { rhs }));
+ s = new AssignStmt(x, lhs, ty, rhs);
}
- Expect(14);
+ Expect(15);
}
void HavocStmt(out Statement/*!*/ s) {
@@ -1113,7 +1122,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(51);
x = t;
LhsExpr(out lhs);
- Expect(14);
+ Expect(15);
s = new AssignStmt(x, lhs);
}
@@ -1126,8 +1135,8 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(56);
x = t;
CallStmtSubExpr(out e);
- if (la.kind == 16 || la.kind == 47) {
- if (la.kind == 16) {
+ if (la.kind == 17 || la.kind == 47) {
+ if (la.kind == 17) {
Get();
e = ConvertToLocal(e);
if (e is IdentifierExpr) {
@@ -1140,7 +1149,7 @@ List<Expression/*!*/>/*!*/ decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
@@ -1161,7 +1170,7 @@ List<Expression/*!*/>/*!*/ decreases) { CallStmtSubExpr(out e);
}
}
- Expect(14);
+ Expect(15);
if (e is FunctionCallExpr) {
FunctionCallExpr fce = (FunctionCallExpr)e;
s = new CallStmt(x, newVars, lhs, fce.Receiver, fce.Name, fce.Args); // this actually does an ownership transfer of fce.Args
@@ -1188,7 +1197,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (la.kind == 52) {
IfStmt(out s);
els = s;
- } else if (la.kind == 6) {
+ } else if (la.kind == 7) {
BlockStmt(out s);
els = s;
} else SynErr(119);
@@ -1208,27 +1217,27 @@ List<Expression/*!*/>/*!*/ decreases) { x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 25 || la.kind == 28 || la.kind == 55) {
- if (la.kind == 25 || la.kind == 55) {
+ while (la.kind == 26 || la.kind == 29 || la.kind == 55) {
+ if (la.kind == 26 || la.kind == 55) {
isFree = false;
- if (la.kind == 25) {
+ if (la.kind == 26) {
Get();
isFree = true;
}
Expect(55);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
- Expect(14);
+ Expect(15);
} else {
Get();
PossiblyWildExpression(out e);
decreases.Add(e);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
PossiblyWildExpression(out e);
decreases.Add(e);
}
- Expect(14);
+ Expect(15);
}
}
BlockStmt(out body);
@@ -1242,12 +1251,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(41);
x = t;
Expression(out e);
- Expect(6);
+ Expect(7);
while (la.kind == 42) {
CaseStatement(out c);
cases.Add(c);
}
- Expect(7);
+ Expect(8);
s = new MatchStmt(x, e, cases);
}
@@ -1265,9 +1274,9 @@ List<Expression/*!*/>/*!*/ decreases) { range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(29);
+ Expect(30);
Ident(out boundVar);
- if (la.kind == 19) {
+ if (la.kind == 20) {
Get();
Type(out ty);
}
@@ -1278,8 +1287,8 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
Expression(out range);
}
- Expect(30);
- Expect(6);
+ Expect(31);
+ Expect(7);
while (la.kind == 60 || la.kind == 61 || la.kind == 62) {
if (la.kind == 60) {
AssertStmt(out s);
@@ -1299,7 +1308,7 @@ List<Expression/*!*/>/*!*/ decreases) { HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
} else SynErr(120);
- Expect(7);
+ Expect(8);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
} else {
@@ -1314,32 +1323,38 @@ List<Expression/*!*/>/*!*/ decreases) { SelectExpression(out e);
}
- void AssignRhs(out Expression e, out Type ty) {
- IToken/*!*/ x; Expression/*!*/ ee; Type/*!*/ tt;
- e = null; ty = null;
+ void AssignRhs(out List<Expression> ee, out Type ty) {
+ IToken/*!*/ x; Expression/*!*/ e;
+ ee = null; ty = null;
if (la.kind == 48) {
Get();
- TypeAndToken(out x, out tt);
- ty = tt;
+ TypeAndToken(out x, out ty);
if (la.kind == 49) {
Get();
- Expression(out ee);
+ Expression(out e);
+ ee = new List<Expression>(); ee.Add(e);
+ while (la.kind == 17) {
+ Get();
+ Expression(out e);
+ ee.Add(e);
+ }
Expect(50);
- e = ee;
+ UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+
}
} else if (StartOf(8)) {
- Expression(out ee);
- e = ee;
+ Expression(out e);
+ ee = new List<Expression>(); ee.Add(e);
} else SynErr(121);
- if (e == null && ty == null) { e = dummyExpr; }
+ if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); }
}
void SelectExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
+ } else if (la.kind == 30 || la.kind == 95 || la.kind == 96) {
ObjectExpression(out e);
} else SynErr(122);
while (la.kind == 49 || la.kind == 92) {
@@ -1349,11 +1364,11 @@ List<Expression/*!*/>/*!*/ decreases) { void IdentTypeRhs(out VarDecl/*!*/ d, bool isGhost) {
Contract.Ensures(Contract.ValueAtReturn(out d) != null); IToken/*!*/ id; Type/*!*/ ty;
- Expression rhs = null; Type newType = null;
+ List<Expression> rhs = null; Type newType = null;
Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
Ident(out id);
- if (la.kind == 19) {
+ if (la.kind == 20) {
Get();
Type(out ty);
optionalType = ty;
@@ -1363,12 +1378,13 @@ List<Expression/*!*/>/*!*/ decreases) { AssignRhs(out rhs, out newType);
}
if (newType == null && rhs != null) {
- optionalRhs = new ExprRhs(rhs);
+ Contract.Assert(rhs.Count == 1);
+ optionalRhs = new ExprRhs(rhs[0]);
} else if (newType != null) {
if (rhs == null) {
optionalRhs = new TypeRhs(newType);
} else {
- optionalRhs = new TypeRhs(newType, new List<Expression>(new Expression[] { rhs }));
+ optionalRhs = new TypeRhs(newType, rhs);
}
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
@@ -1379,7 +1395,7 @@ List<Expression/*!*/>/*!*/ decreases) { void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- Expect(29);
+ Expect(30);
if (la.kind == 39) {
Get();
e = null;
@@ -1387,7 +1403,7 @@ List<Expression/*!*/>/*!*/ decreases) { Expression(out ee);
e = ee;
} else SynErr(123);
- Expect(30);
+ Expect(31);
}
void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -1399,18 +1415,18 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(42);
x = t; parseVarScope.PushMarker();
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(30);
+ Expect(31);
}
Expect(43);
parseVarScope.PushMarker();
@@ -1426,7 +1442,7 @@ List<Expression/*!*/>/*!*/ decreases) { Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr;
if (la.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (la.kind == 29 || la.kind == 95 || la.kind == 96) {
+ } else if (la.kind == 30 || la.kind == 95 || la.kind == 96) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
} else SynErr(124);
@@ -1437,7 +1453,7 @@ List<Expression/*!*/>/*!*/ decreases) { void AttributeArg(out Attributes.Argument/*!*/ arg) {
Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg;
- if (la.kind == 3) {
+ if (la.kind == 4) {
Get();
arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
} else if (StartOf(8)) {
@@ -1558,12 +1574,12 @@ List<Expression/*!*/>/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Eq;
break;
}
- case 20: {
+ case 21: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 21: {
+ case 22: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
@@ -1711,12 +1727,12 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(92);
Ident(out id);
elements = new List<Expression/*!*/>();
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
if (StartOf(8)) {
Expressions(elements);
}
- Expect(30);
+ Expect(31);
}
e = new DatatypeValue(t, dtName.val, id.val, elements);
break;
@@ -1724,9 +1740,9 @@ List<Expression/*!*/>/*!*/ decreases) { case 93: {
Get();
x = t;
- Expect(29);
- Expression(out e);
Expect(30);
+ Expression(out e);
+ Expect(31);
e = new FreshExpr(x, e);
break;
}
@@ -1738,14 +1754,14 @@ List<Expression/*!*/>/*!*/ decreases) { Expect(59);
break;
}
- case 6: {
+ case 7: {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
- Expect(7);
+ Expect(8);
break;
}
case 49: {
@@ -1776,13 +1792,13 @@ List<Expression/*!*/>/*!*/ decreases) { void IdentOrFuncExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ id; e = dummyExpr; List<Expression/*!*/>/*!*/ args;
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
args = new List<Expression/*!*/>();
if (StartOf(8)) {
Expressions(args);
}
- Expect(30);
+ Expect(31);
e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
@@ -1803,36 +1819,37 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 96) {
Get();
x = t;
- Expect(29);
- Expression(out e);
Expect(30);
+ Expression(out e);
+ Expect(31);
e = new OldExpr(x, e);
- } else if (la.kind == 29) {
+ } else if (la.kind == 30) {
Get();
if (StartOf(16)) {
QuantifierGuts(out e);
} else if (StartOf(8)) {
Expression(out e);
} else SynErr(136);
- Expect(30);
+ Expect(31);
} else SynErr(137);
}
void SelectOrCallSuffix(ref Expression/*!*/ e) {
Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
+ List<Expression> multipleIndices = null;
bool func = false;
if (la.kind == 92) {
Get();
Ident(out id);
- if (la.kind == 29) {
+ if (la.kind == 30) {
Get();
args = new List<Expression/*!*/>(); func = true;
if (StartOf(8)) {
Expressions(args);
}
- Expect(30);
+ Expect(31);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
@@ -1842,43 +1859,56 @@ List<Expression/*!*/>/*!*/ decreases) { if (StartOf(8)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 47 || la.kind == 94) {
- if (la.kind == 94) {
- Get();
- anyDots = true;
- if (StartOf(8)) {
- Expression(out ee);
- e1 = ee;
- }
- } else {
- Get();
+ if (la.kind == 94) {
+ Get();
+ anyDots = true;
+ if (StartOf(8)) {
Expression(out ee);
e1 = ee;
}
- }
+ } else if (la.kind == 47) {
+ Get();
+ Expression(out ee);
+ e1 = ee;
+ } else if (la.kind == 17 || la.kind == 50) {
+ while (la.kind == 17) {
+ Get();
+ Expression(out ee);
+ if (multipleIndices == null) {
+ multipleIndices = new List<Expression>();
+ multipleIndices.Add(e0);
+ }
+ multipleIndices.Add(ee);
+
+ }
+ } else SynErr(138);
} else if (la.kind == 94) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(138);
- if (!anyDots && e0 == null) {
- /* a parsing error occurred */
- e0 = dummyExpr;
- }
- Contract.Assert(anyDots || e0 != null);
- if (anyDots) {
- Contract.Assert(e0 != null || e1 != null);
- e = new SeqSelectExpr(x, false, e, e0, e1);
- } else if (e1 == null) {
- Contract.Assert(e0 != null);
- e = new SeqSelectExpr(x, true, e, e0, null);
+ } else SynErr(139);
+ if (multipleIndices != null) {
+ e = new MultiSelectExpr(x, e, multipleIndices);
} else {
- Contract.Assert(e0 != null);
- e = new SeqUpdateExpr(x, e, e0, e1);
+ if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
+ Contract.Assert(anyDots || e0 != null);
+ if (anyDots) {
+ Contract.Assert(e0 != null || e1 != null);
+ e = new SeqSelectExpr(x, false, e, e0, e1);
+ } else if (e1 == null) {
+ Contract.Assert(e0 != null);
+ e = new SeqSelectExpr(x, true, e, e0, null);
+ } else {
+ Contract.Assert(e0 != null);
+ e = new SeqUpdateExpr(x, e, e0, e1);
+ }
}
Expect(50);
- } else SynErr(139);
+ } else SynErr(140);
}
void QuantifierGuts(out Expression/*!*/ q) {
@@ -1896,16 +1926,16 @@ List<Expression/*!*/>/*!*/ decreases) { } else if (la.kind == 99 || la.kind == 100) {
Exists();
x = t;
- } else SynErr(140);
+ } else SynErr(141);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
}
- while (la.kind == 6) {
+ while (la.kind == 7) {
AttributeOrTrigger(ref attrs, ref trigs);
}
QSep();
@@ -1924,7 +1954,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 98) {
Get();
- } else SynErr(141);
+ } else SynErr(142);
}
void Exists() {
@@ -1932,21 +1962,21 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 100) {
Get();
- } else SynErr(142);
+ } else SynErr(143);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
List<Expression/*!*/> es = new List<Expression/*!*/>();
- Expect(6);
- if (la.kind == 19) {
+ Expect(7);
+ if (la.kind == 20) {
AttributeBody(ref attrs);
} else if (StartOf(8)) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(143);
- Expect(7);
+ } else SynErr(144);
+ Expect(8);
}
void QSep() {
@@ -1954,7 +1984,7 @@ List<Expression/*!*/>/*!*/ decreases) { Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(144);
+ } else SynErr(145);
}
void AttributeBody(ref Attributes attrs) {
@@ -1962,13 +1992,13 @@ List<Expression/*!*/>/*!*/ decreases) { List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
Attributes.Argument/*!*/ aArg;
- Expect(19);
+ Expect(20);
Expect(1);
aName = t.val;
if (StartOf(17)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (la.kind == 16) {
+ while (la.kind == 17) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -1990,23 +2020,23 @@ List<Expression/*!*/>/*!*/ decreases) { static readonly bool[,]/*!*/ set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,T, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,T, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,T,x, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x}
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x}
};
} // end Parser
@@ -2026,40 +2056,40 @@ public class Errors { case 0: s = "EOF expected"; break;
case 1: s = "ident expected"; break;
case 2: s = "digits expected"; break;
- case 3: s = "string expected"; break;
- case 4: s = "\"module\" expected"; break;
- case 5: s = "\"imports\" expected"; break;
- case 6: s = "\"{\" expected"; break;
- case 7: s = "\"}\" expected"; break;
- case 8: s = "\"class\" expected"; break;
- case 9: s = "\"refines\" expected"; break;
- case 10: s = "\"ghost\" expected"; break;
- case 11: s = "\"static\" expected"; break;
- case 12: s = "\"unlimited\" expected"; break;
- case 13: s = "\"datatype\" expected"; break;
- case 14: s = "\";\" expected"; break;
- case 15: s = "\"var\" expected"; break;
- case 16: s = "\",\" expected"; break;
- case 17: s = "\"replaces\" expected"; break;
- case 18: s = "\"by\" expected"; break;
- case 19: s = "\":\" expected"; break;
- case 20: s = "\"<\" expected"; break;
- case 21: s = "\">\" expected"; break;
- case 22: s = "\"method\" expected"; break;
- case 23: s = "\"returns\" expected"; break;
- case 24: s = "\"modifies\" expected"; break;
- case 25: s = "\"free\" expected"; break;
- case 26: s = "\"requires\" expected"; break;
- case 27: s = "\"ensures\" expected"; break;
- case 28: s = "\"decreases\" expected"; break;
- case 29: s = "\"(\" expected"; break;
- case 30: s = "\")\" expected"; break;
- case 31: s = "\"bool\" expected"; break;
- case 32: s = "\"int\" expected"; break;
- case 33: s = "\"set\" expected"; break;
- case 34: s = "\"seq\" expected"; break;
- case 35: s = "\"object\" expected"; break;
- case 36: s = "\"array\" expected"; break;
+ case 3: s = "arrayToken expected"; break;
+ case 4: s = "string expected"; break;
+ case 5: s = "\"module\" expected"; break;
+ case 6: s = "\"imports\" expected"; break;
+ case 7: s = "\"{\" expected"; break;
+ case 8: s = "\"}\" expected"; break;
+ case 9: s = "\"class\" expected"; break;
+ case 10: s = "\"refines\" expected"; break;
+ case 11: s = "\"ghost\" expected"; break;
+ case 12: s = "\"static\" expected"; break;
+ case 13: s = "\"unlimited\" expected"; break;
+ case 14: s = "\"datatype\" expected"; break;
+ case 15: s = "\";\" expected"; break;
+ case 16: s = "\"var\" expected"; break;
+ case 17: s = "\",\" expected"; break;
+ case 18: s = "\"replaces\" expected"; break;
+ case 19: s = "\"by\" expected"; break;
+ case 20: s = "\":\" expected"; break;
+ case 21: s = "\"<\" expected"; break;
+ case 22: s = "\">\" expected"; break;
+ case 23: s = "\"method\" expected"; break;
+ case 24: s = "\"returns\" expected"; break;
+ case 25: s = "\"modifies\" expected"; break;
+ case 26: s = "\"free\" expected"; break;
+ case 27: s = "\"requires\" expected"; break;
+ case 28: s = "\"ensures\" expected"; break;
+ case 29: s = "\"decreases\" expected"; break;
+ case 30: s = "\"(\" expected"; break;
+ case 31: s = "\")\" expected"; break;
+ case 32: s = "\"bool\" expected"; break;
+ case 33: s = "\"int\" expected"; break;
+ case 34: s = "\"set\" expected"; break;
+ case 35: s = "\"seq\" expected"; break;
+ case 36: s = "\"object\" expected"; break;
case 37: s = "\"function\" expected"; break;
case 38: s = "\"reads\" expected"; break;
case 39: s = "\"*\" expected"; break;
@@ -2163,11 +2193,12 @@ public class Errors { case 137: s = "invalid ObjectExpression"; break;
case 138: s = "invalid SelectOrCallSuffix"; break;
case 139: s = "invalid SelectOrCallSuffix"; break;
- case 140: s = "invalid QuantifierGuts"; break;
- case 141: s = "invalid Forall"; break;
- case 142: s = "invalid Exists"; break;
- case 143: s = "invalid AttributeOrTrigger"; break;
- case 144: s = "invalid QSep"; break;
+ case 140: s = "invalid SelectOrCallSuffix"; break;
+ case 141: s = "invalid QuantifierGuts"; break;
+ case 142: s = "invalid Forall"; break;
+ case 143: s = "invalid Exists"; break;
+ case 144: s = "invalid AttributeOrTrigger"; break;
+ case 145: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 31c43a44..1e355f63 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -14,10 +14,10 @@ namespace Microsoft.Dafny { class Printer {
TextWriter wr;
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
-}
+ void ObjectInvariant()
+ {
+ Contract.Invariant(wr!=null);
+ }
public Printer(TextWriter wr) {
Contract.Requires(wr != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c3dceb97..2c1a9175 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -43,21 +43,26 @@ namespace Microsoft.Dafny { Contract.Requires(msg != null);
Error(e.tok, msg, args);
}
-
+
+ readonly BuiltIns builtIns;
readonly Dictionary<string/*!*/,TopLevelDecl/*!*/>/*!*/ classes = new Dictionary<string/*!*/,TopLevelDecl/*!*/>();
readonly Dictionary<ClassDecl/*!*/,Dictionary<string/*!*/,MemberDecl/*!*/>/*!*/>/*!*/ classMembers = new Dictionary<ClassDecl/*!*/,Dictionary<string/*!*/,MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/,Dictionary<string/*!*/,DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/,Dictionary<string/*!*/,DatatypeCtor/*!*/>/*!*/>();
readonly Graph<ModuleDecl/*!*/>/*!*/ importGraph = new Graph<ModuleDecl/*!*/>();
-
+
+ public Resolver(Program prog) {
+ Contract.Requires(prog != null);
+ builtIns = prog.BuiltIns;
+ }
+
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(cce.NonNullElements(classes));
+ void ObjectInvariant() {
+ Contract.Invariant(builtIns != null);
+ Contract.Invariant(cce.NonNullElements(classes));
Contract.Invariant(cce.NonNullElements(importGraph));
- Contract.Invariant(cce.NonNullElements(classMembers) && Contract.ForAll(classMembers.Values, v=> cce.NonNullElements(v)));
- Contract.Invariant(cce.NonNullElements(datatypeCtors)&&Contract.ForAll(datatypeCtors.Values, v=> cce.NonNullElements(v)));
-
-}
+ Contract.Invariant(cce.NonNullElements(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullElements(v)));
+ Contract.Invariant(cce.NonNullElements(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullElements(v)));
+ }
bool checkRefinements = true; // used to indicate a cycle in refinements
@@ -73,6 +78,7 @@ void ObjectInvariant() }
}
// resolve imports and register top-level declarations
+ RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls);
Graph<TopLevelDecl> refines = new Graph<TopLevelDecl>();
foreach (ModuleDecl m in prog.Modules) {
importGraph.AddVertex(m);
@@ -174,11 +180,11 @@ void ObjectInvariant() if (d is ClassDecl) {
ClassDecl cl = (ClassDecl)d;
-
+
// register the names of the class members
- Dictionary<string,MemberDecl> members = new Dictionary<string,MemberDecl>();
+ Dictionary<string, MemberDecl> members = new Dictionary<string, MemberDecl>();
classMembers.Add(cl, members);
-
+
foreach (MemberDecl m in cl.Members) {
if (members.ContainsKey(m.Name)) {
Error(m, "Duplicate member name: {0}", m.Name);
@@ -186,6 +192,7 @@ void ObjectInvariant() members.Add(m.Name, m);
}
}
+
} else {
DatatypeDecl dt = (DatatypeDecl)d;
@@ -203,7 +210,7 @@ void ObjectInvariant() }
}
}
-
+
public void ResolveTopLevelRefinement(ClassRefinementDecl decl) {
Contract.Requires(decl != null);
if (!classes.ContainsKey(decl.RefinedClass.val)) {
@@ -326,7 +333,7 @@ void ObjectInvariant() if (currentClass is ClassRefinementDecl) {
ClassDecl refined = ((ClassRefinementDecl)currentClass).Refined;
if (refined != null) {
- Contract.Assert( classMembers.ContainsKey(refined));
+ Contract.Assert(classMembers.ContainsKey(refined));
// there is a member with the same name in refined class if and only if the member is a refined method
if ((member is MethodRefinement) != (classMembers[refined].ContainsKey(member.Name)))
@@ -983,7 +990,7 @@ void ObjectInvariant() return true;
} else if (b is IndexableTypeProxy) {
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
- a.T = UserDefinedType.ArrayType(Token.NoToken, 1, ((IndexableTypeProxy)b).Arg);
+ a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);
b.T = a.T;
return true;
} else {
@@ -1159,6 +1166,9 @@ void ObjectInvariant() }
}
}
+ if (!fse.Field.IsMutable) {
+ Error(stmt, "LHS of assignment does not denote a mutable field");
+ }
}
}
} else if (s.Lhs is SeqSelectExpr) {
@@ -1167,7 +1177,7 @@ void ObjectInvariant() if (lhsResolvedSuccessfully) {
Contract.Assert( lhs.Seq.Type != null);
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(lhs.Seq.Type, UserDefinedType.ArrayType(Token.NoToken, 1, elementType))) {
+ if (!UnifyTypes(lhs.Seq.Type, builtIns.ArrayType(1, elementType))) {
Error(lhs.Seq, "LHS of array assignment must denote an array element (found {0})", lhs.Seq.Type);
}
if (specContextOnly) {
@@ -1194,10 +1204,10 @@ void ObjectInvariant() if (s.Rhs is ExprRhs) {
ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, true, lvalueIsGhost);
- Contract.Assert( rr.Expr.Type != null); // follows from postcondition of ResolveExpression
+ Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
Type lhsType = s.Lhs.Type;
if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
- Contract.Assert( lhsType.IsArrayType);
+ Contract.Assert(lhsType.IsArrayType);
lhsType = UserDefinedType.ArrayElementType(lhsType);
}
if (!UnifyTypes(lhsType, rr.Expr.Type)) {
@@ -1579,7 +1589,7 @@ void ObjectInvariant() }
i++;
}
- return UserDefinedType.ArrayType(stmt.Tok, rr.ArrayDimensions.Count, rr.EType);
+ return builtIns.ArrayType(rr.ArrayDimensions.Count, rr.EType);
}
}
@@ -1588,7 +1598,7 @@ void ObjectInvariant() Contract.Requires(tok != null);
Contract.Requires(receiverType != null);
Contract.Requires(memberName != null);
- Contract.Ensures( Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out ctype) != null && ctype.ResolvedClass != null);
+ Contract.Ensures(Contract.Result<MemberDecl>() == null || Contract.ValueAtReturn(out ctype) != null && ctype.ResolvedClass != null);
ctype = UserDefinedType.DenotesClass(receiverType);
if (ctype == null) {
@@ -1837,7 +1847,7 @@ void ObjectInvariant() ResolveExpression(e.Array, twoState, specContext);
Contract.Assert(e.Array.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Array.Type, UserDefinedType.ArrayType(Token.NoToken, 1, elementType))) {
+ if (!UnifyTypes(e.Array.Type, builtIns.ArrayType(e.Indices.Count, elementType))) {
Error(e.Array, "array selection requires an array (got {0})", e.Array.Type);
}
int i = 0;
@@ -1856,7 +1866,7 @@ void ObjectInvariant() SeqUpdateExpr e = (SeqUpdateExpr)expr;
bool seqErr = false;
ResolveExpression(e.Seq, twoState, specContext);
- Contract.Assert( e.Seq.Type != null); // follows from postcondition of ResolveExpression
+ Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
Error(expr, "sequence update requires a sequence (got {0})", e.Seq.Type);
@@ -1988,8 +1998,8 @@ void ObjectInvariant() expr.Type = Type.Bool;
break;
case UnaryExpr.Opcode.SeqLength:
- if (!UnifyTypes(e.E.Type, new IndexableTypeProxy(new InferredTypeProxy()))) {
- Error(expr, "length operator expects a sequence or array argument (instead got {0})", e.E.Type);
+ if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
+ Error(expr, "length operator expects a sequence argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Int;
break;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index b7224070..75d301a4 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -250,43 +250,44 @@ void objectInvariant(){ for (int i = 65; i <= 90; ++i) start[i] = 1;
for (int i = 92; i <= 92; ++i) start[i] = 1;
for (int i = 95; i <= 95; ++i) start[i] = 1;
- for (int i = 97; i <= 122; ++i) start[i] = 1;
- for (int i = 48; i <= 57; ++i) start[i] = 2;
- for (int i = 34; i <= 34; ++i) start[i] = 3;
- start[123] = 5;
- start[125] = 6;
- start[59] = 7;
- start[44] = 8;
- start[58] = 46;
- start[60] = 47;
- start[62] = 48;
- start[40] = 9;
- start[41] = 10;
- start[42] = 11;
- start[96] = 12;
- start[61] = 49;
- start[91] = 15;
- start[93] = 16;
- start[124] = 50;
- start[8660] = 19;
- start[8658] = 21;
- start[38] = 22;
- start[8743] = 24;
- start[8744] = 26;
- start[33] = 51;
- start[8800] = 32;
- start[8804] = 33;
- start[8805] = 34;
- start[43] = 35;
- start[45] = 36;
- start[47] = 37;
- start[37] = 38;
- start[172] = 39;
- start[35] = 40;
- start[46] = 52;
- start[8704] = 42;
- start[8707] = 43;
- start[8226] = 45;
+ for (int i = 98; i <= 122; ++i) start[i] = 1;
+ for (int i = 48; i <= 57; ++i) start[i] = 7;
+ for (int i = 34; i <= 34; ++i) start[i] = 8;
+ start[97] = 10;
+ start[123] = 17;
+ start[125] = 18;
+ start[59] = 19;
+ start[44] = 20;
+ start[58] = 58;
+ start[60] = 59;
+ start[62] = 60;
+ start[40] = 21;
+ start[41] = 22;
+ start[42] = 23;
+ start[96] = 24;
+ start[61] = 61;
+ start[91] = 27;
+ start[93] = 28;
+ start[124] = 62;
+ start[8660] = 31;
+ start[8658] = 33;
+ start[38] = 34;
+ start[8743] = 36;
+ start[8744] = 38;
+ start[33] = 63;
+ start[8800] = 44;
+ start[8804] = 45;
+ start[8805] = 46;
+ start[43] = 47;
+ start[45] = 48;
+ start[47] = 49;
+ start[37] = 50;
+ start[172] = 51;
+ start[35] = 52;
+ start[46] = 64;
+ start[8704] = 54;
+ start[8707] = 55;
+ start[8226] = 57;
start[Buffer.EOF] = -1;
}
@@ -486,30 +487,29 @@ void objectInvariant(){ void CheckLiteral() {
switch (t.val) {
- case "module": t.kind = 4; break;
- case "imports": t.kind = 5; break;
- case "class": t.kind = 8; break;
- case "refines": t.kind = 9; break;
- case "ghost": t.kind = 10; break;
- case "static": t.kind = 11; break;
- case "unlimited": t.kind = 12; break;
- case "datatype": t.kind = 13; break;
- case "var": t.kind = 15; break;
- case "replaces": t.kind = 17; break;
- case "by": t.kind = 18; break;
- case "method": t.kind = 22; break;
- case "returns": t.kind = 23; break;
- case "modifies": t.kind = 24; break;
- case "free": t.kind = 25; break;
- case "requires": t.kind = 26; break;
- case "ensures": t.kind = 27; break;
- case "decreases": t.kind = 28; break;
- case "bool": t.kind = 31; break;
- case "int": t.kind = 32; break;
- case "set": t.kind = 33; break;
- case "seq": t.kind = 34; break;
- case "object": t.kind = 35; break;
- case "array": t.kind = 36; break;
+ case "module": t.kind = 5; break;
+ case "imports": t.kind = 6; break;
+ case "class": t.kind = 9; break;
+ case "refines": t.kind = 10; break;
+ case "ghost": t.kind = 11; break;
+ case "static": t.kind = 12; break;
+ case "unlimited": t.kind = 13; break;
+ case "datatype": t.kind = 14; break;
+ case "var": t.kind = 16; break;
+ case "replaces": t.kind = 18; break;
+ case "by": t.kind = 19; break;
+ case "method": t.kind = 23; break;
+ case "returns": t.kind = 24; break;
+ case "modifies": t.kind = 25; break;
+ case "free": t.kind = 26; break;
+ case "requires": t.kind = 27; break;
+ case "ensures": t.kind = 28; break;
+ case "decreases": t.kind = 29; break;
+ case "bool": t.kind = 32; break;
+ case "int": t.kind = 33; break;
+ case "set": t.kind = 34; break;
+ case "seq": t.kind = 35; break;
+ case "object": t.kind = 36; break;
case "function": t.kind = 37; break;
case "reads": t.kind = 38; break;
case "match": t.kind = 41; break;
@@ -573,138 +573,192 @@ void objectInvariant(){ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 1;}
else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 2:
- recEnd = pos; recKind = 2;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 2;}
- else {t.kind = 2; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 2;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 3:
- if (ch == '"') {AddCh(); goto case 4;}
- else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 3;}
- else {goto case 0;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 3;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 4:
- {t.kind = 3; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 4;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 5:
- {t.kind = 6; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 5;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 6:
- {t.kind = 7; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 7:
- {t.kind = 14; break;}
+ recEnd = pos; recKind = 2;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 7;}
+ else {t.kind = 2; break;}
case 8:
- {t.kind = 16; break;}
+ if (ch == '"') {AddCh(); goto case 9;}
+ else if (ch >= ' ' && ch <= '!' || ch >= '#' && ch <= '~') {AddCh(); goto case 8;}
+ else {goto case 0;}
case 9:
- {t.kind = 29; break;}
+ {t.kind = 4; break;}
case 10:
- {t.kind = 30; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 2;}
+ else if (ch == 'r') {AddCh(); goto case 12;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 11:
- {t.kind = 39; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 11;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 12:
- {t.kind = 40; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'q' || ch >= 's' && ch <= 'z') {AddCh(); goto case 3;}
+ else if (ch == 'r') {AddCh(); goto case 13;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 13:
- {t.kind = 43; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'b' && ch <= 'z') {AddCh(); goto case 4;}
+ else if (ch == 'a') {AddCh(); goto case 14;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 14:
- {t.kind = 47; break;}
+ recEnd = pos; recKind = 1;
+ if (ch == 39 || ch >= '0' && ch <= '9' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'x' || ch == 'z') {AddCh(); goto case 5;}
+ else if (ch == 'y') {AddCh(); goto case 15;}
+ else {t.kind = 1; t.val = new String(tval, 0, tlen); CheckLiteral(); return t;}
case 15:
- {t.kind = 49; break;}
+ recEnd = pos; recKind = 3;
+ if (ch == 39 || ch == '0' || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 6;}
+ else if (ch >= '1' && ch <= '9') {AddCh(); goto case 16;}
+ else {t.kind = 3; break;}
case 16:
- {t.kind = 50; break;}
+ recEnd = pos; recKind = 3;
+ if (ch == 39 || ch == '?' || ch >= 'A' && ch <= 'Z' || ch == 92 || ch == '_' || ch >= 'a' && ch <= 'z') {AddCh(); goto case 11;}
+ else if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
+ else {t.kind = 3; break;}
case 17:
- if (ch == '>') {AddCh(); goto case 18;}
- else {goto case 0;}
+ {t.kind = 7; break;}
case 18:
- {t.kind = 65; break;}
+ {t.kind = 8; break;}
case 19:
- {t.kind = 66; break;}
+ {t.kind = 15; break;}
case 20:
- {t.kind = 67; break;}
+ {t.kind = 17; break;}
case 21:
- {t.kind = 68; break;}
+ {t.kind = 30; break;}
case 22:
- if (ch == '&') {AddCh(); goto case 23;}
- else {goto case 0;}
+ {t.kind = 31; break;}
case 23:
- {t.kind = 69; break;}
+ {t.kind = 39; break;}
case 24:
- {t.kind = 70; break;}
+ {t.kind = 40; break;}
case 25:
- {t.kind = 71; break;}
+ {t.kind = 43; break;}
case 26:
- {t.kind = 72; break;}
+ {t.kind = 47; break;}
case 27:
- {t.kind = 75; break;}
+ {t.kind = 49; break;}
case 28:
- {t.kind = 76; break;}
+ {t.kind = 50; break;}
case 29:
- {t.kind = 77; break;}
- case 30:
- if (ch == 'n') {AddCh(); goto case 31;}
+ if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
+ case 30:
+ {t.kind = 65; break;}
case 31:
- {t.kind = 78; break;}
+ {t.kind = 66; break;}
case 32:
- {t.kind = 79; break;}
+ {t.kind = 67; break;}
case 33:
- {t.kind = 80; break;}
+ {t.kind = 68; break;}
case 34:
- {t.kind = 81; break;}
+ if (ch == '&') {AddCh(); goto case 35;}
+ else {goto case 0;}
case 35:
- {t.kind = 82; break;}
+ {t.kind = 69; break;}
case 36:
- {t.kind = 83; break;}
+ {t.kind = 70; break;}
case 37:
- {t.kind = 84; break;}
+ {t.kind = 71; break;}
case 38:
- {t.kind = 85; break;}
+ {t.kind = 72; break;}
case 39:
- {t.kind = 87; break;}
+ {t.kind = 75; break;}
case 40:
- {t.kind = 91; break;}
+ {t.kind = 76; break;}
case 41:
- {t.kind = 94; break;}
+ {t.kind = 77; break;}
case 42:
- {t.kind = 98; break;}
+ if (ch == 'n') {AddCh(); goto case 43;}
+ else {goto case 0;}
case 43:
- {t.kind = 100; break;}
+ {t.kind = 78; break;}
case 44:
- {t.kind = 101; break;}
+ {t.kind = 79; break;}
case 45:
- {t.kind = 102; break;}
+ {t.kind = 80; break;}
case 46:
- recEnd = pos; recKind = 19;
- if (ch == '=') {AddCh(); goto case 14;}
- else if (ch == ':') {AddCh(); goto case 44;}
- else {t.kind = 19; break;}
+ {t.kind = 81; break;}
case 47:
+ {t.kind = 82; break;}
+ case 48:
+ {t.kind = 83; break;}
+ case 49:
+ {t.kind = 84; break;}
+ case 50:
+ {t.kind = 85; break;}
+ case 51:
+ {t.kind = 87; break;}
+ case 52:
+ {t.kind = 91; break;}
+ case 53:
+ {t.kind = 94; break;}
+ case 54:
+ {t.kind = 98; break;}
+ case 55:
+ {t.kind = 100; break;}
+ case 56:
+ {t.kind = 101; break;}
+ case 57:
+ {t.kind = 102; break;}
+ case 58:
recEnd = pos; recKind = 20;
- if (ch == '=') {AddCh(); goto case 53;}
+ if (ch == '=') {AddCh(); goto case 26;}
+ else if (ch == ':') {AddCh(); goto case 56;}
else {t.kind = 20; break;}
- case 48:
+ case 59:
recEnd = pos; recKind = 21;
- if (ch == '=') {AddCh(); goto case 27;}
+ if (ch == '=') {AddCh(); goto case 65;}
else {t.kind = 21; break;}
- case 49:
- if (ch == '>') {AddCh(); goto case 13;}
- else if (ch == '=') {AddCh(); goto case 54;}
+ case 60:
+ recEnd = pos; recKind = 22;
+ if (ch == '=') {AddCh(); goto case 39;}
+ else {t.kind = 22; break;}
+ case 61:
+ if (ch == '>') {AddCh(); goto case 25;}
+ else if (ch == '=') {AddCh(); goto case 66;}
else {goto case 0;}
- case 50:
+ case 62:
recEnd = pos; recKind = 59;
- if (ch == '|') {AddCh(); goto case 25;}
+ if (ch == '|') {AddCh(); goto case 37;}
else {t.kind = 59; break;}
- case 51:
+ case 63:
recEnd = pos; recKind = 86;
- if (ch == '=') {AddCh(); goto case 28;}
- else if (ch == '!') {AddCh(); goto case 29;}
- else if (ch == 'i') {AddCh(); goto case 30;}
+ if (ch == '=') {AddCh(); goto case 40;}
+ else if (ch == '!') {AddCh(); goto case 41;}
+ else if (ch == 'i') {AddCh(); goto case 42;}
else {t.kind = 86; break;}
- case 52:
+ case 64:
recEnd = pos; recKind = 92;
- if (ch == '.') {AddCh(); goto case 41;}
+ if (ch == '.') {AddCh(); goto case 53;}
else {t.kind = 92; break;}
- case 53:
+ case 65:
recEnd = pos; recKind = 74;
- if (ch == '=') {AddCh(); goto case 17;}
+ if (ch == '=') {AddCh(); goto case 29;}
else {t.kind = 74; break;}
- case 54:
+ case 66:
recEnd = pos; recKind = 73;
- if (ch == '>') {AddCh(); goto case 20;}
+ if (ch == '>') {AddCh(); goto case 32;}
else {t.kind = 73; break;}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 6d106855..55769d0f 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -29,6 +29,7 @@ namespace Microsoft.Dafny { // translation state
readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
+ readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
// Machinery for providing information to the Counterexample Visualizer
readonly Dictionary<string/*!*/,int>/*!*/ cevFilenames = new Dictionary<string/*!*/,int>();
@@ -40,6 +41,7 @@ namespace Microsoft.Dafny { {
Contract.Invariant(cce.NonNullElements(classes));
Contract.Invariant(cce.NonNullElements(fields));
+ Contract.Invariant(cce.NonNullElements(fieldFunctions));
Contract.Invariant(cce.NonNullElements(cevFilenames));
Contract.Invariant(cce.NonNullElements(cevLocations));
Contract.Invariant(cce.NonNullElements(cevVariables));
@@ -126,9 +128,8 @@ namespace Microsoft.Dafny { public readonly Bpl.Expr Null;
private readonly Bpl.Constant allocField;
[ContractInvariantMethod]
- void ObjectInvariant()
-{
- Contract.Invariant(RefType!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(RefType != null);
Contract.Invariant(BoxType != null);
Contract.Invariant(CevTokenType != null);
Contract.Invariant(CevVariableKind != null);
@@ -144,7 +145,7 @@ namespace Microsoft.Dafny { Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
Contract.Invariant(allocField != null);
-}
+ }
public Bpl.Type SetType(IToken tok, Bpl.Type ty) {
@@ -363,11 +364,13 @@ namespace Microsoft.Dafny { return new Bpl.Program();
}
- // add the array classes used in this program
- foreach (ClassDecl arrayDecl in UserDefinedType.ArrayTypeDecls.Values) {
- AddClassMembers(arrayDecl);
+ foreach (TopLevelDecl d in program.BuiltIns.SystemModule.TopLevelDecls) {
+ if (d is DatatypeDecl) {
+ AddDatatype((DatatypeDecl)d);
+ } else {
+ AddClassMembers((ClassDecl)d);
+ }
}
-
foreach (ModuleDecl m in program.Modules) {
foreach (TopLevelDecl d in m.TopLevelDecls) {
if (d is DatatypeDecl) {
@@ -498,8 +501,13 @@ namespace Microsoft.Dafny { foreach (MemberDecl member in c.Members) {
if (member is Field) {
Field f = (Field)member;
- Bpl.Constant fc = GetField(f);
- sink.TopLevelDeclarations.Add(fc);
+ if (f.IsMutable) {
+ Bpl.Constant fc = GetField(f);
+ sink.TopLevelDeclarations.Add(fc);
+ } else {
+ Bpl.Function ff = GetReadonlyField(f);
+ sink.TopLevelDeclarations.Add(ff);
+ }
AddAllocationAxiom(f);
@@ -795,7 +803,7 @@ namespace Microsoft.Dafny { Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
Bpl.Expr length = isSequence ?
FunctionCall(tok, BuiltinFunction.SeqLength, null, seq) :
- FunctionCall(tok, BuiltinFunction.ArrayLength, null, seq, Bpl.Expr.Literal(0));
+ ArrayLength(tok, seq, 1, 0);
Bpl.Expr upper;
if (includeUpperBound) {
upper = Bpl.Expr.Le(index, length);
@@ -809,13 +817,11 @@ namespace Microsoft.Dafny { int loopHeapVarCount = 0;
int otherTmpVarCount = 0;
Bpl.IdentifierExpr _phvie = null;
- Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Bpl.VariableSeq locals){ // local variable that's shared between statements that need it
+ Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Bpl.VariableSeq locals) { // local variable that's shared between statements that need it
Contract.Requires(tok != null);
Contract.Requires(locals != null); Contract.Requires( predef != null);
Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
-
-
if (_phvie == null) {
// the "tok" of the first request for this variable is the one we use
Bpl.LocalVariable prevHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$prevHeap", predef.HeapType));
@@ -826,12 +832,11 @@ namespace Microsoft.Dafny { }
Bpl.IdentifierExpr _nwie = null;
Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals) // local variable that's shared between statements that need it
- { Contract.Requires(tok != null);
+ {
+ Contract.Requires(tok != null);
Contract.Requires(locals != null);
Contract.Requires( predef != null);
-
- Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
-
+ Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);
if (_nwie == null) {
// the "tok" of the first request for this variable is the one we use
@@ -846,10 +851,10 @@ namespace Microsoft.Dafny { {
Contract.Requires(m != null);
Contract.Requires(proc != null);
- Contract.Requires( sink != null && predef != null);
- Contract.Requires( wellformednessProc || m.Body != null);
- Contract.Requires( currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);
- Contract.Ensures( currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);
+ Contract.Requires(sink != null && predef != null);
+ Contract.Requires(wellformednessProc || m.Body != null);
+ Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);
+ Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);
currentMethod = m;
@@ -935,7 +940,7 @@ namespace Microsoft.Dafny { Contract.Requires(outParams != null);
Contract.Requires(builder != null);
Contract.Requires(localVariables != null);
- Contract.Requires( predef != null);
+ Contract.Requires(predef != null);
// Add CEV prelude
CEVPrelude(m, inParams, outParams, builder);
@@ -1301,7 +1306,7 @@ namespace Microsoft.Dafny { Bpl.Expr index = etran.TrExpr(idx);
Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
- Bpl.Expr length = FunctionCall(idx.tok, BuiltinFunction.ArrayLength, null, array, Bpl.Expr.Literal(i));
+ Bpl.Expr length = ArrayLength(idx.tok, array, e.Indices.Count, i);
Bpl.Expr upper = Bpl.Expr.Lt(index, length);
total = BplAnd(total, Bpl.Expr.And(lower, upper));
i++;
@@ -1454,7 +1459,7 @@ namespace Microsoft.Dafny { Contract.Requires(locals != null);
Contract.Requires(builder != null);
Contract.Requires(etran != null);
- Contract.Requires( predef != null);
+ Contract.Requires(predef != null);
if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {
// always allowed
@@ -1467,7 +1472,7 @@ namespace Microsoft.Dafny { FieldSelectExpr e = (FieldSelectExpr)expr;
CheckWellformed(e.Obj, func, Position.Neither, locals, builder, etran);
CheckNonNull(expr.tok, e.Obj, builder, etran);
- if (func != null) {
+ if (func != null && e.Field.IsMutable) {
builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field"));
}
} else if (expr is SeqSelectExpr) {
@@ -1500,7 +1505,7 @@ namespace Microsoft.Dafny { Bpl.Expr index = etran.TrExpr(idx);
Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);
- Bpl.Expr length = FunctionCall(idx.tok, BuiltinFunction.ArrayLength, null, array, Bpl.Expr.Literal(i));
+ Bpl.Expr length = ArrayLength(idx.tok, array, e.Indices.Count, i);
Bpl.Expr upper = Bpl.Expr.Lt(index, length);
builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range"));
i++;
@@ -1780,14 +1785,14 @@ namespace Microsoft.Dafny { }
Bpl.Constant GetField(Field f)
- {
- Contract.Requires(f != null);Contract.Requires( sink != null && predef != null);
+ {
+ Contract.Requires(f != null && f.IsMutable);
+ Contract.Requires(sink != null && predef != null);
Contract.Ensures(Contract.Result<Bpl.Constant>() != null);
-
Bpl.Constant fc;
if (fields.TryGetValue(f, out fc)) {
- Contract.Assert( fc != null);
+ Contract.Assert(fc != null);
} else {
// const unique f: Field ty;
Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
@@ -1801,12 +1806,43 @@ namespace Microsoft.Dafny { }
return fc;
}
-
+
+ Bpl.Function GetReadonlyField(Field f)
+ {
+ Contract.Requires(f != null && !f.IsMutable);
+ Contract.Requires(sink != null && predef != null);
+ Contract.Ensures(Contract.Result<Bpl.Function>() != null);
+
+ Bpl.Function ff;
+ if (fieldFunctions.TryGetValue(f, out ff)) {
+ Contract.Assert(ff != null);
+ } else {
+ // function f(Ref): ty;
+ Bpl.Type ty = TrType(f.Type);
+ Bpl.VariableSeq args = new Bpl.VariableSeq();
+ args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));
+ Bpl.Formal result = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, ty), false);
+ ff = new Bpl.Function(f.tok, f.FullName, args, result);
+ fieldFunctions.Add(f, ff);
+ // treat certain fields specially
+ if (f.EnclosingClass is ArrayClassDecl) {
+ // add non-negative-range axioms for array Length fields
+ // axiom (forall o: Ref :: 0 <= array.Length(o));
+ Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "o", predef.RefType));
+ Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(f.tok, oVar);
+ Bpl.Expr body = Bpl.Expr.Le(Bpl.Expr.Literal(0), new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(ff), new Bpl.ExprSeq(o)));
+ Bpl.Expr qq = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(oVar), body);
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, qq));
+ }
+ }
+ return ff;
+ }
+
Bpl.Expr GetField(FieldSelectExpr fse)
- {
- Contract.Requires(fse != null);Contract.Requires( fse.Field != null);
+ {
+ Contract.Requires(fse != null);
+ Contract.Requires(fse.Field != null && fse.Field.IsMutable);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
-
return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
}
@@ -1815,9 +1851,9 @@ namespace Microsoft.Dafny { /// This method is expected to be called just once for each function in the program.
/// </summary>
void AddFunction(Function f)
- {
+ {
Contract.Requires(f != null);
- Contract.Requires( predef != null && sink != null);
+ Contract.Requires( predef != null && sink != null);
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.VariableSeq args = new Bpl.VariableSeq();
args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true));
@@ -2151,12 +2187,11 @@ void ObjectInvariant() class BoilerplateTriple { // a triple that is now a quintuple
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(tok!=null);
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
Contract.Invariant(Expr != null);
Contract.Invariant(IsFree || ErrorMessage != null);
-}
+ }
public readonly IToken tok;
public readonly bool IsFree;
@@ -2879,7 +2914,7 @@ void ObjectInvariant() builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
}
- // Here comes: Contract.Assert( (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
+ // Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));
@@ -3320,16 +3355,16 @@ void ObjectInvariant() builder.Add(cmd);
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
- } else {
+ } else if (lhs is SeqSelectExpr) {
SeqSelectExpr sel = (SeqSelectExpr)lhs;
- Contract.Assert( sel.Seq.Type != null && sel.Seq.Type.IsArrayType);
+ Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType);
bRhs = etran.BoxIfNecessary(tok, bRhs, UserDefinedType.ArrayElementType(sel.Seq.Type));
if (sel.SelectOne) {
- Contract.Assert( sel.E0 != null);
+ Contract.Assert(sel.E0 != null);
Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0));
// check that the enclosing modifies clause allows this object to be written: Contract.Assert( $_Frame[obj,index]);
- builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName), "assignment may update an array not in the enclosing method's modifies clause"));
-
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+
Bpl.IdentifierExpr h = cce.NonNull((Bpl.IdentifierExpr)etran.HeapExpr); // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, etran.TrExpr(sel.Seq), fieldName, bRhs));
builder.Add(cmd);
@@ -3337,7 +3372,7 @@ void ObjectInvariant() builder.Add(AssumeGoodHeap(tok, etran));
} else {
Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);
- Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq), Bpl.Expr.Literal(0)) : etran.TrExpr(sel.E1);
+ Bpl.Expr high = sel.E1 == null ? ArrayLength(tok, etran.TrExpr(sel.Seq), 1, 0) : etran.TrExpr(sel.E1);
// check frame:
// assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
@@ -3346,12 +3381,25 @@ void ObjectInvariant() Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, ie);
Bpl.Expr cons = Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName);
Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
- builder.Add(Assert(tok, q, "assignment may update an array not in the enclosing method's modifies clause"));
+ builder.Add(Assert(tok, q, "assignment may update an array element not in the enclosing method's modifies clause"));
// do the update: call UpdateArrayRange(arr, low, high, rhs);
builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
new Bpl.ExprSeq(etran.TrExpr(sel.Seq), low, high, bRhs),
new Bpl.IdentifierExprSeq()));
}
+ } else {
+ MultiSelectExpr mse = (MultiSelectExpr)lhs;
+ Contract.Assert(mse.Array.Type != null && mse.Array.Type.IsArrayType);
+ bRhs = etran.BoxIfNecessary(tok, bRhs, UserDefinedType.ArrayElementType(mse.Array.Type));
+
+ Bpl.Expr fieldName = etran.GetArrayIndexFieldName(mse.tok, mse.Indices);
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(mse.Array), fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));
+
+ Bpl.IdentifierExpr h = cce.NonNull((Bpl.IdentifierExpr)etran.HeapExpr); // TODO: is this cast always justified?
+ Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, h, ExpressionTranslator.UpdateHeap(tok, h, etran.TrExpr(mse.Array), fieldName, bRhs));
+ builder.Add(cmd);
+ // assume $IsGoodHeap($Heap);
+ builder.Add(AssumeGoodHeap(tok, etran));
}
} else if (rhs is HavocRhs) {
@@ -3385,7 +3433,7 @@ void ObjectInvariant() // array allocation
List<Type> typeArgs = new List<Type>();
typeArgs.Add(tRhs.EType);
- rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array" + tRhs.ArrayDimensions.Count, predef.ClassNameType), typeArgs, true);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);
} else if (tRhs.EType is ObjectType) {
rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type>(), true);
} else {
@@ -3396,7 +3444,7 @@ void ObjectInvariant() int i = 0;
foreach (Expression dim in tRhs.ArrayDimensions) {
// assume Array#Length($nw, i) == arraySize;
- Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw, Bpl.Expr.Literal(i));
+ Bpl.Expr arrayLength = ArrayLength(tok, nw, tRhs.ArrayDimensions.Count, i);
builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim))));
i++;
}
@@ -3577,7 +3625,14 @@ void ObjectInvariant() } else if (expr is FieldSelectExpr) {
FieldSelectExpr e = (FieldSelectExpr)expr;
- Bpl.Expr result = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Obj), new Bpl.IdentifierExpr(expr.tok, translator.GetField(cce.NonNull(e.Field))));
+ Contract.Assert(e.Field != null);
+ Bpl.Expr obj = TrExpr(e.Obj);
+ Bpl.Expr result;
+ if (e.Field.IsMutable) {
+ result = ReadHeap(expr.tok, HeapExpr, obj, new Bpl.IdentifierExpr(expr.tok, translator.GetField(e.Field)));
+ } else {
+ result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new Bpl.ExprSeq(obj));
+ }
return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type));
} else if (expr is SeqSelectExpr) {
@@ -3630,17 +3685,7 @@ void ObjectInvariant() Type elmtType = UserDefinedType.ArrayElementType(e.Array.Type);;
Bpl.Type elType = translator.TrType(elmtType);
- Bpl.Expr fieldName = null;
- foreach (Expression idx in e.Indices) {
- Bpl.Expr index = TrExpr(idx);
- if (fieldName == null) {
- // the index in dimension 0: IndexField(index0)
- fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, index);
- } else {
- // the index in dimension n: MultiIndexField(...field name for first n indices..., index_n)
- fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.MultiIndexField, null, fieldName, index);
- }
- }
+ Bpl.Expr fieldName = GetArrayIndexFieldName(expr.tok, e.Indices);
Bpl.Expr x = ReadHeap(expr.tok, HeapExpr, TrExpr(e.Array), fieldName);
if (!ModeledAsBoxType(elmtType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
@@ -3729,7 +3774,7 @@ void ObjectInvariant() if (e.E.Type is SeqType) {
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
} else {
- return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg, Bpl.Expr.Literal(0));
+ return translator.ArrayLength(expr.tok, arg, 1, 0);
}
default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression
@@ -3884,7 +3929,22 @@ void ObjectInvariant() Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression
}
}
-
+
+ public Bpl.Expr GetArrayIndexFieldName(IToken tok, List<Expression> indices) {
+ Bpl.Expr fieldName = null;
+ foreach (Expression idx in indices) {
+ Bpl.Expr index = TrExpr(idx);
+ if (fieldName == null) {
+ // the index in dimension 0: IndexField(index0)
+ fieldName = translator.FunctionCall(tok, BuiltinFunction.IndexField, null, index);
+ } else {
+ // the index in dimension n: MultiIndexField(...field name for first n indices..., index_n)
+ fieldName = translator.FunctionCall(tok, BuiltinFunction.MultiIndexField, null, fieldName, index);
+ }
+ }
+ return fieldName;
+ }
+
public Bpl.Expr ProperSubset(IToken tok, Bpl.Expr e0, Bpl.Expr e1) {
Contract.Requires(tok != null);
Contract.Requires(e0 != null);
@@ -4238,7 +4298,6 @@ Contract.Requires(tok != null); SeqEqual,
SeqSameUntil,
- ArrayLength,
IndexField,
MultiIndexField,
@@ -4358,10 +4417,6 @@ Contract.Requires(tok != null); Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
- case BuiltinFunction.ArrayLength:
- Contract.Assert(args.Length == 2);
- Contract.Assert(typeInstantiation == null);
- return FunctionCall(tok, "Array#Length", Bpl.Type.Int, args);
case BuiltinFunction.IndexField:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
@@ -4466,9 +4521,7 @@ Contract.Requires(tok != null); Contract.Requires(function != null);
Contract.Requires(returnType != null);
Contract.Requires(cce.NonNullElements(args));
-
-
- Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
+ Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);
Bpl.ExprSeq aa = new Bpl.ExprSeq();
foreach (Bpl.Expr arg in args) {
@@ -4477,6 +4530,19 @@ Contract.Requires(tok != null); return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, function, returnType)), aa);
}
+ Bpl.Expr ArrayLength(IToken tok, Bpl.Expr arr, int totalDims, int dim) {
+ Contract.Requires(tok != null);
+ Contract.Requires(arr != null);
+ Contract.Requires(1 <= totalDims);
+ Contract.Requires(0 <= dim && dim < totalDims);
+
+ string name = BuiltIns.ArrayClassName(totalDims) + ".Length";
+ if (totalDims != 1) {
+ name += dim;
+ }
+ return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, name, Bpl.Type.Int)), new Bpl.ExprSeq(arr));
+ }
+
public bool SplitExpr(Expression expr, out List<Expression/*!*/>/*!*/ definitions, out List<Expression/*!*/>/*!*/ pieces) {
Contract.Requires(expr != null);
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out definitions)));
@@ -4658,7 +4724,15 @@ Contract.Requires(tok != null); if (seq != sse.Seq || index != sse.Index || val != sse.Value) {
newExpr = new SeqUpdateExpr(sse.tok, seq, index, val);
}
-
+
+ } else if (expr is MultiSelectExpr) {
+ MultiSelectExpr mse = (MultiSelectExpr)expr;
+ Expression array = Substitute(mse.Array, receiverReplacement, substMap);
+ List<Expression> newArgs = SubstituteExprList(mse.Indices, receiverReplacement, substMap);
+ if (array != mse.Array || newArgs != mse.Indices) {
+ newExpr = new MultiSelectExpr(mse.tok, array, newArgs);
+ }
+
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
Expression receiver = Substitute(e.Receiver, receiverReplacement, substMap);
diff --git a/Test/VSComp2010/Problem1-SumMax.dfy b/Test/VSComp2010/Problem1-SumMax.dfy index be7cc2c8..1b105ac1 100644 --- a/Test/VSComp2010/Problem1-SumMax.dfy +++ b/Test/VSComp2010/Problem1-SumMax.dfy @@ -8,7 +8,7 @@ // the requested postcondition.
method M(N: int, a: array<int>) returns (sum: int, max: int)
- requires 0 <= N && a != null && |a| == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]);
+ requires 0 <= N && a != null && a.Length == N && (forall k :: 0 <= k && k < N ==> 0 <= a[k]);
ensures sum <= N * max;
{
sum := 0;
@@ -39,5 +39,5 @@ method Main() a[8] := 10;
a[9] := 6;
call s, m := M(10, a);
- print "N = ", |a|, " sum = ", s, " max = ", m, "\n";
+ print "N = ", a.Length, " sum = ", s, " max = ", m, "\n";
}
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 63da4cb5..bf6aca37 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -23,7 +23,7 @@ // connect the two.
method M(N: int, A: array<int>, B: array<int>)
- requires 0 <= N && A != null && B != null && N == |A| && N == |B| && A != B;
+ requires 0 <= N && A != null && B != null && N == A.Length && N == B.Length && A != B;
requires (forall k :: 0 <= k && k < N ==> 0 <= A[k] && A[k] < N);
requires (forall j,k :: 0 <= j && j < k && k < N ==> A[j] != A[k]); // A is injective
requires (forall m :: 0 <= m && m < N && inImage(m) ==> (exists k :: 0 <= k && k < N && A[k] == m)); // A is surjective
@@ -72,7 +72,7 @@ method PrintArray(a: array<int>) requires a != null;
{
var i := 0;
- while (i < |a|) {
+ while (i < a.Length) {
print a[i], "\n";
i := i + 1;
}
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 1021ee85..6c6f11b3 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -2,18 +2,18 @@ class Benchmark2 {
method BinarySearch(a: array<int>, key: int) returns (result: int)
requires a != null;
- requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
- ensures -1 <= result && result < |a|;
+ requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
+ ensures -1 <= result && result < a.Length;
ensures 0 <= result ==> a[result] == key;
- ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key);
+ ensures result == -1 ==> (forall i :: 0 <= i && i < a.Length ==> a[i] != key);
{
var low := 0;
- var high := |a|;
+ var high := a.Length;
while (low < high)
- invariant 0 <= low && low <= high && high <= |a|;
+ invariant 0 <= low && low <= high && high <= a.Length;
invariant (forall i :: 0 <= i && i < low ==> a[i] < key);
- invariant (forall i :: high <= i && i < |a| ==> key < a[i]);
+ invariant (forall i :: high <= i && i < a.Length ==> key < a[i]);
{
var mid := low + (high - low) / 2;
var midVal := a[mid];
@@ -49,7 +49,7 @@ method Main() { method TestSearch(a: array<int>, key: int)
requires a != null;
- requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
+ requires (forall i, j :: 0 <= i && i < j && j < a.Length ==> a[i] <= a[j]);
{
var b := new Benchmark2;
call r := b.BinarySearch(a, key);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b698f917..4b4bf920 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -267,7 +267,7 @@ Execution trace: Dafny program verifier finished with 21 verified, 29 errors
-------------------- Array.dfy --------------------
-Array.dfy(10,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -280,11 +280,11 @@ Execution trace: Array.dfy(48,20): Error: assertion violation
Execution trace:
(0,0): anon0
-Array.dfy(56,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Array.dfy(63,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
@@ -301,15 +301,29 @@ Execution trace: (0,0): anon0
(0,0): anon4_Then
(0,0): anon5_Then
-Array.dfy(131,10): Error: assignment may update an array not in the enclosing method's modifies clause
+Array.dfy(131,10): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(138,10): Error: assignment may update an array not in the enclosing method's modifies clause
+Array.dfy(138,10): Error: assignment may update an array element not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
Dafny program verifier finished with 22 verified, 11 errors
+-------------------- MultiDimArray.dfy --------------------
+MultiDimArray.dfy(53,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon10_Then
+MultiDimArray.dfy(80,25): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Then
+ (0,0): anon6_Then
+
+Dafny program verifier finished with 8 verified, 2 errors
+
-------------------- 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
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 928f2bc5..048ecd7a 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -5,8 +5,8 @@ class A { }
method N0() {
- var a;
- if (a != null && 5 < |a|) {
+ var a: array<int>;
+ if (a != null && 5 < a.Length) {
a[5] := 12; // error: violates modifies clause
}
}
@@ -14,7 +14,7 @@ class A { method N1(a: array<int>)
modifies a;
{
- var b := |a|; // error: a may be null
+ var b := a.Length; // error: a may be null
}
method N2(a: array<int>)
@@ -25,9 +25,9 @@ class A { }
method N3(a: array<int>)
- requires a != null && 5 < |a|;
+ requires a != null && 5 < a.Length;
modifies a;
- ensures (forall i :: 0 <= i && i < |a| ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12));
+ ensures (forall i :: 0 <= i && i < a.Length ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12));
{
a[5] := 12; // all is good
}
@@ -52,21 +52,21 @@ class A { method P0()
modifies this;
{
- if (x != null && 100 <= |x|) {
+ if (x != null && 100 <= x.Length) {
x[5] := 12; // error: violates modifies clause
}
}
method P1()
modifies this`x;
{
- if (x != null && 100 <= |x|) {
+ if (x != null && 100 <= x.Length) {
x[5] := 12; // error: violates modifies clause
}
}
method P2()
modifies x;
{
- if (x != null && 100 <= |x|) {
+ if (x != null && 100 <= x.Length) {
x[5] := 12; // fine
}
}
@@ -76,7 +76,7 @@ class A { y[5] := null;
y[0..] := null;
y[..83] := null;
- y[0..|y|] := null;
+ y[0..y.Length] := null;
}
method R() {
@@ -91,7 +91,7 @@ class A { assert y[55] == 90;
assert y[83] == 25;
assert y[8] == 30;
- assert y[90] + y[91] + y[0] + 20 == |y|;
+ assert y[90] + y[91] + y[0] + 20 == y.Length;
assert y[93] == 24; // error (it's 25)
}
}
@@ -103,7 +103,7 @@ class B { } class ArrayTests {
function F0(a: array<int>): bool
{
- a != null && 10 <= |a| &&
+ a != null && 10 <= a.Length &&
a[7] == 13 // error: reads on something outside reads clause
}
@@ -111,28 +111,28 @@ class ArrayTests { function F1(): bool
reads this;
{
- b != null && 10 <= |b| &&
+ b != null && 10 <= b.Length &&
b[7] == 13 // error: reads on something outside reads clause
}
function F2(a: array<int>): bool
reads this, b, a;
{
- a != null && 10 <= |a| &&
+ a != null && 10 <= a.Length &&
a[7] == 13 // good
&&
- b != null && 10 <= |b| &&
+ b != null && 10 <= b.Length &&
b[7] == 13 // good
}
method M0(a: array<int>)
- requires a != null && 10 <= |a|;
+ requires a != null && 10 <= a.Length;
{
a[7] := 13; // error: updates location not in modifies clause
}
method M1()
- requires b != null && 10 <= |b|;
+ requires b != null && 10 <= b.Length;
modifies this;
{
b[7] := 13; // error: updates location not in modifies clause
@@ -146,8 +146,8 @@ class ArrayTests { }
method M3(a: array<int>)
- requires a != null && 10 <= |a|;
- requires b != null && 10 <= |b|;
+ requires a != null && 10 <= a.Length;
+ requires b != null && 10 <= b.Length;
modifies this, b, a;
{
a[7] := 13; // good
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy new file mode 100644 index 00000000..ba5dc9da --- /dev/null +++ b/Test/dafny0/MultiDimArray.dfy @@ -0,0 +1,91 @@ +class A {
+ // all of the following array types are allowed
+ var a: array<int>;
+ var b: array <bool>;
+ var c: array <A>;
+ var d: array1 <A>; // this is a synonym for array<A>
+ var e: array2 <A>;
+ var f: array3 <A>;
+ var g: array300 <A>;
+ var h: array3000 <array2<int>>;
+
+ method M0()
+ requires a != null && b != null;
+ modifies a;
+ {
+ if (5 <= a.Length && a.Length <= b.Length) {
+ var x := b[2];
+ var y := a[1];
+ var z := a[2];
+ a[2] := a[2] + 1;
+ assert x == b[2];
+ assert y == a[1];
+ assert z == a[2] - 1;
+ }
+ }
+
+ method M1()
+ requires a != null && d != null;
+ modifies a;
+ {
+ if (5 <= a.Length && a.Length <= d.Length) {
+ var x := d[2];
+ var y := a[1];
+ var z := a[2];
+ a[2] := a[2] + 1;
+ assert y == a[1];
+ assert z == a[2] - 1;
+ assert x == d[2]; // error: a and d may be equal
+ }
+ }
+
+ method M2(i: int, j: int, k: int, val: A)
+ requires f != null;
+ requires 0 <= i && i < f.Length0;
+ requires 0 <= j && j < f.Length1;
+ requires 0 <= k && k < f.Length2;
+ modifies f;
+ {
+ if (*) {
+ if (k < f.Length0) {
+ var save := f[k,j,k];
+ f[i,j,k] := val;
+ assert save == f[k,j,k]; // error: k and i may be equal
+ }
+ } else if (k < f.Length0 && k != i) {
+ if (k < f.Length0) {
+ var save := f[k,j,k];
+ f[i,j,k] := val;
+ assert save == f[k,j,k]; // fine
+ }
+ }
+ }
+
+ method M3(i: int, j: int, k: int)
+ requires f != null;
+ requires 0 <= i && i < f.Length0;
+ requires 0 <= j && j < f.Length1;
+ requires 0 <= k && k < f.Length2;
+ modifies f;
+ decreases i;
+ {
+ if (i != 0) {
+ var z := new A[2,3,5]; // first three primes (nice!)
+ var s := z[1,2,4]; // first three powers of 2 (tra-la-la)
+ var some: A;
+ f[i,j,k] := some;
+ call M3(i-1, j, k);
+ assert s == z[1,2,4];
+ if (*) {
+ assert f[i,j,k] == some; // error: the recursive call may have modified any element in 'f'
+ }
+ }
+ }
+
+ method M4(a: array2<bool>) returns (k: int)
+ requires a != null;
+ ensures 0 <= k;
+ {
+ k := a.Length0 + a.Length1;
+ }
+}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index ccdbcb91..6e8e2b72 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -49,7 +49,7 @@ datatype ReverseOrder_TheCounterpart<T> { class ArrayTests {
ghost method G(a: array<int>)
- requires a != null && 10 <= |a|;
+ requires a != null && 10 <= a.Length;
modifies a;
{
a[7] := 13; // error: array elements are not ghost locations
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index d29edd34..16596fa5 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -11,7 +11,7 @@ for %%f in (Simple.dfy) do ( %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f
)
-for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy
+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy MultiDimArray.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy
Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy) do (
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index 71646dab..c81c0268 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -31,6 +31,10 @@ Dafny program verifier finished with 2 verified, 0 errors Dafny program verifier finished with 9 verified, 0 errors
+-------------------- MatrixFun.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+
-------------------- SchorrWaite.dfy --------------------
Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy new file mode 100644 index 00000000..96d89ad6 --- /dev/null +++ b/Test/dafny1/MatrixFun.dfy @@ -0,0 +1,59 @@ +method MirrorImage<T>(m: array2<T>)
+ requires m != null;
+ modifies m;
+ ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+{
+ var a := 0;
+ while (a < m.Length0)
+ invariant a <= m.Length0;
+ invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+ invariant (forall i,j :: a <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i,j]));
+ {
+ var b := 0;
+ while (b < m.Length1 / 2)
+ invariant b <= m.Length1 / 2;
+ invariant (forall i,j :: 0 <= i && i < a && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i, m.Length1-1-j]));
+ invariant (forall j :: 0 <= j && j < b ==>
+ m[a,j] == old(m[a, m.Length1-1-j]) &&
+ old(m[a,j]) == m[a, m.Length1-1-j]);
+ invariant (forall j :: b <= j && j < m.Length1-b ==> m[a,j] == old(m[a,j]));
+ invariant (forall i,j :: a+1 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==>
+ m[i,j] == old(m[i,j]));
+ {
+ var tmp := m[a, m.Length1-1-b];
+ m[a, m.Length1-1-b] := m[a, b];
+ m[a, b] := tmp;
+ b := b + 1;
+ }
+ a := a + 1;
+ }
+}
+
+method Flip<T>(m: array2<T>)
+ requires m != null && m.Length0 == m.Length1;
+ modifies m;
+ ensures (forall i,j :: 0 <= i && i < m.Length0 && 0 <= j && j < m.Length1 ==> m[i,j] == old(m[j,i]));
+{
+ var N := m.Length0;
+ var a := 0;
+ var b := 0;
+ while (a != N)
+ invariant a <= b && b <= N;
+ invariant (forall i,j :: 0 <= i && i <= j && j < N ==>
+ (if i < a || (i == a && j < b)
+ then m[i,j] == old(m[j,i]) && m[j,i] == old(m[i,j])
+ else m[i,j] == old(m[i,j]) && m[j,i] == old(m[j,i])));
+ decreases N-a, N-b;
+ {
+ if (b < N) {
+ var tmp := m[a,b]; m[a,b] := m[b,a]; m[b,a] := tmp;
+ b := b + 1;
+ } else {
+ a := a + 1; b := a;
+ }
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index eaee07d4..ea5b0ec7 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -16,6 +16,7 @@ for %%f in (Queue.dfy UnboundedStack.dfy
SeparationLogicList.dfy
ListCopy.dfy ListReverse.dfy ListContents.dfy
+ MatrixFun.dfy
SchorrWaite.dfy
SumOfCubes.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy index c5a032fe..fc4d687d 100644 --- a/Test/vacid0/LazyInitArray.dfy +++ b/Test/vacid0/LazyInitArray.dfy @@ -11,11 +11,11 @@ class LazyInitArray<T> { reads this, a, b, c;
{
a != null && b != null && c != null &&
- |a| == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
- |b| == |Contents| &&
- |c| == |Contents| &&
+ a.Length == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
+ b.Length == |Contents| &&
+ c.Length == |Contents| &&
b != c &&
- 0 <= n && n <= |c| &&
+ 0 <= n && n <= c.Length &&
(forall i :: 0 <= i && i < |Contents| ==>
Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
(forall i :: 0 <= i && i < |Contents| ==>
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 2f5fc467..82490ae7 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -39,7 +39,7 @@ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("array" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 12d433b1..48841c43 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -25,7 +25,7 @@ namespace Demo "int", "bool", "false", "true", "null",
"function", "free",
"in", "forall", "exists",
- "seq", "set", "array",
+ "seq", "set", "array", "array2", "array3",
"match", "case",
"fresh", "old"
);
@@ -330,6 +330,8 @@ namespace Demo | "seq"
| "set"
| "array"
+ | "array2"
+ | "array3"
| "match"
| "case"
| "fresh"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 5551cec0..9eb941de 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,bool,int,object,set,seq,array,%
+ morekeywords={class,datatype,bool,int,object,set,seq,array,array2,array3,%
function,unlimited,
ghost,var,static,refines,replaces,by,
method,returns,module,imports,in,
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim index 91166eb0..df2666c3 100644 --- a/Util/vim/syntax/dafny.vim +++ b/Util/vim/syntax/dafny.vim @@ -11,7 +11,7 @@ syntax keyword dafnyConditional if then else match case syntax keyword dafnyRepeat foreach while syntax keyword dafnyStatement havoc assume assert return call new print break label syntax keyword dafnyKeyword var ghost returns null static this refines replaces by -syntax keyword dafnyType int bool seq set object +syntax keyword dafnyType int bool seq set object array array2 array3 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant syntax keyword dafnyOperator forall exists old fresh syntax keyword dafnyBoolean true false |