diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 58 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.ssc | 43 | ||||
| -rw-r--r-- | Source/Dafny/DafnyMain.ssc | 5 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 987 | ||||
| -rw-r--r-- | Source/Dafny/Printer.ssc | 98 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.ssc | 50 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.ssc | 183 | ||||
| -rw-r--r-- | Source/Dafny/SccGraph.ssc | 81 | ||||
| -rw-r--r-- | Source/Dafny/Translator.ssc | 48 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 136 | ||||
| -rw-r--r-- | Test/dafny0/BinaryTree.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 218 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 34 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 219 | ||||
| -rw-r--r-- | Test/dafny0/SumOfCubes.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 1 | ||||
| -rw-r--r-- | Util/latex/dafny.sty | 4 |
18 files changed, 1237 insertions, 953 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 33a1d903..3ac46422 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -18,6 +18,7 @@ COMPILER Dafny /*--------------------------------------------------------------------------*/
+static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
@@ -29,7 +30,7 @@ static int anonymousIds = 0; struct MemberModifiers {
public bool IsGhost;
- public bool IsClass;
+ public bool IsStatic;
public bool IsUse;
}
@@ -57,20 +58,20 @@ private static Expression! ConvertToLocal(Expression! e) }
///<summary>
-/// Parses top level declarations from "filename" and appends them to "classes".
+/// Parses top level declarations from "filename" and appends them to "modules" and "classes".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
if (filename == "stdin.dfy") {
BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
- return Parse(classes);
+ return Parse(modules, classes);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
- return Parse(classes);
+ return Parse(modules, classes);
}
}
}
@@ -80,10 +81,13 @@ public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* thro /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<TopLevelDecl!>! classes) {
+public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {
+ List<ModuleDecl!> oldModules = theModules;
List<TopLevelDecl!> oldClasses = theClasses;
+ theModules = modules;
theClasses = classes;
Parse();
+ theModules = oldModules;
theClasses = oldClasses;
return Errors.count;
}
@@ -122,14 +126,27 @@ IGNORE cr + lf + tab PRODUCTIONS
Dafny
-= (. ClassDecl! c; DatatypeDecl! dt; .)
- { ClassDecl<out c> (. theClasses.Add(c); .)
- | DatatypeDecl<out dt> (. theClasses.Add(dt); .)
+= (. ClassDecl! c; DatatypeDecl! dt;
+ ModuleDecl m; Attributes attrs; Token! id; List<string!> theImports;
+ .)
+ { "module" (. attrs = null; theImports = new List<string!>(); .)
+ { Attribute<ref attrs> }
+ Ident<out id>
+ [ "imports" Idents<theImports> ] (. m = new ModuleDecl(id, id.val, theImports, attrs);
+ theModules.Add(m);
+ .)
+ "{"
+ { ClassDecl<m, out c> (. theClasses.Add(c); .)
+ | DatatypeDecl<m, out dt> (. theClasses.Add(dt); .)
+ }
+ "}"
+ | ClassDecl<null, out c> (. theClasses.Add(c); .)
+ | DatatypeDecl<null, out dt> (. theClasses.Add(dt); .)
}
EOF
.
-ClassDecl<out ClassDecl! c>
+ClassDecl<ModuleDecl module, out ClassDecl! c>
= (. Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
@@ -142,7 +159,7 @@ ClassDecl<out ClassDecl! c> "{"
{ ClassMemberDecl<members>
}
- "}" (. c = new ClassDecl(id, id.val, typeArgs, members, attrs); .)
+ "}" (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs); .)
.
ClassMemberDecl<List<MemberDecl!\>! mm>
@@ -151,7 +168,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm> MemberModifiers mmod = new MemberModifiers();
.)
{ "ghost" (. mmod.IsGhost = true; .)
- | "class" (. mmod.IsClass = true; .)
+ | "static" (. mmod.IsStatic = true; .)
| "use" (. mmod.IsUse = true; .)
}
( FieldDecl<mmod, mm>
@@ -160,7 +177,7 @@ ClassMemberDecl<List<MemberDecl!\>! mm> )
.
-DatatypeDecl<out DatatypeDecl! dt>
+DatatypeDecl<ModuleDecl module, out DatatypeDecl! dt>
= (. Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
@@ -173,7 +190,7 @@ DatatypeDecl<out DatatypeDecl! dt> "{"
{ DatatypeMemberDecl<ctors>
}
- "}" (. dt = new DatatypeDecl(id, id.val, typeArgs, ctors, attrs); .)
+ "}" (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); .)
.
DatatypeMemberDecl<List<DatatypeCtor!\>! ctors>
@@ -199,7 +216,7 @@ FieldDecl<MemberModifiers mmod, List<MemberDecl!\>! mm> .)
"var"
(. if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }
- if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); }
+ if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
.)
{ Attribute<ref attrs> }
IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
@@ -295,7 +312,7 @@ MethodDecl<MemberModifiers mmod, out Method! m> )
(. parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
.)
.
@@ -419,7 +436,7 @@ FunctionDecl<MemberModifiers mmod, out Function! f> FunctionBody<out bb> (. body = bb; .)
)
(. parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
.)
.
@@ -1115,6 +1132,13 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs> /*------------------------------------------------------------------------*/
+Idents<List<string!\>! ids>
+= (. Token! id; .)
+ Ident<out id> (. ids.Add(id.val); .)
+ { "," Ident<out id> (. ids.Add(id.val); .)
+ }
+ .
+
Ident<out Token! x>
=
ident (. x = token; .)
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 2a0fa32c..2e5bd893 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -12,9 +12,11 @@ namespace Microsoft.Dafny {
public class Program {
public readonly string! Name;
+ public readonly List<ModuleDecl!>! Modules;
public readonly List<TopLevelDecl!>! Classes;
- public Program(string! name, [Captured] List<TopLevelDecl!>! classes) {
+ public Program(string! name, [Captured] List<ModuleDecl!>! modules, [Captured] List<TopLevelDecl!>! classes) {
Name = name;
+ Modules = modules;
Classes = classes;
}
}
@@ -305,6 +307,11 @@ namespace Microsoft.Dafny this.Name = name;
this.Attributes = attributes;
}
+
+ [Pure]
+ public override string! ToString() {
+ return Name;
+ }
}
public class TypeParameter : Declaration {
@@ -332,30 +339,40 @@ namespace Microsoft.Dafny }
}
+ public class ModuleDecl : Declaration {
+ public readonly List<string!>! Imports;
+ public ModuleDecl(Token! tok, string! name, [Captured] List<string!>! imports, Attributes attributes) {
+ Imports = imports;
+ base(tok, name, attributes);
+ }
+ }
+
public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType {
+ public readonly ModuleDecl Module;
public readonly List<TypeParameter!>! TypeArgs;
- public TopLevelDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, Attributes attributes) {
+ public TopLevelDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, Attributes attributes) {
+ Module = module;
TypeArgs = typeArgs;
base(tok, name, attributes);
}
}
-
+
public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl!>! Members;
- public ClassDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
+ public ClassDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<MemberDecl!>! members, Attributes attributes) {
Members = members;
- base(tok, name, typeArgs, attributes);
+ base(tok, name, module, typeArgs, attributes);
}
}
public class DatatypeDecl : TopLevelDecl {
public readonly List<DatatypeCtor!>! Ctors;
- public DatatypeDecl(Token! tok, string! name, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
+ public DatatypeDecl(Token! tok, string! name, ModuleDecl module, List<TypeParameter!>! typeArgs, [Captured] List<DatatypeCtor!>! ctors, Attributes attributes) {
Ctors = ctors;
- base(tok, name, typeArgs, attributes);
+ base(tok, name, module, typeArgs, attributes);
}
}
@@ -473,7 +490,7 @@ namespace Microsoft.Dafny }
public class Function : MemberDecl, TypeParameter.ParentType {
- public readonly bool IsClass;
+ public readonly bool IsStatic;
public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method"
public readonly bool IsUse;
public readonly List<TypeParameter!>! TypeArgs;
@@ -484,9 +501,9 @@ namespace Microsoft.Dafny public readonly List<Expression!>! Decreases;
public readonly Expression Body; // an extended expression
- public Function(Token! tok, string! name, bool isClass, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
+ public Function(Token! tok, string! name, bool isStatic, bool isGhost, bool isUse, [Captured] List<TypeParameter!>! typeArgs, [Captured] List<Formal!>! formals, Type! resultType,
List<Expression!>! req, List<Expression!>! reads, List<Expression!>! decreases, Expression body, Attributes attributes) {
- this.IsClass = isClass;
+ this.IsStatic = isStatic;
this.IsGhost = isGhost;
this.IsUse = isUse;
this.TypeArgs = typeArgs;
@@ -501,7 +518,7 @@ namespace Microsoft.Dafny }
public class Method : MemberDecl, TypeParameter.ParentType {
- public readonly bool IsClass;
+ public readonly bool IsStatic;
public readonly bool IsGhost;
public readonly List<TypeParameter!>! TypeArgs;
public readonly List<Formal!>! Ins;
@@ -513,14 +530,14 @@ namespace Microsoft.Dafny public readonly Statement Body;
public Method(Token! tok, string! name,
- bool isClass, bool isGhost,
+ bool isStatic, bool isGhost,
[Captured] List<TypeParameter!>! typeArgs,
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
[Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
[Captured] List<Expression!>! decreases,
[Captured] Statement body,
Attributes attributes) {
- this.IsClass = isClass;
+ this.IsStatic = isStatic;
this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.Ins = ins;
diff --git a/Source/Dafny/DafnyMain.ssc b/Source/Dafny/DafnyMain.ssc index 2cccc08e..36ca4191 100644 --- a/Source/Dafny/DafnyMain.ssc +++ b/Source/Dafny/DafnyMain.ssc @@ -19,6 +19,7 @@ namespace Microsoft.Dafny { {
program = null;
Dafny.Errors.count = 0;
+ List<ModuleDecl!> modules = new List<ModuleDecl!>();
List<TopLevelDecl!> classes = new List<TopLevelDecl!>();
foreach (string! dafnyFileName in fileNames){
if (Bpl.CommandLineOptions.Clo.XmlSink != null && Bpl.CommandLineOptions.Clo.XmlSink.IsOpen) {
@@ -32,7 +33,7 @@ namespace Microsoft.Dafny { int errorCount;
try
{
- errorCount = Dafny.Parser.Parse(dafnyFileName, classes);
+ errorCount = Dafny.Parser.Parse(dafnyFileName, modules, classes);
if (errorCount != 0)
{
return string.Format("{0} parse errors detected in {1}", Dafny.Errors.count, dafnyFileName);
@@ -44,7 +45,7 @@ namespace Microsoft.Dafny { }
}
- program = new Program(programName, classes);
+ program = new Program(programName, modules, classes);
if (Bpl.CommandLineOptions.Clo.DafnyPrintFile != null) {
string filename = Bpl.CommandLineOptions.Clo.DafnyPrintFile;
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index ca1eed51..b76182e4 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -6,7 +6,7 @@ using Microsoft.Contracts; namespace Microsoft.Dafny {
public class Parser {
- const int maxT = 93;
+ const int maxT = 96;
const bool T = true;
const bool x = false;
@@ -16,7 +16,8 @@ public class Parser { static Token/*!*/ t; // lookahead token
static int errDist = minErrDist;
- static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
+ static List<ModuleDecl!>! theModules = new List<ModuleDecl!>();
+static List<TopLevelDecl!>! theClasses = new List<TopLevelDecl!>();
static Expression! dummyExpr = new LiteralExpr(Token.NoToken);
@@ -27,7 +28,7 @@ static int anonymousIds = 0; struct MemberModifiers {
public bool IsGhost;
- public bool IsClass;
+ public bool IsStatic;
public bool IsUse;
}
@@ -55,20 +56,20 @@ private static Expression! ConvertToLocal(Expression! e) }
///<summary>
-/// Parses top level declarations from "filename" and appends them to "classes".
+/// Parses top level declarations from "filename" and appends them to "modules" and "classes".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
+public static int Parse (string! filename, List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) /* throws System.IO.IOException */ {
if (filename == "stdin.dfy") {
BoogiePL.Buffer.Fill(System.Console.In);
Scanner.Init(filename);
- return Parse(classes);
+ return Parse(modules, classes);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
BoogiePL.Buffer.Fill(reader);
Scanner.Init(filename);
- return Parse(classes);
+ return Parse(modules, classes);
}
}
}
@@ -78,10 +79,13 @@ public static int Parse (string! filename, List<TopLevelDecl!>! classes) /* thro /// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///</summary>
-public static int Parse (List<TopLevelDecl!>! classes) {
+public static int Parse (List<ModuleDecl!>! modules, List<TopLevelDecl!>! classes) {
+ List<ModuleDecl!> oldModules = theModules;
List<TopLevelDecl!> oldClasses = theClasses;
+ theModules = modules;
theClasses = classes;
Parse();
+ theModules = oldModules;
theClasses = oldClasses;
return Errors.count;
}
@@ -145,85 +149,123 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
static void Dafny() {
- ClassDecl! c; DatatypeDecl! dt;
- while (t.kind == 4 || t.kind == 9) {
+ ClassDecl! c; DatatypeDecl! dt;
+ ModuleDecl m; Attributes attrs; Token! id; List<string!> theImports;
+
+ while (t.kind == 4 || t.kind == 8 || t.kind == 12) {
if (t.kind == 4) {
- ClassDecl(out c);
+ Get();
+ attrs = null; theImports = new List<string!>();
+ while (t.kind == 6) {
+ Attribute(ref attrs);
+ }
+ Ident(out id);
+ if (t.kind == 5) {
+ Get();
+ Idents(theImports);
+ }
+ m = new ModuleDecl(id, id.val, theImports, attrs);
+ theModules.Add(m);
+
+ Expect(6);
+ while (t.kind == 8 || t.kind == 12) {
+ if (t.kind == 8) {
+ ClassDecl(m, out c);
+ theClasses.Add(c);
+ } else {
+ DatatypeDecl(m, out dt);
+ theClasses.Add(dt);
+ }
+ }
+ Expect(7);
+ } else if (t.kind == 8) {
+ ClassDecl(null, out c);
theClasses.Add(c);
} else {
- DatatypeDecl(out dt);
+ DatatypeDecl(null, out dt);
theClasses.Add(dt);
}
}
Expect(0);
}
- static void ClassDecl(out ClassDecl! c) {
+ static void Attribute(ref Attributes attrs) {
+ Expect(6);
+ AttributeBody(ref attrs);
+ Expect(7);
+ }
+
+ static void Ident(out Token! x) {
+ Expect(1);
+ x = token;
+ }
+
+ static void Idents(List<string!>! ids) {
+ Token! id;
+ Ident(out id);
+ ids.Add(id.val);
+ while (t.kind == 15) {
+ Get();
+ Ident(out id);
+ ids.Add(id.val);
+ }
+ }
+
+ static void ClassDecl(ModuleDecl module, out ClassDecl! c) {
Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<MemberDecl!> members = new List<MemberDecl!>();
- Expect(4);
- while (t.kind == 5) {
+ Expect(8);
+ while (t.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericParameters(typeArgs);
}
- Expect(5);
+ Expect(6);
while (StartOf(1)) {
ClassMemberDecl(members);
}
- Expect(6);
- c = new ClassDecl(id, id.val, typeArgs, members, attrs);
+ Expect(7);
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
}
- static void DatatypeDecl(out DatatypeDecl! dt) {
+ static void DatatypeDecl(ModuleDecl module, out DatatypeDecl! dt) {
Token! id;
Attributes attrs = null;
List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<DatatypeCtor!> ctors = new List<DatatypeCtor!>();
- Expect(9);
- while (t.kind == 5) {
+ Expect(12);
+ while (t.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericParameters(typeArgs);
}
- Expect(5);
- while (t.kind == 1 || t.kind == 5) {
+ Expect(6);
+ while (t.kind == 1 || t.kind == 6) {
DatatypeMemberDecl(ctors);
}
- Expect(6);
- dt = new DatatypeDecl(id, id.val, typeArgs, ctors, attrs);
- }
-
- static void Attribute(ref Attributes attrs) {
- Expect(5);
- AttributeBody(ref attrs);
- Expect(6);
- }
-
- static void Ident(out Token! x) {
- Expect(1);
- x = token;
+ Expect(7);
+ dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
Token! id;
- Expect(14);
+ Expect(17);
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Ident(out id);
typeArgs.Add(new TypeParameter(id, id.val));
}
- Expect(15);
+ Expect(18);
}
static void ClassMemberDecl(List<MemberDecl!>! mm) {
@@ -231,48 +273,48 @@ public static int Parse (List<TopLevelDecl!>! classes) { Function! f;
MemberModifiers mmod = new MemberModifiers();
- while (t.kind == 4 || t.kind == 7 || t.kind == 8) {
- if (t.kind == 7) {
+ while (t.kind == 9 || t.kind == 10 || t.kind == 11) {
+ if (t.kind == 9) {
Get();
mmod.IsGhost = true;
- } else if (t.kind == 4) {
+ } else if (t.kind == 10) {
Get();
- mmod.IsClass = true;
+ mmod.IsStatic = true;
} else {
Get();
mmod.IsUse = true;
}
}
- if (t.kind == 11) {
+ if (t.kind == 14) {
FieldDecl(mmod, mm);
- } else if (t.kind == 30) {
+ } else if (t.kind == 33) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (t.kind == 16) {
+ } else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(94);
+ } else Error(97);
}
static void FieldDecl(MemberModifiers mmod, List<MemberDecl!>! mm) {
Attributes attrs = null;
Token! id; Type! ty;
- Expect(11);
+ Expect(14);
if (mmod.IsUse) { SemErr(token, "fields cannot be declared 'use'"); }
- if (mmod.IsClass) { SemErr(token, "fields cannot be declared 'class'"); }
+ if (mmod.IsStatic) { SemErr(token, "fields cannot be declared 'static'"); }
- while (t.kind == 5) {
+ while (t.kind == 6) {
Attribute(ref attrs);
}
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
IdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- Expect(10);
+ Expect(13);
}
static void FunctionDecl(MemberModifiers mmod, out Function! f) {
@@ -287,38 +329,38 @@ public static int Parse (List<TopLevelDecl!>! classes) { Expression! bb; Expression body = null;
bool isFunctionMethod = false;
- Expect(30);
- if (t.kind == 16) {
+ Expect(33);
+ if (t.kind == 19) {
Get();
isFunctionMethod = true;
}
if (mmod.IsGhost) { SemErr(token, "functions cannot be declared 'ghost' (they are ghost by default)"); }
- while (t.kind == 5) {
+ while (t.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, false, formals);
- Expect(13);
+ Expect(16);
Type(out returnType);
- if (t.kind == 10) {
+ if (t.kind == 13) {
Get();
- while (t.kind == 20 || t.kind == 22 || t.kind == 31) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(2)) {
- while (t.kind == 20 || t.kind == 22 || t.kind == 31) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
- } else Error(95);
+ } else Error(98);
parseVarScope.PopMarker();
- f = new Function(id, id.val, mmod.IsClass, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
+ f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUse, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
}
@@ -334,23 +376,23 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<Expression!> dec = new List<Expression!>();
Statement! bb; Statement body = null;
- Expect(16);
+ Expect(19);
if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
- while (t.kind == 5) {
+ while (t.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
Formals(true, true, ins);
- if (t.kind == 17) {
+ if (t.kind == 20) {
Get();
Formals(false, true, outs);
}
- if (t.kind == 10) {
+ if (t.kind == 13) {
Get();
while (StartOf(3)) {
MethodSpec(req, mod, ens, dec);
@@ -361,9 +403,9 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
BlockStmt(out bb);
body = bb;
- } else Error(96);
+ } else Error(99);
parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
+ m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
}
@@ -373,47 +415,47 @@ public static int Parse (List<TopLevelDecl!>! classes) { List<TypeParameter!> typeArgs = new List<TypeParameter!>();
List<Formal!> formals = new List<Formal!>();
- while (t.kind == 5) {
+ while (t.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericParameters(typeArgs);
}
parseVarScope.PushMarker();
- if (t.kind == 23) {
+ if (t.kind == 26) {
FormalsOptionalIds(formals);
}
parseVarScope.PopMarker();
ctors.Add(new DatatypeCtor(id, id.val, typeArgs, formals, attrs));
- Expect(10);
+ Expect(13);
}
static void FormalsOptionalIds(List<Formal!>! formals) {
Token! id; Type! ty; string! name;
- Expect(23);
+ Expect(26);
if (StartOf(5)) {
TypeIdentOptional(out id, out name, out ty);
formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
TypeIdentOptional(out id, out name, out ty);
formals.Add(new Formal(id, name, ty, true, false)); parseVarScope.Push(name, name);
}
}
- Expect(24);
+ Expect(27);
}
static void IdentType(out Token! id, out Type! ty) {
Ident(out id);
- Expect(13);
+ Expect(16);
Type(out ty);
}
static void GIdentType(bool allowGhost, out Token! id, out Type! ty, out bool isGhost) {
isGhost = false;
- if (t.kind == 7) {
+ if (t.kind == 9) {
Get();
if (allowGhost) { isGhost = true; } else { SemErr(token, "formal cannot be declared 'ghost' in this context"); }
}
@@ -429,7 +471,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { Token! id; Type! ty; Type optType = null;
Ident(out id);
- if (t.kind == 13) {
+ if (t.kind == 16) {
Get();
Type(out ty);
optType = ty;
@@ -440,7 +482,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { static void TypeIdentOptional(out Token! id, out string! identName, out Type! ty) {
string name = null;
TypeAndToken(out id, out ty);
- if (t.kind == 13) {
+ if (t.kind == 16) {
Get();
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
@@ -463,13 +505,13 @@ public static int Parse (List<TopLevelDecl!>! classes) { tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 25) {
+ if (t.kind == 28) {
Get();
tok = token;
- } else if (t.kind == 26) {
+ } else if (t.kind == 29) {
Get();
tok = token; ty = new IntType();
- } else if (t.kind == 27) {
+ } else if (t.kind == 30) {
Get();
tok = token; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -478,7 +520,7 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
ty = new SetType(gt[0]);
- } else if (t.kind == 28) {
+ } else if (t.kind == 31) {
Get();
tok = token; gt = new List<Type!>();
GenericInstantiation(gt);
@@ -487,63 +529,63 @@ public static int Parse (List<TopLevelDecl!>! classes) { }
ty = new SeqType(gt[0]);
- } else if (t.kind == 1 || t.kind == 29) {
+ } else if (t.kind == 1 || t.kind == 32) {
ReferenceType(out tok, out ty);
- } else Error(97);
+ } else Error(100);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
Token! id; Type! ty; bool isGhost;
- Expect(23);
- if (t.kind == 1 || t.kind == 7) {
+ Expect(26);
+ if (t.kind == 1 || t.kind == 9) {
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 (t.kind == 12) {
+ while (t.kind == 15) {
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(24);
+ Expect(27);
}
static void MethodSpec(List<MaybeFreeExpression!>! req, List<Expression!>! mod, List<MaybeFreeExpression!>! ens,
List<Expression!>! decreases) {
Expression! e; bool isFree = false;
- if (t.kind == 18) {
+ if (t.kind == 21) {
Get();
if (StartOf(6)) {
Expression(out e);
mod.Add(e);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Expression(out e);
mod.Add(e);
}
}
- Expect(10);
- } else if (t.kind == 19 || t.kind == 20 || t.kind == 21) {
- if (t.kind == 19) {
+ Expect(13);
+ } else if (t.kind == 22 || t.kind == 23 || t.kind == 24) {
+ if (t.kind == 22) {
Get();
isFree = true;
}
- if (t.kind == 20) {
+ if (t.kind == 23) {
Get();
Expression(out e);
- Expect(10);
+ Expect(13);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (t.kind == 21) {
+ } else if (t.kind == 24) {
Get();
Expression(out e);
- Expect(10);
+ Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(98);
- } else if (t.kind == 22) {
+ } else Error(101);
+ } else if (t.kind == 25) {
Get();
PossiblyWildExpressions(decreases);
- Expect(10);
- } else Error(99);
+ Expect(13);
+ } else Error(102);
}
static void BlockStmt(out Statement! block) {
@@ -552,12 +594,12 @@ List<Expression!>! decreases) { Statement! s;
parseVarScope.PushMarker();
- Expect(5);
+ Expect(6);
x = token;
while (StartOf(7)) {
Stmt(body);
}
- Expect(6);
+ Expect(7);
block = new BlockStmt(x, body);
parseVarScope.PopMarker();
}
@@ -566,25 +608,25 @@ List<Expression!>! decreases) { Token! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
- if (t.kind == 42) {
+ if (t.kind == 45) {
Get();
x = token;
Expression(out e);
- Expect(52);
+ Expect(55);
Expression(out e0);
- Expect(43);
+ Expect(46);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(8)) {
EquivExpression(out e);
- } else Error(100);
+ } else Error(103);
}
static void PossiblyWildExpressions(List<Expression!>! args) {
Expression! e;
PossiblyWildExpression(out e);
args.Add(e);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
PossiblyWildExpression(out e);
args.Add(e);
@@ -593,70 +635,70 @@ List<Expression!>! decreases) { static void GenericInstantiation(List<Type!>! gt) {
Type! ty;
- Expect(14);
+ Expect(17);
Type(out ty);
gt.Add(ty);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Type(out ty);
gt.Add(ty);
}
- Expect(15);
+ Expect(18);
}
static void ReferenceType(out Token! tok, out Type! ty) {
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type!>! gt;
- if (t.kind == 29) {
+ if (t.kind == 32) {
Get();
tok = token; ty = new ObjectType();
} else if (t.kind == 1) {
Ident(out tok);
gt = new List<Type!>();
- if (t.kind == 14) {
+ if (t.kind == 17) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(101);
+ } else Error(104);
}
static void FunctionSpec(List<Expression!>! reqs, List<Expression!>! reads, List<Expression!>! decreases) {
Expression! e;
- if (t.kind == 20) {
+ if (t.kind == 23) {
Get();
Expression(out e);
- Expect(10);
+ Expect(13);
reqs.Add(e);
- } else if (t.kind == 31) {
+ } else if (t.kind == 34) {
Get();
if (StartOf(9)) {
PossiblyWildExpressions(reads);
}
- Expect(10);
- } else if (t.kind == 22) {
+ Expect(13);
+ } else if (t.kind == 25) {
Get();
Expressions(decreases);
- Expect(10);
- } else Error(102);
+ Expect(13);
+ } else Error(105);
}
static void FunctionBody(out Expression! e) {
e = dummyExpr;
- Expect(5);
- if (t.kind == 33) {
+ Expect(6);
+ if (t.kind == 36) {
MatchExpression(out e);
} else if (StartOf(6)) {
Expression(out e);
- } else Error(103);
- Expect(6);
+ } else Error(106);
+ Expect(7);
}
static void Expressions(List<Expression!>! args) {
Expression! e;
Expression(out e);
args.Add(e);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Expression(out e);
args.Add(e);
@@ -665,34 +707,34 @@ List<Expression!>! decreases) { static void PossiblyWildExpression(out Expression! e) {
e = dummyExpr;
- if (t.kind == 32) {
+ if (t.kind == 35) {
Get();
e = new WildcardExpr(token);
} else if (StartOf(6)) {
Expression(out e);
- } else Error(104);
+ } else Error(107);
}
static void MatchExpression(out Expression! e) {
Token! x;
List<MatchCase!> cases = new List<MatchCase!>();
- Expect(33);
+ Expect(36);
x = token;
Expression(out e);
- if (t.kind == 5) {
+ if (t.kind == 6) {
Get();
CaseExpressions(cases);
- Expect(6);
- } else if (t.kind == 6 || t.kind == 34) {
+ Expect(7);
+ } else if (t.kind == 7 || t.kind == 37) {
CaseExpressions(cases);
- } else Error(105);
+ } else Error(108);
e = new MatchExpr(x, e, cases);
}
static void CaseExpressions(List<MatchCase!>! cases) {
MatchCase! c;
- while (t.kind == 34) {
+ while (t.kind == 37) {
CaseExpression(out c);
cases.Add(c);
}
@@ -703,23 +745,23 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(34);
+ Expect(37);
x = token; parseVarScope.PushMarker();
Ident(out id);
- if (t.kind == 23) {
+ if (t.kind == 26) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Ident(out arg);
arguments.Add(new BoundVar(arg, arg.val, new InferredTypeProxy()));
parseVarScope.Push(arg.val, arg.val);
}
- Expect(24);
+ Expect(27);
}
- Expect(35);
+ Expect(38);
Expression(out body);
c = new MatchCase(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -727,16 +769,16 @@ List<Expression!>! decreases) { static void Stmt(List<Statement!>! ss) {
Statement! s;
- while (t.kind == 5) {
+ while (t.kind == 6) {
BlockStmt(out s);
ss.Add(s);
}
if (StartOf(10)) {
OneStmt(out s);
ss.Add(s);
- } else if (t.kind == 7 || t.kind == 11) {
+ } else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(106);
+ } else Error(109);
}
static void OneStmt(out Statement! s) {
@@ -744,113 +786,113 @@ List<Expression!>! decreases) { s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 50: {
+ case 53: {
AssertStmt(out s);
break;
}
- case 51: {
+ case 54: {
AssumeStmt(out s);
break;
}
- case 8: {
+ case 11: {
UseStmt(out s);
break;
}
- case 1: case 23: case 85: case 86: {
+ case 1: case 26: case 88: case 89: {
AssignStmt(out s);
break;
}
- case 41: {
+ case 44: {
HavocStmt(out s);
break;
}
- case 46: {
+ case 49: {
CallStmt(out s);
break;
}
- case 42: {
+ case 45: {
IfStmt(out s);
break;
}
- case 44: {
+ case 47: {
WhileStmt(out s);
break;
}
- case 47: {
+ case 50: {
ForeachStmt(out s);
break;
}
- case 36: {
+ case 39: {
Get();
x = token;
Ident(out id);
- Expect(13);
+ Expect(16);
s = new LabelStmt(x, id.val);
break;
}
- case 37: {
+ case 40: {
Get();
x = token;
if (t.kind == 1) {
Ident(out id);
label = id.val;
}
- Expect(10);
+ Expect(13);
s = new BreakStmt(x, label);
break;
}
- case 38: {
+ case 41: {
Get();
x = token;
- Expect(10);
+ Expect(13);
s = new ReturnStmt(x);
break;
}
- default: Error(107); break;
+ default: Error(110); break;
}
}
static void VarDeclStmts(List<Statement!>! ss) {
VarDecl! d; bool isGhost = false;
- if (t.kind == 7) {
+ if (t.kind == 9) {
Get();
isGhost = true;
}
- Expect(11);
+ Expect(14);
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
IdentTypeRhs(out d, isGhost);
ss.Add(d); parseVarScope.Push(d.Name, d.Name);
}
- Expect(10);
+ Expect(13);
}
static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(50);
+ Expect(53);
x = token;
Expression(out e);
- Expect(10);
+ Expect(13);
s = new AssertStmt(x, e);
}
static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(51);
+ Expect(54);
x = token;
Expression(out e);
- Expect(10);
+ Expect(13);
s = new AssumeStmt(x, e);
}
static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(8);
+ Expect(11);
x = token;
Expression(out e);
- Expect(10);
+ Expect(13);
s = new UseStmt(x, e);
}
@@ -862,7 +904,7 @@ List<Expression!>! decreases) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(39);
+ Expect(42);
x = token;
AssignRhs(out rhs, out ty);
if (rhs != null) {
@@ -872,15 +914,15 @@ List<Expression!>! decreases) { s = new AssignStmt(x, lhs, ty);
}
- Expect(10);
+ Expect(13);
}
static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(41);
+ Expect(44);
x = token;
LhsExpr(out lhs);
- Expect(10);
+ Expect(13);
s = new AssignStmt(x, lhs);
}
@@ -890,11 +932,11 @@ List<Expression!>! decreases) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
- Expect(46);
+ Expect(49);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 12 || t.kind == 39) {
- if (t.kind == 12) {
+ if (t.kind == 15 || t.kind == 42) {
+ if (t.kind == 15) {
Get();
e = ConvertToLocal(e);
if (e is IdentifierExpr) {
@@ -907,12 +949,12 @@ List<Expression!>! decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(39);
+ Expect(42);
CallStmtSubExpr(out e);
} else {
Get();
@@ -928,7 +970,7 @@ List<Expression!>! decreases) { CallStmtSubExpr(out e);
}
}
- Expect(10);
+ Expect(13);
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
@@ -946,19 +988,19 @@ List<Expression!>! decreases) { Statement! s;
Statement els = null;
- Expect(42);
+ Expect(45);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 43) {
+ if (t.kind == 46) {
Get();
- if (t.kind == 42) {
+ if (t.kind == 45) {
IfStmt(out s);
els = s;
- } else if (t.kind == 5) {
+ } else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(108);
+ } else Error(111);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -971,25 +1013,25 @@ List<Expression!>! decreases) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(44);
+ Expect(47);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 19 || t.kind == 22 || t.kind == 45) {
- if (t.kind == 19 || t.kind == 45) {
+ while (t.kind == 22 || t.kind == 25 || t.kind == 48) {
+ if (t.kind == 22 || t.kind == 48) {
isFree = false;
- if (t.kind == 19) {
+ if (t.kind == 22) {
Get();
isFree = true;
}
- Expect(45);
+ Expect(48);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
- Expect(10);
+ Expect(13);
} else {
Get();
PossiblyWildExpressions(decreases);
- Expect(10);
+ Expect(13);
}
}
BlockStmt(out body);
@@ -1005,31 +1047,31 @@ List<Expression!>! decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(47);
+ Expect(50);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
- Expect(23);
+ Expect(26);
Ident(out boundVar);
- if (t.kind == 13) {
+ if (t.kind == 16) {
Get();
Type(out ty);
}
- Expect(48);
+ Expect(51);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 49) {
+ if (t.kind == 52) {
Get();
Expression(out range);
}
- Expect(24);
- Expect(5);
- while (t.kind == 8 || t.kind == 50 || t.kind == 51) {
- if (t.kind == 50) {
+ Expect(27);
+ Expect(6);
+ while (t.kind == 11 || t.kind == 53 || t.kind == 54) {
+ if (t.kind == 53) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 51) {
+ } else if (t.kind == 54) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1040,11 +1082,11 @@ List<Expression!>! decreases) { if (StartOf(11)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 41) {
+ } else if (t.kind == 44) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(109);
- Expect(6);
+ } else Error(112);
+ Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
} else {
@@ -1062,14 +1104,14 @@ List<Expression!>! decreases) { Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 40) {
+ if (t.kind == 43) {
Get();
ReferenceType(out x, out tt);
ty = tt;
} else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else Error(110);
+ } else Error(113);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1077,10 +1119,10 @@ List<Expression!>! decreases) { Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {
+ } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
ObjectExpression(out e);
- } else Error(111);
- while (t.kind == 80 || t.kind == 82) {
+ } else Error(114);
+ while (t.kind == 83 || t.kind == 85) {
SelectOrCallSuffix(ref e);
}
}
@@ -1091,12 +1133,12 @@ List<Expression!>! decreases) { Type optionalType = null; DeterminedAssignmentRhs optionalRhs = null;
Ident(out id);
- if (t.kind == 13) {
+ if (t.kind == 16) {
Get();
Type(out ty);
optionalType = ty;
}
- if (t.kind == 39) {
+ if (t.kind == 42) {
Get();
AssignRhs(out rhs, out newType);
}
@@ -1114,26 +1156,26 @@ List<Expression!>! decreases) { static void Guard(out Expression e) {
Expression! ee; e = null;
- Expect(23);
- if (t.kind == 32) {
+ Expect(26);
+ if (t.kind == 35) {
Get();
e = null;
} else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else Error(112);
- Expect(24);
+ } else Error(115);
+ Expect(27);
}
static void CallStmtSubExpr(out Expression! e) {
e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 23 || t.kind == 85 || t.kind == 86) {
+ } else if (t.kind == 26 || t.kind == 88 || t.kind == 89) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(113);
- while (t.kind == 80 || t.kind == 82) {
+ } else Error(116);
+ while (t.kind == 83 || t.kind == 85) {
SelectOrCallSuffix(ref e);
}
}
@@ -1141,7 +1183,7 @@ List<Expression!>! decreases) { static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 53 || t.kind == 54) {
+ while (t.kind == 56 || t.kind == 57) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1152,7 +1194,7 @@ List<Expression!>! decreases) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 55 || t.kind == 56) {
+ if (t.kind == 58 || t.kind == 59) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1161,23 +1203,23 @@ List<Expression!>! decreases) { }
static void EquivOp() {
- if (t.kind == 53) {
+ if (t.kind == 56) {
Get();
- } else if (t.kind == 54) {
+ } else if (t.kind == 57) {
Get();
- } else Error(114);
+ } else Error(117);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(12)) {
- if (t.kind == 57 || t.kind == 58) {
+ if (t.kind == 60 || t.kind == 61) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 57 || t.kind == 58) {
+ while (t.kind == 60 || t.kind == 61) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1188,7 +1230,7 @@ List<Expression!>! decreases) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 59 || t.kind == 60) {
+ while (t.kind == 62 || t.kind == 63) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1199,11 +1241,11 @@ List<Expression!>! decreases) { }
static void ImpliesOp() {
- if (t.kind == 55) {
+ if (t.kind == 58) {
Get();
- } else if (t.kind == 56) {
+ } else if (t.kind == 59) {
Get();
- } else Error(115);
+ } else Error(118);
}
static void RelationalExpression(out Expression! e0) {
@@ -1217,25 +1259,25 @@ List<Expression!>! decreases) { }
static void AndOp() {
- if (t.kind == 57) {
+ if (t.kind == 60) {
Get();
- } else if (t.kind == 58) {
+ } else if (t.kind == 61) {
Get();
- } else Error(116);
+ } else Error(119);
}
static void OrOp() {
- if (t.kind == 59) {
+ if (t.kind == 62) {
Get();
- } else if (t.kind == 60) {
+ } else if (t.kind == 63) {
Get();
- } else Error(117);
+ } else Error(120);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 70 || t.kind == 71) {
+ while (t.kind == 73 || t.kind == 74) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1245,74 +1287,74 @@ List<Expression!>! decreases) { static void RelOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
switch (t.kind) {
- case 61: {
+ case 64: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
}
- case 14: {
+ case 17: {
Get();
x = token; op = BinaryExpr.Opcode.Lt;
break;
}
- case 15: {
+ case 18: {
Get();
x = token; op = BinaryExpr.Opcode.Gt;
break;
}
- case 62: {
+ case 65: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 63: {
+ case 66: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- case 64: {
+ case 67: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 65: {
+ case 68: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 48: {
+ case 51: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 66: {
+ case 69: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 67: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 68: {
+ case 71: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 69: {
+ case 72: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(118); break;
+ default: Error(121); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 32 || t.kind == 72 || t.kind == 73) {
+ while (t.kind == 35 || t.kind == 75 || t.kind == 76) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1321,23 +1363,23 @@ List<Expression!>! decreases) { static void AddOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 70) {
+ if (t.kind == 73) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 71) {
+ } else if (t.kind == 74) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(119);
+ } else Error(122);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 71) {
+ if (t.kind == 74) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 74 || t.kind == 75) {
+ } else if (t.kind == 77 || t.kind == 78) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1346,29 +1388,29 @@ List<Expression!>! decreases) { SelectExpression(out e);
} else if (StartOf(14)) {
ConstAtomExpression(out e);
- } else Error(120);
+ } else Error(123);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 32) {
+ if (t.kind == 35) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 72) {
+ } else if (t.kind == 75) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 73) {
+ } else if (t.kind == 76) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(121);
+ } else Error(124);
}
static void NegOp() {
- if (t.kind == 74) {
+ if (t.kind == 77) {
Get();
- } else if (t.kind == 75) {
+ } else if (t.kind == 78) {
Get();
- } else Error(122);
+ } else Error(125);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1376,17 +1418,17 @@ List<Expression!>! decreases) { e = dummyExpr;
switch (t.kind) {
- case 76: {
+ case 79: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 77: {
+ case 80: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 78: {
+ case 81: {
Get();
e = new LiteralExpr(token);
break;
@@ -1396,61 +1438,61 @@ List<Expression!>! decreases) { e = new LiteralExpr(token, n);
break;
}
- case 79: {
+ case 82: {
Get();
x = token;
Ident(out dtName);
- Expect(80);
+ Expect(83);
Ident(out id);
elements = new List<Expression!>();
- if (t.kind == 23) {
+ if (t.kind == 26) {
Get();
if (StartOf(6)) {
Expressions(elements);
}
- Expect(24);
+ Expect(27);
}
e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 81: {
+ case 84: {
Get();
x = token;
- Expect(23);
+ Expect(26);
Expression(out e);
- Expect(24);
+ Expect(27);
e = new FreshExpr(x, e);
break;
}
- case 49: {
+ case 52: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(49);
+ Expect(52);
break;
}
- case 5: {
+ case 6: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(6)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
- Expect(6);
+ Expect(7);
break;
}
- case 82: {
+ case 85: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(6)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(83);
+ Expect(86);
break;
}
- default: Error(123); break;
+ default: Error(126); break;
}
}
@@ -1468,13 +1510,13 @@ List<Expression!>! decreases) { static void IdentOrFuncExpression(out Expression! e) {
Token! id; e = dummyExpr; List<Expression!>! args;
Ident(out id);
- if (t.kind == 23) {
+ if (t.kind == 26) {
Get();
args = new List<Expression!>();
if (StartOf(6)) {
Expressions(args);
}
- Expect(24);
+ Expect(27);
e = new FunctionCallExpr(id, id.val, new ImplicitThisExpr(id), args);
}
if (e == dummyExpr) {
@@ -1489,25 +1531,25 @@ List<Expression!>! decreases) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 85) {
+ if (t.kind == 88) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 86) {
+ } else if (t.kind == 89) {
Get();
x = token;
- Expect(23);
+ Expect(26);
Expression(out e);
- Expect(24);
+ Expect(27);
e = new OldExpr(x, e);
- } else if (t.kind == 23) {
+ } else if (t.kind == 26) {
Get();
if (StartOf(15)) {
QuantifierGuts(out e);
} else if (StartOf(6)) {
Expression(out e);
- } else Error(124);
- Expect(24);
- } else Error(125);
+ } else Error(127);
+ Expect(27);
+ } else Error(128);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1515,27 +1557,27 @@ List<Expression!>! decreases) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 80) {
+ if (t.kind == 83) {
Get();
Ident(out id);
- if (t.kind == 23) {
+ if (t.kind == 26) {
Get();
args = new List<Expression!>(); func = true;
if (StartOf(6)) {
Expressions(args);
}
- Expect(24);
+ Expect(27);
e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 82) {
+ } else if (t.kind == 85) {
Get();
x = token;
if (StartOf(6)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 39 || t.kind == 84) {
- if (t.kind == 84) {
+ if (t.kind == 42 || t.kind == 87) {
+ if (t.kind == 87) {
Get();
anyDots = true;
if (StartOf(6)) {
@@ -1548,11 +1590,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (t.kind == 84) {
+ } else if (t.kind == 87) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(126);
+ } else Error(129);
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
@@ -1565,8 +1607,8 @@ List<Expression!>! decreases) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(83);
- } else Error(127);
+ Expect(86);
+ } else Error(130);
}
static void QuantifierGuts(out Expression! q) {
@@ -1579,22 +1621,22 @@ List<Expression!>! decreases) { Triggers trigs = null;
Expression! body;
- if (t.kind == 87 || t.kind == 88) {
+ if (t.kind == 90 || t.kind == 91) {
Forall();
x = token; univ = true;
- } else if (t.kind == 89 || t.kind == 90) {
+ } else if (t.kind == 92 || t.kind == 93) {
Exists();
x = token;
- } else Error(128);
+ } else Error(131);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
}
- while (t.kind == 5) {
+ while (t.kind == 6) {
AttributeOrTrigger(ref attrs, ref trigs);
}
QSep();
@@ -1609,41 +1651,41 @@ List<Expression!>! decreases) { }
static void Forall() {
- if (t.kind == 87) {
+ if (t.kind == 90) {
Get();
- } else if (t.kind == 88) {
+ } else if (t.kind == 91) {
Get();
- } else Error(129);
+ } else Error(132);
}
static void Exists() {
- if (t.kind == 89) {
+ if (t.kind == 92) {
Get();
- } else if (t.kind == 90) {
+ } else if (t.kind == 93) {
Get();
- } else Error(130);
+ } else Error(133);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
List<Expression!> es = new List<Expression!>();
- Expect(5);
- if (t.kind == 13) {
+ Expect(6);
+ if (t.kind == 16) {
AttributeBody(ref attrs);
} else if (StartOf(6)) {
es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(131);
- Expect(6);
+ } else Error(134);
+ Expect(7);
}
static void QSep() {
- if (t.kind == 91) {
+ if (t.kind == 94) {
Get();
- } else if (t.kind == 92) {
+ } else if (t.kind == 95) {
Get();
- } else Error(132);
+ } else Error(135);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1651,13 +1693,13 @@ List<Expression!>! decreases) { List<Attributes.Argument!> aArgs = new List<Attributes.Argument!>();
Attributes.Argument! aArg;
- Expect(13);
+ Expect(16);
Expect(1);
aName = token.val;
if (StartOf(16)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
- while (t.kind == 12) {
+ while (t.kind == 15) {
Get();
AttributeArg(out aArg);
aArgs.Add(aArg);
@@ -1674,7 +1716,7 @@ List<Expression!>! decreases) { } else if (StartOf(6)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(133);
+ } else Error(136);
}
@@ -1697,136 +1739,139 @@ List<Expression!>! decreases) { case 1: s = "ident expected"; break;
case 2: s = "digits expected"; break;
case 3: s = "string expected"; break;
- case 4: s = "class expected"; break;
- case 5: s = "{ expected"; break;
- case 6: s = "} expected"; break;
- case 7: s = "ghost expected"; break;
- case 8: s = "use expected"; break;
- case 9: s = "datatype expected"; break;
- case 10: s = "; expected"; break;
- case 11: s = "var expected"; break;
- case 12: s = ", expected"; break;
- case 13: s = ": expected"; break;
- case 14: s = "< expected"; break;
- case 15: s = "> expected"; break;
- case 16: s = "method expected"; break;
- case 17: s = "returns expected"; break;
- case 18: s = "modifies expected"; break;
- case 19: s = "free expected"; break;
- case 20: s = "requires expected"; break;
- case 21: s = "ensures expected"; break;
- case 22: s = "decreases expected"; break;
- case 23: s = "( expected"; break;
- case 24: s = ") expected"; break;
- case 25: s = "bool expected"; break;
- case 26: s = "int expected"; break;
- case 27: s = "set expected"; break;
- case 28: s = "seq expected"; break;
- case 29: s = "object expected"; break;
- case 30: s = "function expected"; break;
- case 31: s = "reads expected"; break;
- case 32: s = "* expected"; break;
- case 33: s = "match expected"; break;
- case 34: s = "case expected"; break;
- case 35: s = "=> expected"; break;
- case 36: s = "label expected"; break;
- case 37: s = "break expected"; break;
- case 38: s = "return expected"; break;
- case 39: s = ":= expected"; break;
- case 40: s = "new expected"; break;
- case 41: s = "havoc expected"; break;
- case 42: s = "if expected"; break;
- case 43: s = "else expected"; break;
- case 44: s = "while expected"; break;
- case 45: s = "invariant expected"; break;
- case 46: s = "call expected"; break;
- case 47: s = "foreach expected"; break;
- case 48: s = "in expected"; break;
- case 49: s = "| expected"; break;
- case 50: s = "assert expected"; break;
- case 51: s = "assume expected"; break;
- case 52: s = "then expected"; break;
- case 53: s = "<==> expected"; break;
- case 54: s = "\\u21d4 expected"; break;
- case 55: s = "==> expected"; break;
- case 56: s = "\\u21d2 expected"; break;
- case 57: s = "&& expected"; break;
- case 58: s = "\\u2227 expected"; break;
- case 59: s = "|| expected"; break;
- case 60: s = "\\u2228 expected"; break;
- case 61: s = "== expected"; break;
- case 62: s = "<= expected"; break;
- case 63: s = ">= expected"; break;
- case 64: s = "!= expected"; break;
- case 65: s = "!! expected"; break;
- case 66: s = "!in expected"; break;
- case 67: s = "\\u2260 expected"; break;
- case 68: s = "\\u2264 expected"; break;
- case 69: s = "\\u2265 expected"; break;
- case 70: s = "+ expected"; break;
- case 71: s = "- expected"; break;
- case 72: s = "/ expected"; break;
- case 73: s = "% expected"; break;
- case 74: s = "! expected"; break;
- case 75: s = "\\u00ac expected"; break;
- case 76: s = "false expected"; break;
- case 77: s = "true expected"; break;
- case 78: s = "null expected"; break;
- case 79: s = "# expected"; break;
- case 80: s = ". expected"; break;
- case 81: s = "fresh expected"; break;
- case 82: s = "[ expected"; break;
- case 83: s = "] expected"; break;
- case 84: s = ".. expected"; break;
- case 85: s = "this expected"; break;
- case 86: s = "old expected"; break;
- case 87: s = "forall expected"; break;
- case 88: s = "\\u2200 expected"; break;
- case 89: s = "exists expected"; break;
- case 90: s = "\\u2203 expected"; break;
- case 91: s = ":: expected"; break;
- case 92: s = "\\u2022 expected"; break;
- case 93: s = "??? expected"; break;
- case 94: s = "invalid ClassMemberDecl"; break;
- case 95: s = "invalid FunctionDecl"; break;
- case 96: s = "invalid MethodDecl"; break;
- case 97: s = "invalid TypeAndToken"; break;
- case 98: s = "invalid MethodSpec"; break;
- case 99: s = "invalid MethodSpec"; break;
- case 100: s = "invalid Expression"; break;
- case 101: s = "invalid ReferenceType"; break;
- case 102: s = "invalid FunctionSpec"; break;
- case 103: s = "invalid FunctionBody"; break;
- case 104: s = "invalid PossiblyWildExpression"; break;
- case 105: s = "invalid MatchExpression"; break;
- case 106: s = "invalid Stmt"; break;
- case 107: s = "invalid OneStmt"; break;
- case 108: s = "invalid IfStmt"; break;
- case 109: s = "invalid ForeachStmt"; break;
- case 110: s = "invalid AssignRhs"; break;
- case 111: s = "invalid SelectExpression"; break;
- case 112: s = "invalid Guard"; break;
- case 113: s = "invalid CallStmtSubExpr"; break;
- case 114: s = "invalid EquivOp"; break;
- case 115: s = "invalid ImpliesOp"; break;
- case 116: s = "invalid AndOp"; break;
- case 117: s = "invalid OrOp"; break;
- case 118: s = "invalid RelOp"; break;
- case 119: s = "invalid AddOp"; break;
- case 120: s = "invalid UnaryExpression"; break;
- case 121: s = "invalid MulOp"; break;
- case 122: s = "invalid NegOp"; break;
- case 123: s = "invalid ConstAtomExpression"; break;
- case 124: s = "invalid ObjectExpression"; break;
- case 125: s = "invalid ObjectExpression"; break;
- case 126: s = "invalid SelectOrCallSuffix"; break;
- case 127: s = "invalid SelectOrCallSuffix"; break;
- case 128: s = "invalid QuantifierGuts"; break;
- case 129: s = "invalid Forall"; break;
- case 130: s = "invalid Exists"; break;
- case 131: s = "invalid AttributeOrTrigger"; break;
- case 132: s = "invalid QSep"; break;
- case 133: s = "invalid AttributeArg"; 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 = "ghost expected"; break;
+ case 10: s = "static expected"; break;
+ case 11: s = "use expected"; break;
+ case 12: s = "datatype expected"; break;
+ case 13: s = "; expected"; break;
+ case 14: s = "var expected"; break;
+ case 15: s = ", expected"; break;
+ case 16: s = ": expected"; break;
+ case 17: s = "< expected"; break;
+ case 18: s = "> expected"; break;
+ case 19: s = "method expected"; break;
+ case 20: s = "returns expected"; break;
+ case 21: s = "modifies expected"; break;
+ case 22: s = "free expected"; break;
+ case 23: s = "requires expected"; break;
+ case 24: s = "ensures expected"; break;
+ case 25: s = "decreases expected"; break;
+ case 26: s = "( expected"; break;
+ case 27: s = ") expected"; break;
+ case 28: s = "bool expected"; break;
+ case 29: s = "int expected"; break;
+ case 30: s = "set expected"; break;
+ case 31: s = "seq expected"; break;
+ case 32: s = "object expected"; break;
+ case 33: s = "function expected"; break;
+ case 34: s = "reads expected"; break;
+ case 35: s = "* expected"; break;
+ case 36: s = "match expected"; break;
+ case 37: s = "case expected"; break;
+ case 38: s = "=> expected"; break;
+ case 39: s = "label expected"; break;
+ case 40: s = "break expected"; break;
+ case 41: s = "return expected"; break;
+ case 42: s = ":= expected"; break;
+ case 43: s = "new expected"; break;
+ case 44: s = "havoc expected"; break;
+ case 45: s = "if expected"; break;
+ case 46: s = "else expected"; break;
+ case 47: s = "while expected"; break;
+ case 48: s = "invariant expected"; break;
+ case 49: s = "call expected"; break;
+ case 50: s = "foreach expected"; break;
+ case 51: s = "in expected"; break;
+ case 52: s = "| expected"; break;
+ case 53: s = "assert expected"; break;
+ case 54: s = "assume expected"; break;
+ case 55: s = "then expected"; break;
+ case 56: s = "<==> expected"; break;
+ case 57: s = "\\u21d4 expected"; break;
+ case 58: s = "==> expected"; break;
+ case 59: s = "\\u21d2 expected"; break;
+ case 60: s = "&& expected"; break;
+ case 61: s = "\\u2227 expected"; break;
+ case 62: s = "|| expected"; break;
+ case 63: s = "\\u2228 expected"; break;
+ case 64: s = "== expected"; break;
+ case 65: s = "<= expected"; break;
+ case 66: s = ">= expected"; break;
+ case 67: s = "!= expected"; break;
+ case 68: s = "!! expected"; break;
+ case 69: s = "!in expected"; break;
+ case 70: s = "\\u2260 expected"; break;
+ case 71: s = "\\u2264 expected"; break;
+ case 72: s = "\\u2265 expected"; break;
+ case 73: s = "+ expected"; break;
+ case 74: s = "- expected"; break;
+ case 75: s = "/ expected"; break;
+ case 76: s = "% expected"; break;
+ case 77: s = "! expected"; break;
+ case 78: s = "\\u00ac expected"; break;
+ case 79: s = "false expected"; break;
+ case 80: s = "true expected"; break;
+ case 81: s = "null expected"; break;
+ case 82: s = "# expected"; break;
+ case 83: s = ". expected"; break;
+ case 84: s = "fresh expected"; break;
+ case 85: s = "[ expected"; break;
+ case 86: s = "] expected"; break;
+ case 87: s = ".. expected"; break;
+ case 88: s = "this expected"; break;
+ case 89: s = "old expected"; break;
+ case 90: s = "forall expected"; break;
+ case 91: s = "\\u2200 expected"; break;
+ case 92: s = "exists expected"; break;
+ case 93: s = "\\u2203 expected"; break;
+ case 94: s = ":: expected"; break;
+ case 95: s = "\\u2022 expected"; break;
+ case 96: s = "??? expected"; break;
+ case 97: s = "invalid ClassMemberDecl"; break;
+ case 98: s = "invalid FunctionDecl"; break;
+ case 99: s = "invalid MethodDecl"; break;
+ case 100: s = "invalid TypeAndToken"; break;
+ case 101: s = "invalid MethodSpec"; break;
+ case 102: s = "invalid MethodSpec"; break;
+ case 103: s = "invalid Expression"; break;
+ case 104: s = "invalid ReferenceType"; break;
+ case 105: s = "invalid FunctionSpec"; break;
+ case 106: s = "invalid FunctionBody"; break;
+ case 107: s = "invalid PossiblyWildExpression"; break;
+ case 108: s = "invalid MatchExpression"; break;
+ case 109: s = "invalid Stmt"; break;
+ case 110: s = "invalid OneStmt"; break;
+ case 111: s = "invalid IfStmt"; break;
+ case 112: s = "invalid ForeachStmt"; break;
+ case 113: s = "invalid AssignRhs"; break;
+ case 114: s = "invalid SelectExpression"; break;
+ case 115: s = "invalid Guard"; break;
+ case 116: s = "invalid CallStmtSubExpr"; break;
+ case 117: s = "invalid EquivOp"; break;
+ case 118: s = "invalid ImpliesOp"; break;
+ case 119: s = "invalid AndOp"; break;
+ case 120: s = "invalid OrOp"; break;
+ case 121: s = "invalid RelOp"; break;
+ case 122: s = "invalid AddOp"; break;
+ case 123: s = "invalid UnaryExpression"; break;
+ case 124: s = "invalid MulOp"; break;
+ case 125: s = "invalid NegOp"; break;
+ case 126: s = "invalid ConstAtomExpression"; break;
+ case 127: s = "invalid ObjectExpression"; break;
+ case 128: s = "invalid ObjectExpression"; break;
+ case 129: s = "invalid SelectOrCallSuffix"; break;
+ case 130: s = "invalid SelectOrCallSuffix"; break;
+ case 131: s = "invalid QuantifierGuts"; break;
+ case 132: s = "invalid Forall"; break;
+ case 133: s = "invalid Exists"; break;
+ case 134: s = "invalid AttributeOrTrigger"; break;
+ case 135: s = "invalid QSep"; break;
+ case 136: s = "invalid AttributeArg"; break;
default: s = "error " + n; break;
}
@@ -1834,23 +1879,23 @@ List<Expression!>! decreases) { }
static 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, T,x,x,T, T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,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,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,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,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,T,T,x, x,T,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,T,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,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, x,T,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,T,T,x, T,x,T,T, 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,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,T,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,T,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,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,T,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,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,T, x,x,T,T, T,T,T,T, x,T,T,x, x,T,T,x, x,x,x,x, x,x,x},
- {x,T,x,x, 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, T,T,T,x, x,T,T,x, T,x,T,T, 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,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,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,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,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,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, T,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},
- {x,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, 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, T,T,T,T, 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,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,T,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,T,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,T,x, x,T,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, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,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,T,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,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, 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,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,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, T,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,T,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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, 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,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,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,T,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,T,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, T,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,T,x,x, T,T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, T,T,x,T, x,T,T,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, 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,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, 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, 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,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,T, 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},
+ {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,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,T, T,T,T,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,x,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,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, T,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,T,x,x, T,T,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index cf3d8294..88e9d5dc 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -23,41 +23,69 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment);
}
wr.WriteLine("// {0}", prog.Name);
+ ModuleDecl currentModule = null;
+ int indent = 0;
foreach (TopLevelDecl d in prog.Classes) {
+ if (d.Module != currentModule) {
+ if (currentModule != null) {
+ wr.WriteLine("}");
+ }
+ if (d.Module == null) {
+ indent = 0;
+ } else {
+ wr.Write("module ");
+ PrintAttributes(d.Module.Attributes);
+ wr.Write("{0}", d.Module.Name);
+ if (d.Module.Imports.Count != 0) {
+ string sep = "imports ";
+ foreach (string imp in d.Module.Imports) {
+ wr.Write("{0}{1}", sep, imp);
+ sep = ", ";
+ }
+ }
+ wr.WriteLine("{");
+ indent = IndentAmount;
+ }
+ }
wr.WriteLine();
if (d is ClassDecl) {
- PrintClass((ClassDecl)d);
+ PrintClass((ClassDecl)d, indent);
} else {
- PrintDatatype((DatatypeDecl)d);
+ PrintDatatype((DatatypeDecl)d, indent);
}
}
+ if (currentModule != null) {
+ wr.WriteLine("}");
+ }
}
- public void PrintClass(ClassDecl! c) {
+ public void PrintClass(ClassDecl! c, int indent) {
+ Indent(indent);
PrintClassMethodHelper("class", c.Attributes, c.Name, c.TypeArgs);
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
} else {
int state = 0; // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field
wr.WriteLine(" {");
+ int ind = indent + IndentAmount;
foreach (MemberDecl m in c.Members) {
if (m is Method) {
if (state != 0) { wr.WriteLine(); }
- PrintMethod((Method)m);
+ PrintMethod((Method)m, ind);
state = 2;
} else if (m is Field) {
if (state == 2) { wr.WriteLine(); }
- PrintField((Field)m);
+ PrintField((Field)m, ind);
state = 1;
} else if (m is Function) {
if (state != 0) { wr.WriteLine(); }
- PrintFunction((Function)m);
+ PrintFunction((Function)m, ind);
state = 2;
} else {
assert false; // unexpected member
}
}
- wr.WriteLine("}");
+ Indent(indent); wr.WriteLine("}");
}
}
@@ -78,16 +106,18 @@ namespace Microsoft.Dafny { }
}
- public void PrintDatatype(DatatypeDecl! dt) {
+ public void PrintDatatype(DatatypeDecl! dt, int indent) {
+ Indent(indent);
PrintClassMethodHelper("datatype", dt.Attributes, dt.Name, dt.TypeArgs);
if (dt.Ctors.Count == 0) {
wr.WriteLine(" { }");
} else {
wr.WriteLine(" {");
+ int ind = indent + IndentAmount;
foreach (DatatypeCtor ctor in dt.Ctors) {
- PrintCtor(ctor);
+ PrintCtor(ctor, ind);
}
- wr.WriteLine("}");
+ Indent(indent); wr.WriteLine("}");
}
}
@@ -111,8 +141,8 @@ namespace Microsoft.Dafny { }
}
- public void PrintField(Field! field) {
- Indent(IndentAmount);
+ public void PrintField(Field! field, int indent) {
+ Indent(indent);
if (field.IsGhost) {
wr.Write("ghost ");
}
@@ -123,11 +153,11 @@ namespace Microsoft.Dafny { wr.WriteLine(";");
}
- public void PrintFunction(Function! f) {
- Indent(IndentAmount);
+ public void PrintFunction(Function! f, int indent) {
+ Indent(indent);
string k = "function";
if (f.IsUse) { k = "use " + k; }
- if (f.IsClass) { k = "class " + k; }
+ if (f.IsStatic) { k = "static " + k; }
if (!f.IsGhost) { k += " method"; }
PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
PrintFormals(f.Formals);
@@ -138,20 +168,21 @@ namespace Microsoft.Dafny { } else {
wr.WriteLine();
}
- PrintSpec("requires", f.Req, 2 * IndentAmount);
- PrintSpecLine("reads", f.Reads, 2 * IndentAmount);
- PrintSpecLine("decreases", f.Decreases, 2 * IndentAmount);
+ int ind = indent + IndentAmount;
+ PrintSpec("requires", f.Req, ind);
+ PrintSpecLine("reads", f.Reads, ind);
+ PrintSpecLine("decreases", f.Decreases, ind);
if (f.Body != null) {
- Indent(IndentAmount);
+ Indent(indent);
wr.WriteLine("{");
- PrintExtendedExpr(f.Body, IndentAmount + IndentAmount);
- Indent(IndentAmount);
+ PrintExtendedExpr(f.Body, ind);
+ Indent(indent);
wr.WriteLine("}");
}
}
- public void PrintCtor(DatatypeCtor! ctor) {
- Indent(IndentAmount);
+ public void PrintCtor(DatatypeCtor! ctor, int indent) {
+ Indent(indent);
PrintClassMethodHelper("", ctor.Attributes, ctor.Name, ctor.TypeArgs);
if (ctor.Formals.Count != 0) {
PrintFormals(ctor.Formals);
@@ -172,10 +203,10 @@ namespace Microsoft.Dafny { }
}
- public void PrintMethod(Method! method) {
- Indent(IndentAmount);
+ public void PrintMethod(Method! method, int indent) {
+ Indent(indent);
string k = "method";
- if (method.IsClass) { k = "class " + k; }
+ if (method.IsStatic) { k = "static " + k; }
if (method.IsGhost) { k = "ghost " + k; }
PrintClassMethodHelper(k, method.Attributes, method.Name, method.TypeArgs);
PrintFormals(method.Ins);
@@ -190,15 +221,16 @@ namespace Microsoft.Dafny { PrintFormals(method.Outs);
}
wr.WriteLine(method.Body == null ? ";" : ":");
-
- PrintSpec("requires", method.Req, 2 * IndentAmount);
- PrintSpecLine("modifies", method.Mod, 2 * IndentAmount);
- PrintSpec("ensures", method.Ens, 2 * IndentAmount);
- PrintSpecLine("decreases", method.Decreases, 2 * IndentAmount);
+
+ int ind = indent + IndentAmount;
+ PrintSpec("requires", method.Req, ind);
+ PrintSpecLine("modifies", method.Mod, ind);
+ PrintSpec("ensures", method.Ens, ind);
+ PrintSpecLine("decreases", method.Decreases, ind);
if (method.Body != null) {
- Indent(IndentAmount);
- PrintStatement(method.Body, IndentAmount);
+ Indent(indent);
+ PrintStatement(method.Body, ind);
wr.WriteLine();
}
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 953f429a..235c9036 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -36,8 +36,44 @@ namespace Microsoft.Dafny { 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 void ResolveProgram(Program! prog) {
+ // register modules
+ Dictionary<string,ModuleDecl!> modules = new Dictionary<string,ModuleDecl!>();
+ foreach (ModuleDecl m in prog.Modules) {
+ if (modules.ContainsKey(m.Name)) {
+ Error(m, "Duplicate module name: {0}", m.Name);
+ } else {
+ modules.Add(m.Name, m);
+ }
+ }
+ // resolve imports
+ foreach (ModuleDecl m in prog.Modules) {
+ foreach (string imp in m.Imports) {
+ ModuleDecl other;
+ if (modules.TryGetValue(imp, out other)) {
+ assert other != null; // follows from postcondition of TryGetValue
+ importGraph.AddEdge(m, other);
+ } else {
+ Error(m, "module {0} named among imports does not exist", imp);
+ }
+ }
+ }
+ // check for cycles in the import graph
+ List<ModuleDecl!> cycle = importGraph.TryFindCycle();
+ if (cycle != null) {
+ string cy = "";
+ string sep = "";
+ foreach (ModuleDecl m in cycle) {
+ cy = m.Name + sep + cy;
+ sep = " -> ";
+ }
+ Error(cycle[0], "import graph contains a cycle: {0}", cy);
+ }
+
+ // Done with modules; now, do classes and datatypes
+
foreach (TopLevelDecl d in prog.Classes) {
// register the class/datatype name
if (classes.ContainsKey(d.Name)) {
@@ -76,7 +112,7 @@ namespace Microsoft.Dafny { }
}
}
-
+
// resolve each class
Graph<DatatypeDecl!> datatypeDependencies = new Graph<DatatypeDecl!>();
foreach (TopLevelDecl d in prog.Classes) {
@@ -324,7 +360,7 @@ namespace Microsoft.Dafny { /// </summary>
void ResolveFunction(Function! f) {
scope.PushMarker();
- if (f.IsClass) {
+ if (f.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in f.Formals) {
@@ -394,7 +430,7 @@ namespace Microsoft.Dafny { void ResolveMethod(Method! m) {
// Add in-parameters to the scope, but don't care about any duplication errors, since they have already been reported
scope.PushMarker();
- if (m.IsClass) {
+ if (m.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in m.Ins) {
@@ -916,11 +952,11 @@ namespace Microsoft.Dafny { Error(s, "wrong number of method result arguments (got {0}, expected {1})", s.Lhs.Count, method.Outs.Count);
} else {
assert ctype != null; // follows from postcondition of ResolveMember above
- if (!scope.AllowInstance && !method.IsClass && s.Receiver is ThisExpr) {
+ if (!scope.AllowInstance && !method.IsStatic && s.Receiver is ThisExpr) {
// The call really needs an instance, but that instance is given as 'this', which is not
// available in this context. For more details, see comment in the resolution of a
// FunctionCallExpr.
- Error(s.Receiver, "'this' is not allowed in a 'class' context");
+ Error(s.Receiver, "'this' is not allowed in a 'static' context");
}
// build the type substitution map
Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
@@ -1363,7 +1399,7 @@ namespace Microsoft.Dafny { Error(expr, "wrong number of function arguments (got {0}, expected {1})", e.Args.Count, function.Formals.Count);
} else {
assert ctype != null; // follows from postcondition of ResolveMember
- if (!scope.AllowInstance && !function.IsClass && e.Receiver is ThisExpr) {
+ if (!scope.AllowInstance && !function.IsStatic && e.Receiver is ThisExpr) {
// The call really needs an instance, but that instance is given as 'this', which is not
// available in this context. In most cases, occurrences of 'this' inside e.Receiver would
// have been caught in the recursive call to resolve e.Receiver, but not the specific case
@@ -1371,7 +1407,7 @@ namespace Microsoft.Dafny { // in the event that a class function calls another class function (and note that we need the
// type of the receiver in order to find the method, so we could not have made this check
// earlier).
- Error(e.Receiver, "'this' is not allowed in a 'class' context");
+ Error(e.Receiver, "'this' is not allowed in a 'static' context");
}
// build the type substitution map
Dictionary<TypeParameter!,Type!> subst = new Dictionary<TypeParameter!,Type!>();
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index a1895c0c..8c7a1b15 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -133,7 +133,7 @@ public class Scanner { start[8804] = 38;
start[8805] = 39;
}
- const int noSym = 93;
+ const int noSym = 96;
static short[] start = new short[16385];
@@ -275,50 +275,53 @@ public class Scanner { static void CheckLiteral() {
switch (t.val) {
- case "class": t.kind = 4; break;
- case "ghost": t.kind = 7; break;
- case "use": t.kind = 8; break;
- case "datatype": t.kind = 9; break;
- case "var": t.kind = 11; break;
- case "method": t.kind = 16; break;
- case "returns": t.kind = 17; break;
- case "modifies": t.kind = 18; break;
- case "free": t.kind = 19; break;
- case "requires": t.kind = 20; break;
- case "ensures": t.kind = 21; break;
- case "decreases": t.kind = 22; break;
- case "bool": t.kind = 25; break;
- case "int": t.kind = 26; break;
- case "set": t.kind = 27; break;
- case "seq": t.kind = 28; break;
- case "object": t.kind = 29; break;
- case "function": t.kind = 30; break;
- case "reads": t.kind = 31; break;
- case "match": t.kind = 33; break;
- case "case": t.kind = 34; break;
- case "label": t.kind = 36; break;
- case "break": t.kind = 37; break;
- case "return": t.kind = 38; break;
- case "new": t.kind = 40; break;
- case "havoc": t.kind = 41; break;
- case "if": t.kind = 42; break;
- case "else": t.kind = 43; break;
- case "while": t.kind = 44; break;
- case "invariant": t.kind = 45; break;
- case "call": t.kind = 46; break;
- case "foreach": t.kind = 47; break;
- case "in": t.kind = 48; break;
- case "assert": t.kind = 50; break;
- case "assume": t.kind = 51; break;
- case "then": t.kind = 52; break;
- case "false": t.kind = 76; break;
- case "true": t.kind = 77; break;
- case "null": t.kind = 78; break;
- case "fresh": t.kind = 81; break;
- case "this": t.kind = 85; break;
- case "old": t.kind = 86; break;
- case "forall": t.kind = 87; break;
- case "exists": t.kind = 89; break;
+ case "module": t.kind = 4; break;
+ case "imports": t.kind = 5; break;
+ case "class": t.kind = 8; break;
+ case "ghost": t.kind = 9; break;
+ case "static": t.kind = 10; break;
+ case "use": t.kind = 11; break;
+ case "datatype": t.kind = 12; break;
+ case "var": t.kind = 14; break;
+ case "method": t.kind = 19; break;
+ case "returns": t.kind = 20; break;
+ case "modifies": t.kind = 21; break;
+ case "free": t.kind = 22; break;
+ case "requires": t.kind = 23; break;
+ case "ensures": t.kind = 24; break;
+ case "decreases": t.kind = 25; break;
+ case "bool": t.kind = 28; break;
+ case "int": t.kind = 29; break;
+ case "set": t.kind = 30; break;
+ case "seq": t.kind = 31; break;
+ case "object": t.kind = 32; break;
+ case "function": t.kind = 33; break;
+ case "reads": t.kind = 34; break;
+ case "match": t.kind = 36; break;
+ case "case": t.kind = 37; break;
+ case "label": t.kind = 39; break;
+ case "break": t.kind = 40; break;
+ case "return": t.kind = 41; break;
+ case "new": t.kind = 43; break;
+ case "havoc": t.kind = 44; break;
+ case "if": t.kind = 45; break;
+ case "else": t.kind = 46; break;
+ case "while": t.kind = 47; break;
+ case "invariant": t.kind = 48; break;
+ case "call": t.kind = 49; break;
+ case "foreach": t.kind = 50; break;
+ case "in": t.kind = 51; break;
+ case "assert": t.kind = 53; break;
+ case "assume": t.kind = 54; break;
+ case "then": t.kind = 55; break;
+ case "false": t.kind = 79; break;
+ case "true": t.kind = 80; break;
+ case "null": t.kind = 81; break;
+ case "fresh": t.kind = 84; break;
+ case "this": t.kind = 88; break;
+ case "old": t.kind = 89; break;
+ case "forall": t.kind = 90; break;
+ case "exists": t.kind = 92; break;
default: break;
}
@@ -348,119 +351,119 @@ public class Scanner { case 4:
{t.kind = 3; goto done;}
case 5:
- {t.kind = 5; goto done;}
- case 6:
{t.kind = 6; goto done;}
+ case 6:
+ {t.kind = 7; goto done;}
case 7:
- {t.kind = 10; goto done;}
+ {t.kind = 13; goto done;}
case 8:
- {t.kind = 12; goto done;}
+ {t.kind = 15; goto done;}
case 9:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 17;}
else if (ch == ':') {buf.Append(ch); NextCh(); goto case 52;}
- else {t.kind = 13; goto done;}
+ else {t.kind = 16; goto done;}
case 10:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 19;}
- else {t.kind = 14; goto done;}
+ else {t.kind = 17; goto done;}
case 11:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 31;}
- else {t.kind = 15; goto done;}
+ else {t.kind = 18; goto done;}
case 12:
- {t.kind = 23; goto done;}
+ {t.kind = 26; goto done;}
case 13:
- {t.kind = 24; goto done;}
+ {t.kind = 27; goto done;}
case 14:
- {t.kind = 32; goto done;}
+ {t.kind = 35; goto done;}
case 15:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 16;}
else if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
else {t.kind = noSym; goto done;}
case 16:
- {t.kind = 35; goto done;}
+ {t.kind = 38; goto done;}
case 17:
- {t.kind = 39; goto done;}
+ {t.kind = 42; goto done;}
case 18:
if (ch == '|') {buf.Append(ch); NextCh(); goto case 29;}
- else {t.kind = 49; goto done;}
+ else {t.kind = 52; goto done;}
case 19:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
- else {t.kind = 62; goto done;}
+ else {t.kind = 65; goto done;}
case 20:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 21;}
else {t.kind = noSym; goto done;}
case 21:
- {t.kind = 53; goto done;}
+ {t.kind = 56; goto done;}
case 22:
- {t.kind = 54; goto done;}
+ {t.kind = 57; goto done;}
case 23:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
- else {t.kind = 61; goto done;}
+ else {t.kind = 64; goto done;}
case 24:
- {t.kind = 55; goto done;}
+ {t.kind = 58; goto done;}
case 25:
- {t.kind = 56; goto done;}
+ {t.kind = 59; goto done;}
case 26:
if (ch == '&') {buf.Append(ch); NextCh(); goto case 27;}
else {t.kind = noSym; goto done;}
case 27:
- {t.kind = 57; goto done;}
+ {t.kind = 60; goto done;}
case 28:
- {t.kind = 58; goto done;}
+ {t.kind = 61; goto done;}
case 29:
- {t.kind = 59; goto done;}
+ {t.kind = 62; goto done;}
case 30:
- {t.kind = 60; goto done;}
- case 31:
{t.kind = 63; goto done;}
+ case 31:
+ {t.kind = 66; goto done;}
case 32:
if (ch == '=') {buf.Append(ch); NextCh(); goto case 33;}
else if (ch == '!') {buf.Append(ch); NextCh(); goto case 34;}
else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 35;}
- else {t.kind = 74; goto done;}
+ else {t.kind = 77; goto done;}
case 33:
- {t.kind = 64; goto done;}
+ {t.kind = 67; goto done;}
case 34:
- {t.kind = 65; goto done;}
+ {t.kind = 68; goto done;}
case 35:
if (ch == 'n') {buf.Append(ch); NextCh(); goto case 36;}
else {t.kind = noSym; goto done;}
case 36:
- {t.kind = 66; goto done;}
+ {t.kind = 69; goto done;}
case 37:
- {t.kind = 67; goto done;}
+ {t.kind = 70; goto done;}
case 38:
- {t.kind = 68; goto done;}
+ {t.kind = 71; goto done;}
case 39:
- {t.kind = 69; goto done;}
+ {t.kind = 72; goto done;}
case 40:
- {t.kind = 70; goto done;}
+ {t.kind = 73; goto done;}
case 41:
- {t.kind = 71; goto done;}
+ {t.kind = 74; goto done;}
case 42:
- {t.kind = 72; goto done;}
+ {t.kind = 75; goto done;}
case 43:
- {t.kind = 73; goto done;}
+ {t.kind = 76; goto done;}
case 44:
- {t.kind = 75; goto done;}
+ {t.kind = 78; goto done;}
case 45:
- {t.kind = 79; goto done;}
+ {t.kind = 82; goto done;}
case 46:
if (ch == '.') {buf.Append(ch); NextCh(); goto case 49;}
- else {t.kind = 80; goto done;}
+ else {t.kind = 83; goto done;}
case 47:
- {t.kind = 82; goto done;}
+ {t.kind = 85; goto done;}
case 48:
- {t.kind = 83; goto done;}
+ {t.kind = 86; goto done;}
case 49:
- {t.kind = 84; goto done;}
+ {t.kind = 87; goto done;}
case 50:
- {t.kind = 88; goto done;}
+ {t.kind = 91; goto done;}
case 51:
- {t.kind = 90; goto done;}
+ {t.kind = 93; goto done;}
case 52:
- {t.kind = 91; goto done;}
+ {t.kind = 94; goto done;}
case 53:
- {t.kind = 92; goto done;}
+ {t.kind = 95; goto done;}
case 54: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/SccGraph.ssc b/Source/Dafny/SccGraph.ssc index 3705be76..e508d129 100644 --- a/Source/Dafny/SccGraph.ssc +++ b/Source/Dafny/SccGraph.ssc @@ -10,8 +10,10 @@ namespace Microsoft.Dafny { public readonly List<Vertex!>! Successors = new List<Vertex!>();
public Vertex SccRepresentative; // null if not computed or if the vertex represents itself
public List<Vertex!> SccMembers; // non-null only for the representative of the SCC
- // the following fields are used during the computation of SCCs:
+ public Dictionary<Vertex,object> downwardClosure; // irrefexive, transitive closure; null if not computed
+ // the following field is used during the computation of SCCs and of reachability
public VisitedStatus Visited;
+ // the following fields are used during the computation of SCCs:
public int DfNumber;
public int LowLink;
@@ -155,5 +157,82 @@ namespace Microsoft.Dafny { }
}
}
+
+ /// <summary>
+ /// Returns null if the graph has no cycles. If the graph does contain some cycle, returns the list of
+ /// vertices on one such cycle.
+ /// </summary>
+ public List<Node> TryFindCycle() {
+ // reset all visited information
+ foreach (Vertex v in vertices.Values) {
+ v.Visited = VisitedStatus.Unvisited;
+ }
+
+ foreach (Vertex v in vertices.Values) {
+ assert v.Visited != VisitedStatus.OnStack;
+ if (v.Visited == VisitedStatus.Unvisited) {
+ List<Vertex!> cycle = CycleSearch(v);
+ if (cycle != null) {
+ List<Node> nodes = new List<Node>();
+ foreach (Vertex v in cycle) {
+ nodes.Add(v.N);
+ }
+ return nodes; // a cycle is found
+ }
+ }
+ }
+ return null; // there are no cycles
+ }
+
+ /// <summary>
+ /// A return of null means there are no cycles involving any vertex in the subtree rooted at v.
+ /// A non-null return means a cycle has been found. Then:
+ /// If v.Visited == Visited, then the entire cycle is described in the returned list.
+ /// If v.Visited == OnStack, then the cycle consists of the vertices strictly deeper than
+ /// w on the stack followed by the vertices (in reverse order) in the returned list, where
+ /// w is the first vertex in the list returned.
+ /// </summary>
+ List<Vertex!> CycleSearch(Vertex! v)
+ requires v.Visited == VisitedStatus.Unvisited;
+ ensures v.Visited != VisitedStatus.Unvisited;
+ ensures result == null ==> v.Visited == VisitedStatus.Visited;
+ ensures result != null ==> result.Count != 0;
+ {
+ v.Visited = VisitedStatus.OnStack;
+ foreach (Vertex succ in v.Successors) {
+ // todo: I would use a 'switch' statement, but there seems to be a bug in the Spec# compiler's type checking.
+ if (succ.Visited == VisitedStatus.Visited) {
+ // there is no cycle in the subtree rooted at succ, hence this path does not give rise to any cycles
+ } else if (succ.Visited == VisitedStatus.OnStack) {
+ // we found a cycle!
+ List<Vertex!> cycle = new List<Vertex!>();
+ cycle.Add(succ);
+ if (v == succ) {
+ // entire cycle has been found
+ v.Visited = VisitedStatus.Visited;
+ }
+ return cycle;
+ } else {
+ assert succ.Visited == VisitedStatus.Unvisited;
+ List<Vertex!> cycle = CycleSearch(succ);
+ if (cycle != null) {
+ if (succ.Visited == VisitedStatus.Visited) {
+ // the entire cycle has been collected
+ v.Visited = VisitedStatus.Visited;
+ return cycle;
+ } else {
+ cycle.Add(succ);
+ if (v == cycle[0]) {
+ // the entire cycle has been collected and we are the first to find out
+ v.Visited = VisitedStatus.Visited;
+ }
+ return cycle;
+ }
+ }
+ }
+ }
+ v.Visited = VisitedStatus.Visited; // there are no cycles from here on
+ return null;
+ }
}
}
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index 89a02ce7..fbf9c361 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -425,7 +425,7 @@ namespace Microsoft.Dafny { args.Add(new Bpl.IdentifierExpr(f.tok, bv));
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
- if (f.IsClass) {
+ if (f.IsStatic) {
bvThis = null;
bvThisIdExpr = null;
} else {
@@ -460,8 +460,8 @@ namespace Microsoft.Dafny { }
Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);
- if (!f.IsClass) {
- assert bvThisIdExpr != null; // set to non-null value above when !f.IsClass
+ if (!f.IsStatic) {
+ assert bvThisIdExpr != null; // set to non-null value above when !f.IsStatic
ante = Bpl.Expr.And(Bpl.Expr.Neq(bvThisIdExpr, predef.Null), ante);
}
foreach (Expression req in f.Req) {
@@ -495,7 +495,7 @@ namespace Microsoft.Dafny { args.Add(new Bpl.IdentifierExpr(f.tok, bv));
Bpl.BoundVariable bvThis;
Bpl.Expr bvThisIdExpr;
- if (f.IsClass) {
+ if (f.IsStatic) {
bvThis = null;
bvThisIdExpr = null;
} else {
@@ -841,7 +841,7 @@ namespace Microsoft.Dafny { bvars.Add(h0Var); bvars.Add(h1Var);
f0args.Add(h0);
f1args.Add(h1);
- if (!f.IsClass) {
+ if (!f.IsStatic) {
Bpl.BoundVariable thVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
Bpl.Expr th = new Bpl.IdentifierExpr(f.tok, thVar);
bvars.Add(thVar);
@@ -932,7 +932,7 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// parameters of the procedure
Bpl.VariableSeq inParams = new Bpl.VariableSeq();
- if (!f.IsClass) {
+ if (!f.IsStatic) {
Bpl.Expr wh = Bpl.Expr.And(
Bpl.Expr.Neq(new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), predef.Null),
etran.GoodRef(f.tok, new Bpl.IdentifierExpr(f.tok, "this", predef.RefType), Resolver.GetThisType(f.tok, (!)f.EnclosingClass)));
@@ -1025,7 +1025,7 @@ namespace Microsoft.Dafny { assert e.Function != null; // follows from the fact that expr has been successfully resolved
// check well-formedness of receiver
Bpl.Expr r = IsTotal(e.Receiver, etran);
- if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {
+ if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null));
}
// check well-formedness of the other parameters
@@ -1180,7 +1180,7 @@ namespace Microsoft.Dafny { assert e.Function != null; // follows from the fact that expr has been successfully resolved
// check well-formedness of receiver
CheckWellformed(e.Receiver, func, Position.Neither, locals, builder, etran);
- if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {
+ if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {
CheckNonNull(expr.tok, e.Receiver, builder, etran);
}
// check well-formedness of the other parameters
@@ -1218,15 +1218,17 @@ namespace Microsoft.Dafny { builder.Add(Assert(expr.tok, q, "insufficient reads clause to invoke function"));
// finally, check that the decreases measure goes down
- List<Expression!> contextDecreases = func.Decreases;
- if (contextDecreases.Count == 0) {
- contextDecreases = func.Reads; // use its reads clause instead
- }
- List<Expression!> calleeDecreases = e.Function.Decreases;
- if (calleeDecreases.Count == 0) {
- calleeDecreases = e.Function.Reads; // use its reads clause instead
+ if (((!)e.Function.EnclosingClass).Module == ((!)func.EnclosingClass).Module) {
+ List<Expression!> contextDecreases = func.Decreases;
+ if (contextDecreases.Count == 0) {
+ contextDecreases = func.Reads; // use its reads clause instead
+ }
+ List<Expression!> calleeDecreases = e.Function.Decreases;
+ if (calleeDecreases.Count == 0) {
+ calleeDecreases = e.Function.Reads; // use its reads clause instead
+ }
+ CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
- CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, e.Receiver, substMap, etran, builder);
}
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
@@ -1419,7 +1421,7 @@ namespace Microsoft.Dafny { 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));
- if (!f.IsClass) {
+ if (!f.IsStatic) {
args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType), true));
}
foreach (Formal p in f.Formals) {
@@ -1450,7 +1452,7 @@ namespace Microsoft.Dafny { Bpl.VariableSeq inParams = new Bpl.VariableSeq();
Bpl.VariableSeq outParams = new Bpl.VariableSeq();
- if (!m.IsClass) {
+ if (!m.IsStatic) {
Bpl.Expr wh = Bpl.Expr.And(
Bpl.Expr.Neq(new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), predef.Null),
etran.GoodRef(m.tok, new Bpl.IdentifierExpr(m.tok, "this", predef.RefType), Resolver.GetThisType(m.tok, (!)m.EnclosingClass)));
@@ -1786,7 +1788,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "call statement");
Bpl.ExprSeq ins = new Bpl.ExprSeq();
assert s.Method != null; // follows from the fact that stmt has been successfully resolved
- if (!s.Method.IsClass) {
+ if (!s.Method.IsStatic) {
ins.Add(etran.TrExpr(s.Receiver));
}
@@ -1843,9 +1845,9 @@ namespace Microsoft.Dafny { }
// Check termination
- if (currentMethod.Decreases.Count == 0 || exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
+ if (exists{Expression e in currentMethod.Decreases; e is WildcardExpr}) {
// omit termination checking for calls in this context
- } else {
+ } else if (((!)currentMethod.EnclosingClass).Module == ((!)s.Method.EnclosingClass).Module) {
CheckCallTermination(stmt.Tok, currentMethod.Decreases, s.Method.Decreases, s.Receiver, substMap, etran, builder);
}
@@ -2575,7 +2577,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type));
Bpl.ExprSeq args = new Bpl.ExprSeq();
args.Add(HeapExpr);
- if (!e.Function.IsClass) {
+ if (!e.Function.IsStatic) {
args.Add(TrExpr(e.Receiver));
}
for (int i = 0; i < e.Args.Count; i++) {
@@ -2795,7 +2797,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(e.tok, ((!)e.Function).FullName + "#use", translator.TrType((!)e.Type));
Bpl.ExprSeq args = new Bpl.ExprSeq();
args.Add(HeapExpr);
- if (!e.Function.IsClass) {
+ if (!e.Function.IsStatic) {
args.Add(TrExpr(e.Receiver));
}
foreach (Expression ee in e.Args) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 3186ae01..5dadda4b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -12,23 +12,23 @@ class MyClass<T, U> { ensures t == t;
ensures old(null) != this;
{
- x := 12;
- while (x < 100)
- invariant x <= 100;
- {
- x := x + 17;
- if (x % 20 == 3) {
- x := this.x + 1;
- } else {
- this.x := x + 0;
+ x := 12;
+ while (x < 100)
+ invariant x <= 100;
+ {
+ x := x + 17;
+ if (x % 20 == 3) {
+ x := this.x + 1;
+ } else {
+ this.x := x + 0;
+ }
+ call t, u, v := M(true, lotsaObjects)
+ var to: MyClass<T,U>;
+ call to, u, v := M(true, lotsaObjects)
+ call to, u, v := to.M(true, lotsaObjects)
+ assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
- call t, u, v := M(true, lotsaObjects)
- var to: MyClass<T,U>;
- call to, u, v := M(true, lotsaObjects)
- call to, u, v := to.M(true, lotsaObjects)
- assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
}
- }
function F(x: int, y: int, h: WildData, k: WildData): WildData
{
@@ -122,144 +122,154 @@ Execution trace: (0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(162,7): Error: possible division by zero
+
+Dafny program verifier finished with 22 verified, 9 errors
+
+-------------------- Definedness.dfy --------------------
+Definedness.dfy(8,7): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(169,16): Error: possible division by zero
+Definedness.dfy(15,16): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(178,16): Error: target object may be null
+Definedness.dfy(24,16): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(179,21): Error: target object may be null
+Definedness.dfy(25,21): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(180,17): Error: possible division by zero
+Definedness.dfy(26,17): Error: possible division by zero
Execution trace:
(0,0): anon0
-SmallTests.dfy(187,16): Error: target object may be null
+Definedness.dfy(33,16): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(204,18): Error: target object may be null
+Definedness.dfy(50,18): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(209,18): Error: target object may be null
+Definedness.dfy(55,18): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(231,9): Error: LHS expression must be well defined
+Definedness.dfy(77,9): Error: LHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(232,12): Error: LHS expression must be well defined
+Definedness.dfy(78,12): Error: LHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(233,7): Error: RHS expression must be well defined
+Definedness.dfy(79,7): Error: RHS expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(238,18): Error: assert condition must be well defined
+Definedness.dfy(84,18): Error: assert condition must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(239,5): Error: assume condition must be well defined
+Definedness.dfy(85,5): Error: assume condition must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(244,16): Error: if guard must be well defined
+Definedness.dfy(90,16): Error: if guard must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(251,19): Error: loop guard must be well defined
+Definedness.dfy(97,19): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(251,5): anon8_LoopHead
+ Definedness.dfy(97,5): anon8_LoopHead
(0,0): anon8_LoopBody
- SmallTests.dfy(251,5): anon9_Else
+ Definedness.dfy(97,5): anon9_Else
(0,0): anon3
-SmallTests.dfy(260,23): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(106,23): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(259,5): anon13_LoopHead
+ Definedness.dfy(105,5): anon13_LoopHead
(0,0): anon13_LoopBody
(0,0): anon14_Then
-SmallTests.dfy(266,17): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(112,17): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(259,5): anon13_LoopHead
+ Definedness.dfy(105,5): anon13_LoopHead
(0,0): anon13_LoopBody
- SmallTests.dfy(259,5): anon14_Else
+ Definedness.dfy(105,5): anon14_Else
(0,0): anon3
(0,0): anon15_Then
(0,0): anon6
- SmallTests.dfy(265,5): anon16_LoopHead
+ Definedness.dfy(111,5): anon16_LoopHead
(0,0): anon16_LoopBody
(0,0): anon17_Then
-SmallTests.dfy(276,22): Error: loop invariant must be well defined
+Definedness.dfy(122,22): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(275,5): anon7_LoopHead
+ Definedness.dfy(121,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(276,22): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-SmallTests.dfy(277,17): Error: decreases expression must be well defined at top of each loop iteration
+Definedness.dfy(123,17): Error: decreases expression must be well defined at top of each loop iteration
Execution trace:
(0,0): anon0
- SmallTests.dfy(275,5): anon7_LoopHead
+ Definedness.dfy(121,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(286,24): Error: loop guard must be well defined
+Definedness.dfy(132,24): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(286,5): anon7_LoopHead
+ Definedness.dfy(132,5): anon7_LoopHead
(0,0): anon7_LoopBody
- SmallTests.dfy(286,5): anon8_Else
+ Definedness.dfy(132,5): anon8_Else
(0,0): anon3
-SmallTests.dfy(305,24): Error: loop guard must be well defined
+Definedness.dfy(151,24): Error: loop guard must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(299,5): anon13_LoopHead
+ Definedness.dfy(145,5): anon13_LoopHead
(0,0): anon13_LoopBody
- SmallTests.dfy(299,5): anon14_Else
+ Definedness.dfy(145,5): anon14_Else
(0,0): anon3
(0,0): anon15_Then
(0,0): anon6
- SmallTests.dfy(305,5): anon16_LoopHead
+ Definedness.dfy(151,5): anon16_LoopHead
(0,0): anon16_LoopBody
- SmallTests.dfy(305,5): anon17_Else
+ Definedness.dfy(151,5): anon17_Else
(0,0): anon9
-SmallTests.dfy(326,44): Error: loop invariant must be well defined
+Definedness.dfy(172,44): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(316,5): anon16_LoopHead
+ Definedness.dfy(162,5): anon16_LoopHead
(0,0): anon16_LoopBody
- SmallTests.dfy(316,5): anon17_Else
+ Definedness.dfy(162,5): anon17_Else
(0,0): anon3
(0,0): anon18_Then
(0,0): anon6
- SmallTests.dfy(324,5): anon19_LoopHead
+ Definedness.dfy(170,5): anon19_LoopHead
(0,0): anon19_LoopBody
(0,0): anon20_Then
-SmallTests.dfy(347,21): Error: collection expression must be well defined
+Definedness.dfy(193,21): Error: collection expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(349,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
Execution trace:
(0,0): anon0
-SmallTests.dfy(351,33): Error: range expression must be well defined
+Definedness.dfy(197,33): Error: range expression must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(357,18): Error: RHS of assignment must be well defined
+Definedness.dfy(203,18): Error: RHS of assignment must be well defined
Execution trace:
(0,0): anon0
-SmallTests.dfy(366,23): Error: loop invariant must be well defined
+Definedness.dfy(212,23): Error: loop invariant must be well defined
Execution trace:
(0,0): anon0
- SmallTests.dfy(364,5): anon7_LoopHead
+ Definedness.dfy(210,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-SmallTests.dfy(366,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 43 verified, 38 errors
+Dafny program verifier finished with 21 verified, 29 errors
+
+-------------------- Modules0.dfy --------------------
+Modules0.dfy(13,7): Error: module T named among imports does not exist
+Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G
+Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
+3 resolution/type errors detected in Modules0.dfy
-------------------- Queue.dfy --------------------
diff --git a/Test/dafny0/BinaryTree.dfy b/Test/dafny0/BinaryTree.dfy index 5f56cf40..276b6c0e 100644 --- a/Test/dafny0/BinaryTree.dfy +++ b/Test/dafny0/BinaryTree.dfy @@ -48,7 +48,7 @@ class IntSet { footprint := root.footprint + {this};
}
- class method InsertHelper(x: int, n: Node) returns (m: Node)
+ static method InsertHelper(x: int, n: Node) returns (m: Node)
requires n == null || n.Valid();
modifies n.footprint;
ensures m != null && m.Valid();
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy new file mode 100644 index 00000000..4bf6ae30 --- /dev/null +++ b/Test/dafny0/Definedness.dfy @@ -0,0 +1,218 @@ +// ----------------- wellformed specifications ----------------------
+
+class SoWellformed {
+ var xyz: int;
+ var next: SoWellformed;
+
+ function F(x: int): int
+ { 5 / x } // error: possible division by zero
+
+ function G(x: int): int
+ requires 0 < x;
+ { 5 / x }
+
+ function H(x: int): int
+ decreases 5/x; // error: possible division by zero
+ { 12 }
+
+ function I(x: int): int
+ requires 0 < x;
+ decreases 5/x;
+ { 12 }
+
+ method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ requires a.xyz == 7; // error: not always defined
+ ensures c ==> d.xyz == -7; // error: not always defined
+ decreases 5 / b; // error: not always defined
+ {
+ c := false;
+ }
+
+ method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ decreases 5 / b;
+ requires a.next != null; // error: not always defined
+ requires a.next.xyz == 7; // this is well-defined, given that the previous line is
+ requires b < -2;
+ ensures 0 <= b ==> d.xyz == -7 && !c;
+ {
+ c := true;
+ }
+
+ method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
+ modifies a.next; // this may not be well-defined, but that's okay for modifies clauses
+ {
+ c := true;
+ }
+
+ method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
+ requires next != null;
+ modifies this;
+ ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
+
+ method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ requires next != null;
+ modifies s;
+ ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
+
+ method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ requires next != null && this !in s;
+ modifies s;
+ ensures next.xyz < 100; // fine
+}
+
+// ---------------------- welldefinedness checks for statements -------------------
+
+class StatementTwoShoes {
+ var x: int;
+
+ function method F(b: int): StatementTwoShoes
+ requires 0 <= b;
+ {
+ this
+ }
+
+ method M(p: StatementTwoShoes, a: int)
+ modifies this, p;
+ {
+ p.x := a; // error: receiver may be null
+ F(a).x := a; // error: LHS may not be well defined
+ x := F(a-10).x; // error: RHS may not be well defined
+ }
+
+ method N(a: int, b: int)
+ {
+ assert 5 / a == 5 / a; // error: expression may not be well defined
+ assume 20 / b == 5; // error: expression may not be well defined
+ }
+
+ method O(a: int) returns (b: int)
+ {
+ if (20 / a == 5) { // error: expression may not be well defined
+ b := a;
+ }
+ }
+
+ method P(a: int)
+ {
+ while (20 / a == 5) { // error: expression may not be well defined
+ break;
+ }
+ }
+
+ method Q(a: int, b: int)
+ {
+ var i := 1;
+ while (i < a)
+ decreases F(i), F(a), a - i; // error: component 1 may not be well defined
+ {
+ i := i + 1;
+ }
+ i := 1;
+ while (i < a)
+ decreases F(b), a - i; // error: component 0 may not be well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method R(a: int)
+ {
+ var i := 0;
+ while (i < 100) // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption
+ invariant F(a) != null; // error: expression may not be well defined, and error: loop invariant may not hold
+ decreases F(a), 100 - i; // error: component 0 not well defined
+ {
+ i := i + 1;
+ }
+ }
+
+ method S(a: int)
+ {
+ var j := 0;
+ while (20 / a == 5 && j < 100) // error: guard may not be well defined
+ invariant j <= 100;
+ decreases F(101 - j), 100 - j;
+ {
+ j := j + 1;
+ }
+ }
+
+ method T(a: int)
+ requires a != 0 && 20 / a == 5;
+ {
+ var k := a;
+ var j := 0;
+ while (20 / k == 5 && j < 100) // fine
+ decreases 100 - j;
+ {
+ j := j + 1;
+ }
+ j := 0;
+ while (20 / k == 5 && j < 100) // error: guard may not be well defined
+ decreases 100 - j;
+ {
+ havoc k;
+ j := j + 1;
+ }
+ }
+
+ method U()
+ {
+ var i := 0;
+ while (i < 100)
+ invariant i <= 100;
+ decreases 100 - i;
+ invariant F(123 - i) == this;
+ {
+ i := i + 1;
+ }
+ i := 0;
+ while (i < 100)
+ decreases 100 - i;
+ invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined
+ {
+ i := i + 1;
+ if (i == 77) { i := i + 1; }
+ }
+ }
+
+ use function G(w: int): int { 5 }
+ function method H(x: int): int;
+
+ method V(s: set<StatementTwoShoes>, a: int, b: int)
+ modifies s;
+ {
+ use G(12 / b); // fine, because there are no welldefinedness checks on use statements
+ foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
+ {
+ assume 0 <= m.x;
+ assert m.x < 1000;
+ use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
+ m.x := m.x + 1;
+ }
+ foreach (m in s + {F(a)}) // error: collection expression may not be well defined
+ {
+ m.x := 5; // error: possible modifies clause violation
+ }
+ foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
+ {
+ m.x := H(m.x);
+ }
+ foreach (m in s)
+ {
+ m.x := 100 / m.x; // error: RhS may not be well defined
+ }
+ }
+
+ method W(x: int)
+ {
+ var i := 0;
+ while (i < 100)
+ // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking
+ invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially
+ decreases 100 - i;
+ {
+ i := i + 1;
+ }
+ }
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy new file mode 100644 index 00000000..cf616fba --- /dev/null +++ b/Test/dafny0/Modules0.dfy @@ -0,0 +1,34 @@ +module M {
+ class T { }
+ class U { }
+}
+
+module N {
+ class T { } // error: duplicate class name
+}
+
+module U imports N { // fine, despite the fact that a class is called U--module names are in their own name space
+}
+
+module V imports T { // error: T is not a module
+}
+
+module A imports B, M {
+ class Y { }
+}
+
+module B imports N, M {
+ class X { }
+}
+
+module G imports A, M, A, H, B { // error: cycle in import graph
+}
+
+module H imports A, N, I {
+}
+
+module I imports J {
+}
+
+module J imports G, M {
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 3bf5ed3f..b627df75 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -151,222 +151,3 @@ class Modifies { }
}
}
-
-// ----------------- wellformed specifications ----------------------
-
-class SoWellformed {
- var xyz: int;
- var next: SoWellformed;
-
- function F(x: int): int
- { 5 / x } // error: possible division by zero
-
- function G(x: int): int
- requires 0 < x;
- { 5 / x }
-
- function H(x: int): int
- decreases 5/x; // error: possible division by zero
- { 12 }
-
- function I(x: int): int
- requires 0 < x;
- decreases 5/x;
- { 12 }
-
- method M(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- requires a.xyz == 7; // error: not always defined
- ensures c ==> d.xyz == -7; // error: not always defined
- decreases 5 / b; // error: not always defined
- {
- c := false;
- }
-
- method N(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- decreases 5 / b;
- requires a.next != null; // error: not always defined
- requires a.next.xyz == 7; // this is well-defined, given that the previous line is
- requires b < -2;
- ensures 0 <= b ==> d.xyz == -7 && !c;
- {
- c := true;
- }
-
- method O(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
- modifies a.next; // this may not be well-defined, but that's okay for modifies clauses
- {
- c := true;
- }
-
- method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
- requires next != null;
- modifies this;
- ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
-
- method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
- requires next != null;
- modifies s;
- ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
-
- method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
- requires next != null && this !in s;
- modifies s;
- ensures next.xyz < 100; // fine
-}
-
-// ---------------------- welldefinedness checks for statements -------------------
-
-class StatementTwoShoes {
- var x: int;
-
- function method F(b: int): StatementTwoShoes
- requires 0 <= b;
- {
- this
- }
-
- method M(p: StatementTwoShoes, a: int)
- modifies this, p;
- {
- p.x := a; // error: receiver may be null
- F(a).x := a; // error: LHS may not be well defined
- x := F(a-10).x; // error: RHS may not be well defined
- }
-
- method N(a: int, b: int)
- {
- assert 5 / a == 5 / a; // error: expression may not be well defined
- assume 20 / b == 5; // error: expression may not be well defined
- }
-
- method O(a: int) returns (b: int)
- {
- if (20 / a == 5) { // error: expression may not be well defined
- b := a;
- }
- }
-
- method P(a: int)
- {
- while (20 / a == 5) { // error: expression may not be well defined
- break;
- }
- }
-
- method Q(a: int, b: int)
- {
- var i := 1;
- while (i < a)
- decreases F(i), F(a), a - i; // error: component 1 may not be well defined
- {
- i := i + 1;
- }
- i := 1;
- while (i < a)
- decreases F(b), a - i; // error: component 0 may not be well defined
- {
- i := i + 1;
- }
- }
-
- method R(a: int)
- {
- var i := 0;
- while (i < 100) // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption
- invariant F(a) != null; // error: expression may not be well defined, and error: loop invariant may not hold
- decreases F(a), 100 - i; // error: component 0 not well defined
- {
- i := i + 1;
- }
- }
-
- method S(a: int)
- {
- var j := 0;
- while (20 / a == 5 && j < 100) // error: guard may not be well defined
- invariant j <= 100;
- decreases F(101 - j), 100 - j;
- {
- j := j + 1;
- }
- }
-
- method T(a: int)
- requires a != 0 && 20 / a == 5;
- {
- var k := a;
- var j := 0;
- while (20 / k == 5 && j < 100) // fine
- decreases 100 - j;
- {
- j := j + 1;
- }
- j := 0;
- while (20 / k == 5 && j < 100) // error: guard may not be well defined
- decreases 100 - j;
- {
- havoc k;
- j := j + 1;
- }
- }
-
- method U()
- {
- var i := 0;
- while (i < 100)
- invariant i <= 100;
- decreases 100 - i;
- invariant F(123 - i) == this;
- {
- i := i + 1;
- }
- i := 0;
- while (i < 100)
- decreases 100 - i;
- invariant F(if i==77 then -3 else i) == this; // error: expression may not be well defined
- {
- i := i + 1;
- if (i == 77) { i := i + 1; }
- }
- }
-
- use function G(w: int): int { 5 }
- function method H(x: int): int;
-
- method V(s: set<StatementTwoShoes>, a: int, b: int)
- modifies s;
- {
- use G(12 / b); // fine, because there are no welldefinedness checks on use statements
- foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
- {
- assume 0 <= m.x;
- assert m.x < 1000;
- use G(5 / m.x); // fine, because there are no welldefinedness checks on use statements
- m.x := m.x + 1;
- }
- foreach (m in s + {F(a)}) // error: collection expression may not be well defined
- {
- m.x := 5; // error: possible modifies clause violation
- }
- foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
- {
- m.x := H(m.x);
- }
- foreach (m in s)
- {
- m.x := 100 / m.x; // error: RhS may not be well defined
- }
- }
-
- method W(x: int)
- {
- var i := 0;
- while (i < 100)
- // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking
- invariant 5 / x != 5 / x; // error: not well-defined, and error: loop invariant does not hold initially
- decreases 100 - i;
- {
- i := i + 1;
- }
- }
-}
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy index 389c885c..42a82fe6 100644 --- a/Test/dafny0/SumOfCubes.dfy +++ b/Test/dafny0/SumOfCubes.dfy @@ -1,12 +1,12 @@ class SumOfCubes {
- class use function SumEmUp(n: int, m: int): int
+ static use function SumEmUp(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m - n;
{
if m == n then 0 else n*n*n + SumEmUp(n+1, m)
}
- class method Socu(n: int, m: int) returns (r: int)
+ static method Socu(n: int, m: int) returns (r: int)
requires 0 <= n && n <= m;
ensures r == SumEmUp(n, m);
{
@@ -16,7 +16,7 @@ class SumOfCubes { call Lemma0(n, m);
}
- class method SocuFromZero(k: int) returns (r: int)
+ static method SocuFromZero(k: int) returns (r: int)
requires 0 <= k;
ensures r == SumEmUp(0, k);
{
@@ -25,7 +25,7 @@ class SumOfCubes { call Lemma1(k);
}
- ghost class method Lemma0(n: int, m: int)
+ ghost static method Lemma0(n: int, m: int)
requires 0 <= n && n <= m;
ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);
{
@@ -42,14 +42,14 @@ class SumOfCubes { call Lemma3(0, k);
}
- class use function GSum(k: int): int
+ static use function GSum(k: int): int
requires 0 <= k;
decreases k;
{
if k == 0 then 0 else GSum(k-1) + k-1
}
- ghost class method Gauss(k: int) returns (r: int)
+ ghost static method Gauss(k: int) returns (r: int)
requires 0 <= k;
ensures r == GSum(k);
{
@@ -57,7 +57,7 @@ class SumOfCubes { call Lemma2(k);
}
- ghost class method Lemma1(k: int)
+ ghost static method Lemma1(k: int)
requires 0 <= k;
ensures SumEmUp(0, k) == GSum(k) * GSum(k);
{
@@ -73,7 +73,7 @@ class SumOfCubes { call Lemma3(0, k);
}
- ghost class method Lemma2(k: int)
+ ghost static method Lemma2(k: int)
requires 0 <= k;
ensures 2 * GSum(k) == k * (k - 1);
{
@@ -87,14 +87,14 @@ class SumOfCubes { }
}
- class use function SumEmDown(n: int, m: int): int
+ static use function SumEmDown(n: int, m: int): int
requires 0 <= n && n <= m;
decreases m;
{
if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)
}
- ghost class method Lemma3(n: int, m: int)
+ ghost static method Lemma3(n: int, m: int)
requires 0 <= n && n <= m;
ensures SumEmUp(n, m) == SumEmDown(n, m);
{
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index c1837b43..2bec0a4d 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,8 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy
+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
+ Modules0.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 3b10c560..da7e59e7 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -31,6 +31,7 @@ `(,(dafny-regexp-opt '(
"class" "datatype" "function" "frame" "ghost" "var" "method"
+ "module" "imports" "static"
"returns" "requires" "ensures" "modifies" "reads" "free"
"invariant" "decreases"
)) . font-lock-builtin-face)
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 23ea36fb..641584b6 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -7,8 +7,8 @@ \lstdefinelanguage{dafny}{
morekeywords={class,datatype,bool,int,object,set,seq,%
function,returns,
- ghost,var,
- method,in,
+ ghost,var,static,
+ method,module,imports,in,
requires,modifies,ensures,reads,decreases,free,
% expressions
match,case,false,true,null,old,fresh,this,
|