diff options
| author |  rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-21 18:38:47 +0000 |
| commit | 2fc9a47b200589fae14f698e7546553a0b31aec2 (patch) | |
| tree | ae0fd61bcd66c4f92833c33f82de518a718bfb7c | |
| parent | 9657b7042a5a55fe96bc9b7560c473876d7efa60 (diff) | |
Dafny:
* Added arrays
* Beefed up set axiomatization to know more things about set displays
* Added a simple heuristic that can infer some simple decreases clauses for loops
* Added Dafny solutions to a couple of VACID benchmarks
30 files changed, 1656 insertions, 584 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index d9ff2f63..13314e29 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -2,7 +2,11 @@ // Created 9 February 2008 by Rustan Leino.
// Converted to Boogie 2 on 28 June 2008.
// Edited sequence axioms 20 October 2009 by Alex Summers.
-// Copyright (c) 2008, Microsoft.
+// Copyright (c) 2008-2010, Microsoft.
+
+// ---------------------------------------------------------------
+// -- References -------------------------------------------------
+// ---------------------------------------------------------------
type ref;
const null: ref;
@@ -23,6 +27,11 @@ axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> function Set#UnionOne<T>(Set T, T) returns (Set T);
axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
Set#UnionOne(a,x)[o] <==> o == x || a[o]);
+axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
+ Set#UnionOne(a, x)[x]);
+axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
+ a[y] ==> Set#UnionOne(a, x)[y]);
+
function Set#Union<T>(Set T, Set T) returns (Set T);
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
@@ -178,6 +187,8 @@ axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): Datatype // note: an axiom like this for bool would not be sound
// ---------------------------------------------------------------
+// -- Encoding of type names -------------------------------------
+// ---------------------------------------------------------------
type ClassName;
const unique class.int: ClassName;
@@ -185,6 +196,7 @@ const unique class.bool: ClassName; const unique class.object: ClassName;
const unique class.set: ClassName;
const unique class.seq: ClassName;
+const unique class.array: ClassName;
function dtype(ref) returns (ClassName);
function TypeParams(ref, int) returns (ClassName);
@@ -198,6 +210,8 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } TypeTupleCdr(TypeTuple(a,b)) == b);
// ---------------------------------------------------------------
+// -- Datatypes --------------------------------------------------
+// ---------------------------------------------------------------
type DatatypeType;
@@ -207,6 +221,8 @@ function DatatypeCtorId(DatatypeType) returns (DtCtorId); function DtRank(DatatypeType) returns (int);
// ---------------------------------------------------------------
+// -- Axiom contexts ---------------------------------------------
+// ---------------------------------------------------------------
// used to make sure function axioms are not used while their consistency is being checked
const $ModuleContextHeight: int;
@@ -214,18 +230,50 @@ const $FunctionContextHeight: int; const $InMethodContext: bool;
// ---------------------------------------------------------------
+// -- Fields -----------------------------------------------------
+// ---------------------------------------------------------------
type Field alpha;
-type HeapType = <alpha>[ref,Field alpha]alpha;
-function $IsGoodHeap(HeapType) returns (bool);
-var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap);
-const unique #loc.$Heap: $token;
+type FieldCategory;
+const unique $NamedField: FieldCategory;
+const unique $IndexedField: FieldCategory;
+function FCat<T>(Field T): FieldCategory;
const unique alloc: Field bool;
+axiom FCat(alloc) == $NamedField;
+
+function IndexField(int): Field BoxType;
+axiom (forall i: int :: { IndexField(i) } FCat(IndexField(i)) == $IndexedField);
+function IndexField_Inverse<T>(Field T): int;
+axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);
function DeclType<T>(Field T) returns (ClassName);
+// ---------------------------------------------------------------
+// -- Arrays -----------------------------------------------------
+// ---------------------------------------------------------------
+
+function Array#Length(ref): int;
+axiom (forall r: ref :: 0 <= Array#Length(r));
+
+procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
+ modifies $Heap;
+ ensures $HeapSucc(old($Heap), $Heap);
+ ensures (forall i: int :: { $Heap[arr, IndexField(i)] } low <= i && i < high ==> $Heap[arr, IndexField(i)] == rhs);
+ ensures (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] } $Heap[o,f] == old($Heap)[o,f] ||
+ (o == arr && FCat(f) == $IndexedField && low <= IndexField_Inverse(f) && IndexField_Inverse(f) < high));
+
+// ---------------------------------------------------------------
+// -- The heap ---------------------------------------------------
+// ---------------------------------------------------------------
+
+type HeapType = <alpha>[ref,Field alpha]alpha;
+
+function $IsGoodHeap(HeapType) returns (bool);
+var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap);
+const unique #loc.$Heap: $token;
+
function $HeapSucc(HeapType, HeapType) returns (bool);
axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { h[r,f:=x] }
$HeapSucc(h, h[r,f:=x]));
@@ -235,6 +283,8 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) } $HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));
// ---------------------------------------------------------------
+// -- Arithmetic -------------------------------------------------
+// ---------------------------------------------------------------
// the connection between % and /
axiom (forall x:int, y:int :: {x % y} {x / y} x % y == x - x / y * y);
@@ -248,6 +298,8 @@ axiom (forall x:int, y:int :: {x % y} y < 0 ==> y < x % y && x % y <= 0); axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);
// ---------------------------------------------------------------
+// -- CEV (counterexample visualizer) ----------------------------
+// ---------------------------------------------------------------
type $token;
function $file_name_is(id:int, tok:$token) returns(bool);
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 982683b9..610cd2f3 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -218,4 +218,19 @@ namespace Dafny this.Cdr = b;
}
}
+ public class Helpers
+ {
+ public static T[] InitNewArray<T>(BigInteger size) {
+ int sz = (int)size;
+ T[] a = new T[sz];
+ BigInteger[] b = a as BigInteger[];
+ if (b != null) {
+ BigInteger z = new BigInteger(0);
+ for (int i = 0; i < sz; i++) {
+ b[i] = z;
+ }
+ }
+ return a;
+ }
+ }
}
diff --git a/Source/Dafny/Compiler.ssc b/Source/Dafny/Compiler.ssc index 155927c4..c7dc73eb 100644 --- a/Source/Dafny/Compiler.ssc +++ b/Source/Dafny/Compiler.ssc @@ -386,6 +386,9 @@ namespace Microsoft.Dafny { return "BigInteger";
} else if (type is ObjectType) {
return "object";
+ } else if (type.IsArrayType) {
+ Type elType = UserDefinedType.ArrayElementType(type);
+ return TypeName(elType) + "[]";
} else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
string s = udt.Name;
@@ -507,13 +510,54 @@ namespace Microsoft.Dafny { wr.WriteLine("return;");
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
- Indent(indent);
- TrExpr(s.Lhs);
- if (!(s.Rhs is HavocRhs)) {
- wr.Write(" = ");
- TrAssignmentRhs(s.Rhs);
+ if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
+ SeqSelectExpr sel = (SeqSelectExpr)s.Lhs;
+ // Generate the following:
+ // tmpArr = sel.Seq;
+ // tmpLow = sel.E0; // or 0 if sel.E0==null
+ // tmpHigh = sel.Eq; // or arr.Length if sel.E1==null
+ // tmpRhs = s.Rhs;
+ // for (int tmpI = tmpLow; tmpI < tmpHigh; tmpI++) {
+ // tmpArr[tmpI] = tmpRhs;
+ // }
+ string arr = "_arr" + tmpVarCount;
+ string low = "_low" + tmpVarCount;
+ string high = "_high" + tmpVarCount;
+ string rhs = "_rhs" + tmpVarCount;
+ string i = "_i" + tmpVarCount;
+ tmpVarCount++;
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Seq.Type), arr); TrExpr(sel.Seq); wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", low);
+ if (sel.E0 == null) {
+ wr.Write("0");
+ } else {
+ TrExpr(sel.E0);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("int {0} = ", high);
+ if (sel.E1 == null) {
+ wr.Write("new BigInteger(arr.Length)");
+ } else {
+ TrExpr(sel.E1);
+ }
+ wr.WriteLine(";");
+ Indent(indent); wr.Write("{0} {1} = ", TypeName((!)sel.Type), rhs); TrAssignmentRhs(s.Rhs); wr.WriteLine(";");
+ Indent(indent);
+ wr.WriteLine("for (BigInteger {0} = {1}; {0} < {2}; {0}++) {{", i, low, high);
+ Indent(indent + IndentAmount);
+ wr.WriteLine("{0}[(int)({1})] = {2};", arr, i, rhs);
+ Indent(indent);
+ wr.WriteLine(";");
+
+ } else {
+ Indent(indent);
+ TrExpr(s.Lhs);
+ if (!(s.Rhs is HavocRhs)) {
+ wr.Write(" = ");
+ TrAssignmentRhs(s.Rhs);
+ }
+ wr.WriteLine(";");
}
- wr.WriteLine(";");
} else if (stmt is VarDecl) {
TrVarDecl((VarDecl)stmt, true, indent);
@@ -686,7 +730,21 @@ namespace Microsoft.Dafny { } else {
TypeRhs tp = (TypeRhs)rhs;
- wr.Write("new {0}()", TypeName(tp.Type));
+ if (tp.ArraySize == null) {
+ wr.Write("new {0}()", TypeName(tp.EType));
+ } else {
+ if (tp.EType is IntType || tp.EType.IsTypeParameter) {
+ // Because the default constructor for BigInteger does not generate a valid BigInteger, we have
+ // to excplicitly initialize the elements of an integer array. This is all done in a helper routine.
+ wr.Write("Dafny.Helpers.InitNewArray<{0}>(", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write(")");
+ } else {
+ wr.Write("new {0}[(int)", TypeName(tp.EType));
+ TrExpr(tp.ArraySize);
+ wr.Write("]");
+ }
+ }
}
}
@@ -827,9 +885,15 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
TrParenExpr(e.Seq);
- if (e.SelectOne) {
- assert e.E0 != null;
- assert e.E1 == null;
+ assert e.Seq.Type != null;
+ if (e.Seq.Type.IsArrayType) {
+ assert e.SelectOne;
+ assert e.E0 != null && e.E1 == null;
+ wr.Write("[(int)");
+ TrParenExpr(e.E0);
+ wr.Write("]");
+ } else if (e.SelectOne) {
+ assert e.E0 != null && e.E1 == null;
TrParenExpr(".Select", e.E0);
} else {
if (e.E1 != null) {
@@ -902,8 +966,14 @@ namespace Microsoft.Dafny { TrParenExpr(e.E);
break;
case UnaryExpr.Opcode.SeqLength:
- TrParenExpr(e.E);
- wr.Write(".Length");
+ if (((!)e.E.Type).IsArrayType) {
+ wr.Write("new BigInteger(");
+ TrParenExpr(e.E);
+ wr.Write(".Length)");
+ } else {
+ TrParenExpr(e.E);
+ wr.Write(".Length");
+ }
break;
default:
assert false; // unexpected unary expression
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 9d232294..6b46aa4f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -397,6 +397,12 @@ ReferenceType<out Token! tok, out Type! ty> List<Type!>! gt;
.)
( "object" (. tok = token; ty = new ObjectType(); .)
+ | "array" (. tok = token; gt = new List<Type!>(); .)
+ GenericInstantiation<gt> (. if (gt.Count != 1) {
+ SemErr("array type expects exactly one type argument");
+ }
+ ty = UserDefinedType.ArrayType(tok, gt[0]);
+ .)
| Ident<out tok> (. gt = new List<Type!>(); .)
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
@@ -590,22 +596,26 @@ AssignStmt<out Statement! s> .)
LhsExpr<out lhs>
":=" (. x = token; .)
- AssignRhs<out rhs, out ty> (. if (rhs != null) {
+ AssignRhs<out rhs, out ty> (. if (ty == null) {
+ assert rhs != null;
s = new AssignStmt(x, lhs, rhs);
- } else {
- assert ty != null;
+ } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
+ } else {
+ s = new AssignStmt(x, lhs, ty, rhs);
}
.)
";"
.
AssignRhs<out Expression e, out Type ty>
-/* ensures e == null <==> ty == null; */
+/* ensures e != null || ty != null; */
= (. Token! x; Expression! ee; Type! tt;
e = null; ty = null;
.)
- ( "new" ReferenceType<out x, out tt> (. ty = tt; .)
+ ( "new" TypeAndToken<out x, out tt> (. ty = tt; .)
+ [ "[" Expression<out ee> "]" (. e = ee; .)
+ ]
| Expression<out ee> (. e = ee; .)
) (. if (e == null && ty == null) { e = dummyExpr; } .)
.
@@ -642,11 +652,14 @@ IdentTypeRhs<out VarDecl! d, bool isGhost> [ ":="
AssignRhs<out rhs, out newType>
]
- (. if (rhs != null) {
- assert newType == null;
+ (. if (newType == null && rhs != null) {
optionalRhs = new ExprRhs(rhs);
} else if (newType != null) {
- optionalRhs = new TypeRhs(newType);
+ if (rhs == null) {
+ optionalRhs = new TypeRhs(newType);
+ } else {
+ optionalRhs = new TypeRhs(newType, rhs);
+ }
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
}
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc index 55e76d30..cea08862 100644 --- a/Source/Dafny/DafnyAst.ssc +++ b/Source/Dafny/DafnyAst.ssc @@ -68,6 +68,12 @@ namespace Microsoft.Dafny }
}
}
+ public bool IsArrayType {
+ get {
+ UserDefinedType udt = UserDefinedType.DenotesClass(this);
+ return udt != null && ((ClassDecl!)udt.ResolvedClass).Name == "array"; // the cast to non-null is guaranteed by postcondition of DenotesClass
+ }
+ }
public bool IsDatatype {
get {
return AsDatatype != null;
@@ -140,7 +146,7 @@ namespace Microsoft.Dafny return "seq<" + Arg + ">";
}
}
-
+
public class UserDefinedType : Type {
public readonly Token! tok;
public readonly string! Name;
@@ -148,6 +154,22 @@ namespace Microsoft.Dafny public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
+
+ public static UserDefinedType! ArrayType(Token! tok, Type! arg) {
+ List<Type!> typeArgs = new List<Type!>();
+ typeArgs.Add(arg);
+ UserDefinedType udt = new UserDefinedType(tok, "array", typeArgs);
+ udt.ResolvedClass = arrayTypeDecl;
+ return udt;
+ }
+ static TopLevelDecl! arrayTypeDecl;
+ static UserDefinedType() {
+ List<TypeParameter!> typeArgs = new List<TypeParameter!>();
+ typeArgs.Add(new TypeParameter(Token.NoToken, "arg"));
+ ModuleDecl systemModule = new ModuleDecl(Token.NoToken, "_System", new List<string!>(), null);
+ arrayTypeDecl = new ClassDecl(Token.NoToken, "array", systemModule, typeArgs, new List<MemberDecl!>(), null);
+ }
+
public UserDefinedType(Token! tok, string! name, [Captured] List<Type!>! typeArgs) {
this.tok = tok;
@@ -201,6 +223,19 @@ namespace Microsoft.Dafny }
}
+ /// <summary>
+ /// If type denotes a resolved class type, then return that class type.
+ /// Otherwise, return null.
+ /// </summary>
+ public static Type! ArrayElementType(Type! type)
+ requires type.IsArrayType;
+ {
+ UserDefinedType udt = DenotesClass(type);
+ assert udt != null;
+ assert udt.TypeArgs.Count == 1; // holds true of all array types
+ return udt.TypeArgs[0];
+ }
+
[Pure] public override string! ToString() {
string s = Name;
if (TypeArgs.Count != 0) {
@@ -253,23 +288,23 @@ namespace Microsoft.Dafny }
/// <summary>
- /// This proxy stands for object or any class type.
+ /// This proxy stands for object or any class/array type.
/// </summary>
public class ObjectTypeProxy : RestrictedTypeProxy {
public override int OrderID { get { return 0; } }
}
/// <summary>
- /// This proxy stands for object or any class type or a set or sequence of object or a class type.
+ /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.
/// </summary>
public class ObjectsTypeProxy : RestrictedTypeProxy {
public override int OrderID { get { return 1; } }
}
/// <summary>
- /// This proxy stands for either:
+ /// This proxy stands for:
/// set(Arg) or seq(Arg)
- /// </summary>
+ /// </summary>
public class CollectionTypeProxy : RestrictedTypeProxy {
public readonly Type! Arg;
public CollectionTypeProxy(Type! arg) {
@@ -293,6 +328,18 @@ namespace Microsoft.Dafny public override int OrderID { get { return 3; } }
}
+ /// <summary>
+ /// This proxy stands for:
+ /// seq(Arg) or array(Arg)
+ /// </summary>
+ public class IndexableTypeProxy : RestrictedTypeProxy {
+ public readonly Type! Arg;
+ public IndexableTypeProxy(Type! arg) {
+ Arg = arg;
+ }
+ public override int OrderID { get { return 4; } }
+ }
+
// ------------------------------------------------------------------------------------------------------
public abstract class Declaration {
@@ -708,9 +755,14 @@ namespace Microsoft.Dafny }
public class TypeRhs : DeterminedAssignmentRhs {
- public readonly Type! Type;
+ public readonly Type! EType;
+ public readonly Expression ArraySize;
public TypeRhs(Type! type) {
- Type = type;
+ EType = type;
+ }
+ public TypeRhs(Type! type, Expression! arraySize) {
+ EType = type;
+ ArraySize = arraySize;
}
}
@@ -730,6 +782,11 @@ namespace Microsoft.Dafny this.Rhs = new TypeRhs(type);
base(tok);
}
+ public AssignStmt(Token! tok, Expression! lhs, Type! type, Expression! arraySize) { // array alloc statement
+ this.Lhs = lhs;
+ this.Rhs = new TypeRhs(type, arraySize);
+ base(tok);
+ }
public AssignStmt(Token! tok, Expression! lhs) { // havoc
this.Lhs = lhs;
this.Rhs = new HavocRhs();
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index 7b28ec2c..2499821c 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 = 99;
+ const int maxT = 100;
const bool T = true;
const bool x = false;
@@ -280,13 +280,13 @@ public static int Parse (List<ModuleDecl!>! modules) { }
if (t.kind == 14) {
FieldDecl(mmod, mm);
- } else if (t.kind == 33) {
+ } else if (t.kind == 34) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (t.kind == 19) {
MethodDecl(mmod, out m);
mm.Add(m);
- } else Error(100);
+ } else Error(101);
}
static void GenericParameters(List<TypeParameter!>! typeArgs) {
@@ -335,7 +335,7 @@ public static int Parse (List<ModuleDecl!>! modules) { Expression! bb; Expression body = null;
bool isFunctionMethod = false;
- Expect(33);
+ Expect(34);
if (t.kind == 19) {
Get();
isFunctionMethod = true;
@@ -355,16 +355,16 @@ public static int Parse (List<ModuleDecl!>! modules) { Type(out returnType);
if (t.kind == 13) {
Get();
- while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
} else if (StartOf(3)) {
- while (t.kind == 23 || t.kind == 25 || t.kind == 34) {
+ while (t.kind == 23 || t.kind == 25 || t.kind == 35) {
FunctionSpec(reqs, reads, decreases);
}
FunctionBody(out bb);
body = bb;
- } else Error(101);
+ } else Error(102);
parseVarScope.PopMarker();
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, decreases, body, attrs);
@@ -409,7 +409,7 @@ public static int Parse (List<ModuleDecl!>! modules) { }
BlockStmt(out bb);
body = (BlockStmt)bb;
- } else Error(102);
+ } else Error(103);
parseVarScope.PopMarker();
m = new Method(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -539,9 +539,9 @@ public static int Parse (List<ModuleDecl!>! modules) { }
ty = new SeqType(gt[0]);
- } else if (t.kind == 1 || t.kind == 32) {
+ } else if (t.kind == 1 || t.kind == 32 || t.kind == 33) {
ReferenceType(out tok, out ty);
- } else Error(103);
+ } else Error(104);
}
static void Formals(bool incoming, bool allowGhosts, List<Formal!>! formals) {
@@ -590,12 +590,12 @@ List<Expression!>! decreases) { Expression(out e);
Expect(13);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else Error(104);
+ } else Error(105);
} else if (t.kind == 25) {
Get();
Expressions(decreases);
Expect(13);
- } else Error(105);
+ } else Error(106);
}
static void BlockStmt(out Statement! block) {
@@ -617,7 +617,7 @@ List<Expression!>! decreases) { static void FrameExpression(out FrameExpression! fe) {
Expression! e; Token! id; string fieldName = null;
Expression(out e);
- if (t.kind == 36) {
+ if (t.kind == 37) {
Get();
Ident(out id);
fieldName = id.val;
@@ -629,18 +629,18 @@ List<Expression!>! decreases) { Token! x; Expression! e0; Expression! e1 = dummyExpr;
e = dummyExpr;
- if (t.kind == 46) {
+ if (t.kind == 49) {
Get();
x = token;
Expression(out e);
- Expect(58);
+ Expect(61);
Expression(out e0);
- Expect(47);
+ Expect(50);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
} else if (StartOf(9)) {
EquivExpression(out e);
- } else Error(106);
+ } else Error(107);
}
static void Expressions(List<Expression!>! args) {
@@ -674,6 +674,15 @@ List<Expression!>! decreases) { if (t.kind == 32) {
Get();
tok = token; ty = new ObjectType();
+ } else if (t.kind == 33) {
+ Get();
+ tok = token; gt = new List<Type!>();
+ GenericInstantiation(gt);
+ if (gt.Count != 1) {
+ SemErr("array type expects exactly one type argument");
+ }
+ ty = UserDefinedType.ArrayType(tok, gt[0]);
+
} else if (t.kind == 1) {
Ident(out tok);
gt = new List<Type!>();
@@ -681,7 +690,7 @@ List<Expression!>! decreases) { GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else Error(107);
+ } else Error(108);
}
static void FunctionSpec(List<Expression!>! reqs, List<FrameExpression!>! reads, List<Expression!>! decreases) {
@@ -691,7 +700,7 @@ List<Expression!>! decreases) { Expression(out e);
Expect(13);
reqs.Add(e);
- } else if (t.kind == 34) {
+ } else if (t.kind == 35) {
Get();
if (StartOf(10)) {
PossiblyWildFrameExpression(out fe);
@@ -707,48 +716,48 @@ List<Expression!>! decreases) { Get();
Expressions(decreases);
Expect(13);
- } else Error(108);
+ } else Error(109);
}
static void FunctionBody(out Expression! e) {
e = dummyExpr;
Expect(6);
- if (t.kind == 37) {
+ if (t.kind == 38) {
MatchExpression(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(109);
+ } else Error(110);
Expect(7);
}
static void PossiblyWildFrameExpression(out FrameExpression! fe) {
fe = dummyFrameExpr;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
fe = new FrameExpression(new WildcardExpr(token), null);
} else if (StartOf(7)) {
FrameExpression(out fe);
- } else Error(110);
+ } else Error(111);
}
static void PossiblyWildExpression(out Expression! e) {
e = dummyExpr;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
e = new WildcardExpr(token);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(111);
+ } else Error(112);
}
static void MatchExpression(out Expression! e) {
Token! x; MatchCaseExpr! c;
List<MatchCaseExpr!> cases = new List<MatchCaseExpr!>();
- Expect(37);
+ Expect(38);
x = token;
Expression(out e);
- while (t.kind == 38) {
+ while (t.kind == 39) {
CaseExpression(out c);
cases.Add(c);
}
@@ -760,7 +769,7 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
Expression! body;
- Expect(38);
+ Expect(39);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -776,7 +785,7 @@ List<Expression!>! decreases) { }
Expect(27);
}
- Expect(39);
+ Expect(40);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
parseVarScope.PopMarker();
@@ -793,7 +802,7 @@ List<Expression!>! decreases) { ss.Add(s);
} else if (t.kind == 9 || t.kind == 14) {
VarDeclStmts(ss);
- } else Error(112);
+ } else Error(113);
}
static void OneStmt(out Statement! s) {
@@ -801,51 +810,51 @@ List<Expression!>! decreases) { s = dummyStmt; /* to please the compiler */
switch (t.kind) {
- case 54: {
+ case 57: {
AssertStmt(out s);
break;
}
- case 55: {
+ case 58: {
AssumeStmt(out s);
break;
}
- case 56: {
+ case 59: {
UseStmt(out s);
break;
}
- case 57: {
+ case 60: {
PrintStmt(out s);
break;
}
- case 1: case 26: case 91: case 92: {
+ case 1: case 26: case 92: case 93: {
AssignStmt(out s);
break;
}
- case 45: {
+ case 48: {
HavocStmt(out s);
break;
}
- case 50: {
+ case 53: {
CallStmt(out s);
break;
}
- case 46: {
+ case 49: {
IfStmt(out s);
break;
}
- case 48: {
+ case 51: {
WhileStmt(out s);
break;
}
- case 37: {
+ case 38: {
MatchStmt(out s);
break;
}
- case 51: {
+ case 54: {
ForeachStmt(out s);
break;
}
- case 40: {
+ case 41: {
Get();
x = token;
Ident(out id);
@@ -853,7 +862,7 @@ List<Expression!>! decreases) { s = new LabelStmt(x, id.val);
break;
}
- case 41: {
+ case 42: {
Get();
x = token;
if (t.kind == 1) {
@@ -864,14 +873,14 @@ List<Expression!>! decreases) { s = new BreakStmt(x, label);
break;
}
- case 42: {
+ case 43: {
Get();
x = token;
Expect(13);
s = new ReturnStmt(x);
break;
}
- default: Error(113); break;
+ default: Error(114); break;
}
}
@@ -894,7 +903,7 @@ List<Expression!>! decreases) { static void AssertStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(54);
+ Expect(57);
x = token;
Expression(out e);
Expect(13);
@@ -903,7 +912,7 @@ List<Expression!>! decreases) { static void AssumeStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(55);
+ Expect(58);
x = token;
Expression(out e);
Expect(13);
@@ -912,7 +921,7 @@ List<Expression!>! decreases) { static void UseStmt(out Statement! s) {
Token! x; Expression! e;
- Expect(56);
+ Expect(59);
x = token;
Expression(out e);
Expect(13);
@@ -923,7 +932,7 @@ List<Expression!>! decreases) { Token! x; Attributes.Argument! arg;
List<Attributes.Argument!> args = new List<Attributes.Argument!>();
- Expect(57);
+ Expect(60);
x = token;
AttributeArg(out arg);
args.Add(arg);
@@ -944,14 +953,16 @@ List<Expression!>! decreases) { s = dummyStmt;
LhsExpr(out lhs);
- Expect(43);
+ Expect(44);
x = token;
AssignRhs(out rhs, out ty);
- if (rhs != null) {
+ if (ty == null) {
+ assert rhs != null;
s = new AssignStmt(x, lhs, rhs);
- } else {
- assert ty != null;
+ } else if (rhs == null) {
s = new AssignStmt(x, lhs, ty);
+ } else {
+ s = new AssignStmt(x, lhs, ty, rhs);
}
Expect(13);
@@ -959,7 +970,7 @@ List<Expression!>! decreases) { static void HavocStmt(out Statement! s) {
Token! x; Expression! lhs;
- Expect(45);
+ Expect(48);
x = token;
LhsExpr(out lhs);
Expect(13);
@@ -972,10 +983,10 @@ List<Expression!>! decreases) { List<IdentifierExpr!> lhs = new List<IdentifierExpr!>();
List<AutoVarDecl!> newVars = new List<AutoVarDecl!>();
- Expect(50);
+ Expect(53);
x = token;
CallStmtSubExpr(out e);
- if (t.kind == 15 || t.kind == 43) {
+ if (t.kind == 15 || t.kind == 44) {
if (t.kind == 15) {
Get();
e = ConvertToLocal(e);
@@ -994,7 +1005,7 @@ List<Expression!>! decreases) { Ident(out id);
RecordCallLhs(new IdentifierExpr(id, id.val), lhs, newVars);
}
- Expect(43);
+ Expect(44);
CallStmtSubExpr(out e);
} else {
Get();
@@ -1028,19 +1039,19 @@ List<Expression!>! decreases) { Statement! s;
Statement els = null;
- Expect(46);
+ Expect(49);
x = token;
Guard(out guard);
BlockStmt(out thn);
- if (t.kind == 47) {
+ if (t.kind == 50) {
Get();
- if (t.kind == 46) {
+ if (t.kind == 49) {
IfStmt(out s);
els = s;
} else if (t.kind == 6) {
BlockStmt(out s);
els = s;
- } else Error(114);
+ } else Error(115);
}
ifStmt = new IfStmt(x, guard, thn, els);
}
@@ -1053,18 +1064,18 @@ List<Expression!>! decreases) { List<Expression!> decreases = new List<Expression!>();
Statement! body;
- Expect(48);
+ Expect(51);
x = token;
Guard(out guard);
assume guard == null || Owner.None(guard);
- while (t.kind == 22 || t.kind == 25 || t.kind == 49) {
- if (t.kind == 22 || t.kind == 49) {
+ while (t.kind == 22 || t.kind == 25 || t.kind == 52) {
+ if (t.kind == 22 || t.kind == 52) {
isFree = false;
if (t.kind == 22) {
Get();
isFree = true;
}
- Expect(49);
+ Expect(52);
Expression(out e);
invariants.Add(new MaybeFreeExpression(e, isFree));
Expect(13);
@@ -1087,11 +1098,11 @@ List<Expression!>! decreases) { static void MatchStmt(out Statement! s) {
Token x; Expression! e; MatchCaseStmt! c;
List<MatchCaseStmt!> cases = new List<MatchCaseStmt!>();
- Expect(37);
+ Expect(38);
x = token;
Expression(out e);
Expect(6);
- while (t.kind == 38) {
+ while (t.kind == 39) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1108,7 +1119,7 @@ List<Expression!>! decreases) { AssignStmt bodyAssign = null;
parseVarScope.PushMarker();
- Expect(51);
+ Expect(54);
x = token;
range = new LiteralExpr(x, true);
ty = new InferredTypeProxy();
@@ -1119,20 +1130,20 @@ List<Expression!>! decreases) { Get();
Type(out ty);
}
- Expect(52);
+ Expect(55);
Expression(out collection);
parseVarScope.Push(boundVar.val, boundVar.val);
- if (t.kind == 53) {
+ if (t.kind == 56) {
Get();
Expression(out range);
}
Expect(27);
Expect(6);
- while (t.kind == 54 || t.kind == 55 || t.kind == 56) {
- if (t.kind == 54) {
+ while (t.kind == 57 || t.kind == 58 || t.kind == 59) {
+ if (t.kind == 57) {
AssertStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else if (t.kind == 55) {
+ } else if (t.kind == 58) {
AssumeStmt(out s);
if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
} else {
@@ -1143,10 +1154,10 @@ List<Expression!>! decreases) { if (StartOf(12)) {
AssignStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else if (t.kind == 45) {
+ } else if (t.kind == 48) {
HavocStmt(out s);
if (s is AssignStmt) { bodyAssign = (AssignStmt)s; }
- } else Error(115);
+ } else Error(116);
Expect(7);
if (bodyAssign != null) {
s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
@@ -1165,14 +1176,20 @@ List<Expression!>! decreases) { Token! x; Expression! ee; Type! tt;
e = null; ty = null;
- if (t.kind == 44) {
+ if (t.kind == 45) {
Get();
- ReferenceType(out x, out tt);
+ TypeAndToken(out x, out tt);
ty = tt;
+ if (t.kind == 46) {
+ Get();
+ Expression(out ee);
+ Expect(47);
+ e = ee;
+ }
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(116);
+ } else Error(117);
if (e == null && ty == null) { e = dummyExpr; }
}
@@ -1180,10 +1197,10 @@ List<Expression!>! decreases) { Token! id; e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
+ } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
ObjectExpression(out e);
- } else Error(117);
- while (t.kind == 86 || t.kind == 88) {
+ } else Error(118);
+ while (t.kind == 46 || t.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
@@ -1199,15 +1216,18 @@ List<Expression!>! decreases) { Type(out ty);
optionalType = ty;
}
- if (t.kind == 43) {
+ if (t.kind == 44) {
Get();
AssignRhs(out rhs, out newType);
}
- if (rhs != null) {
- assert newType == null;
+ if (newType == null && rhs != null) {
optionalRhs = new ExprRhs(rhs);
} else if (newType != null) {
- optionalRhs = new TypeRhs(newType);
+ if (rhs == null) {
+ optionalRhs = new TypeRhs(newType);
+ } else {
+ optionalRhs = new TypeRhs(newType, rhs);
+ }
} else if (optionalType == null) {
optionalType = new InferredTypeProxy();
}
@@ -1218,13 +1238,13 @@ List<Expression!>! decreases) { static void Guard(out Expression e) {
Expression! ee; e = null;
Expect(26);
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
e = null;
} else if (StartOf(7)) {
Expression(out ee);
e = ee;
- } else Error(118);
+ } else Error(119);
Expect(27);
}
@@ -1233,7 +1253,7 @@ List<Expression!>! decreases) { List<BoundVar!> arguments = new List<BoundVar!>();
List<Statement!> body = new List<Statement!>();
- Expect(38);
+ Expect(39);
x = token; parseVarScope.PushMarker();
Ident(out id);
if (t.kind == 26) {
@@ -1249,7 +1269,7 @@ List<Expression!>! decreases) { }
Expect(27);
}
- Expect(39);
+ Expect(40);
parseVarScope.PushMarker();
while (StartOf(8)) {
Stmt(body);
@@ -1263,11 +1283,11 @@ List<Expression!>! decreases) { e = dummyExpr;
if (t.kind == 1) {
IdentOrFuncExpression(out e);
- } else if (t.kind == 26 || t.kind == 91 || t.kind == 92) {
+ } else if (t.kind == 26 || t.kind == 92 || t.kind == 93) {
ObjectExpression(out e);
SelectOrCallSuffix(ref e);
- } else Error(119);
- while (t.kind == 86 || t.kind == 88) {
+ } else Error(120);
+ while (t.kind == 46 || t.kind == 89) {
SelectOrCallSuffix(ref e);
}
}
@@ -1280,13 +1300,13 @@ List<Expression!>! decreases) { } else if (StartOf(7)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else Error(120);
+ } else Error(121);
}
static void EquivExpression(out Expression! e0) {
Token! x; Expression! e1;
ImpliesExpression(out e0);
- while (t.kind == 59 || t.kind == 60) {
+ while (t.kind == 62 || t.kind == 63) {
EquivOp();
x = token;
ImpliesExpression(out e1);
@@ -1297,7 +1317,7 @@ List<Expression!>! decreases) { static void ImpliesExpression(out Expression! e0) {
Token! x; Expression! e1;
LogicalExpression(out e0);
- if (t.kind == 61 || t.kind == 62) {
+ if (t.kind == 64 || t.kind == 65) {
ImpliesOp();
x = token;
ImpliesExpression(out e1);
@@ -1306,23 +1326,23 @@ List<Expression!>! decreases) { }
static void EquivOp() {
- if (t.kind == 59) {
+ if (t.kind == 62) {
Get();
- } else if (t.kind == 60) {
+ } else if (t.kind == 63) {
Get();
- } else Error(121);
+ } else Error(122);
}
static void LogicalExpression(out Expression! e0) {
Token! x; Expression! e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (t.kind == 63 || t.kind == 64) {
+ if (t.kind == 66 || t.kind == 67) {
AndOp();
x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (t.kind == 63 || t.kind == 64) {
+ while (t.kind == 66 || t.kind == 67) {
AndOp();
x = token;
RelationalExpression(out e1);
@@ -1333,7 +1353,7 @@ List<Expression!>! decreases) { x = token;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (t.kind == 65 || t.kind == 66) {
+ while (t.kind == 68 || t.kind == 69) {
OrOp();
x = token;
RelationalExpression(out e1);
@@ -1344,11 +1364,11 @@ List<Expression!>! decreases) { }
static void ImpliesOp() {
- if (t.kind == 61) {
+ if (t.kind == 64) {
Get();
- } else if (t.kind == 62) {
+ } else if (t.kind == 65) {
Get();
- } else Error(122);
+ } else Error(123);
}
static void RelationalExpression(out Expression! e0) {
@@ -1362,25 +1382,25 @@ List<Expression!>! decreases) { }
static void AndOp() {
- if (t.kind == 63) {
+ if (t.kind == 66) {
Get();
- } else if (t.kind == 64) {
+ } else if (t.kind == 67) {
Get();
- } else Error(123);
+ } else Error(124);
}
static void OrOp() {
- if (t.kind == 65) {
+ if (t.kind == 68) {
Get();
- } else if (t.kind == 66) {
+ } else if (t.kind == 69) {
Get();
- } else Error(124);
+ } else Error(125);
}
static void Term(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (t.kind == 76 || t.kind == 77) {
+ while (t.kind == 79 || t.kind == 80) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1390,7 +1410,7 @@ 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 67: {
+ case 70: {
Get();
x = token; op = BinaryExpr.Opcode.Eq;
break;
@@ -1405,59 +1425,59 @@ List<Expression!>! decreases) { x = token; op = BinaryExpr.Opcode.Gt;
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;
}
- case 70: {
+ case 73: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 71: {
+ case 74: {
Get();
x = token; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 52: {
+ case 55: {
Get();
x = token; op = BinaryExpr.Opcode.In;
break;
}
- case 72: {
+ case 75: {
Get();
x = token; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 73: {
+ case 76: {
Get();
x = token; op = BinaryExpr.Opcode.Neq;
break;
}
- case 74: {
+ case 77: {
Get();
x = token; op = BinaryExpr.Opcode.Le;
break;
}
- case 75: {
+ case 78: {
Get();
x = token; op = BinaryExpr.Opcode.Ge;
break;
}
- default: Error(125); break;
+ default: Error(126); break;
}
}
static void Factor(out Expression! e0) {
Token! x; Expression! e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (t.kind == 35 || t.kind == 78 || t.kind == 79) {
+ while (t.kind == 36 || t.kind == 81 || t.kind == 82) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1466,23 +1486,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 == 76) {
+ if (t.kind == 79) {
Get();
x = token; op = BinaryExpr.Opcode.Add;
- } else if (t.kind == 77) {
+ } else if (t.kind == 80) {
Get();
x = token; op = BinaryExpr.Opcode.Sub;
- } else Error(126);
+ } else Error(127);
}
static void UnaryExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 77) {
+ if (t.kind == 80) {
Get();
x = token;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
- } else if (t.kind == 80 || t.kind == 81) {
+ } else if (t.kind == 83 || t.kind == 84) {
NegOp();
x = token;
UnaryExpression(out e);
@@ -1491,29 +1511,29 @@ List<Expression!>! decreases) { SelectExpression(out e);
} else if (StartOf(15)) {
ConstAtomExpression(out e);
- } else Error(127);
+ } else Error(128);
}
static void MulOp(out Token! x, out BinaryExpr.Opcode op) {
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (t.kind == 35) {
+ if (t.kind == 36) {
Get();
x = token; op = BinaryExpr.Opcode.Mul;
- } else if (t.kind == 78) {
+ } else if (t.kind == 81) {
Get();
x = token; op = BinaryExpr.Opcode.Div;
- } else if (t.kind == 79) {
+ } else if (t.kind == 82) {
Get();
x = token; op = BinaryExpr.Opcode.Mod;
- } else Error(128);
+ } else Error(129);
}
static void NegOp() {
- if (t.kind == 80) {
+ if (t.kind == 83) {
Get();
- } else if (t.kind == 81) {
+ } else if (t.kind == 84) {
Get();
- } else Error(129);
+ } else Error(130);
}
static void ConstAtomExpression(out Expression! e) {
@@ -1521,17 +1541,17 @@ List<Expression!>! decreases) { e = dummyExpr;
switch (t.kind) {
- case 82: {
+ case 85: {
Get();
e = new LiteralExpr(token, false);
break;
}
- case 83: {
+ case 86: {
Get();
e = new LiteralExpr(token, true);
break;
}
- case 84: {
+ case 87: {
Get();
e = new LiteralExpr(token);
break;
@@ -1541,11 +1561,11 @@ List<Expression!>! decreases) { e = new LiteralExpr(token, n);
break;
}
- case 85: {
+ case 88: {
Get();
x = token;
Ident(out dtName);
- Expect(86);
+ Expect(89);
Ident(out id);
elements = new List<Expression!>();
if (t.kind == 26) {
@@ -1558,7 +1578,7 @@ List<Expression!>! decreases) { e = new DatatypeValue(token, dtName.val, id.val, elements);
break;
}
- case 87: {
+ case 90: {
Get();
x = token;
Expect(26);
@@ -1567,12 +1587,12 @@ List<Expression!>! decreases) { e = new FreshExpr(x, e);
break;
}
- case 53: {
+ case 56: {
Get();
x = token;
Expression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e);
- Expect(53);
+ Expect(56);
break;
}
case 6: {
@@ -1585,17 +1605,17 @@ List<Expression!>! decreases) { Expect(7);
break;
}
- case 88: {
+ case 46: {
Get();
x = token; elements = new List<Expression!>();
if (StartOf(7)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(89);
+ Expect(47);
break;
}
- default: Error(130); break;
+ default: Error(131); break;
}
}
@@ -1634,10 +1654,10 @@ List<Expression!>! decreases) { static void ObjectExpression(out Expression! e) {
Token! x; e = dummyExpr;
- if (t.kind == 91) {
+ if (t.kind == 92) {
Get();
e = new ThisExpr(token);
- } else if (t.kind == 92) {
+ } else if (t.kind == 93) {
Get();
x = token;
Expect(26);
@@ -1650,9 +1670,9 @@ List<Expression!>! decreases) { QuantifierGuts(out e);
} else if (StartOf(7)) {
Expression(out e);
- } else Error(131);
+ } else Error(132);
Expect(27);
- } else Error(132);
+ } else Error(133);
}
static void SelectOrCallSuffix(ref Expression! e) {
@@ -1660,7 +1680,7 @@ List<Expression!>! decreases) { Expression e0 = null; Expression e1 = null; Expression! ee; bool anyDots = false;
bool func = false;
- if (t.kind == 86) {
+ if (t.kind == 89) {
Get();
Ident(out id);
if (t.kind == 26) {
@@ -1673,14 +1693,14 @@ List<Expression!>! decreases) { e = new FunctionCallExpr(id, id.val, e, args);
}
if (!func) { e = new FieldSelectExpr(id, e, id.val); }
- } else if (t.kind == 88) {
+ } else if (t.kind == 46) {
Get();
x = token;
if (StartOf(7)) {
Expression(out ee);
e0 = ee;
- if (t.kind == 43 || t.kind == 90) {
- if (t.kind == 90) {
+ if (t.kind == 44 || t.kind == 91) {
+ if (t.kind == 91) {
Get();
anyDots = true;
if (StartOf(7)) {
@@ -1693,11 +1713,11 @@ List<Expression!>! decreases) { e1 = ee;
}
}
- } else if (t.kind == 90) {
+ } else if (t.kind == 91) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else Error(133);
+ } else Error(134);
if (!anyDots && e0 == null) {
/* a parsing error occurred */
e0 = dummyExpr;
@@ -1714,8 +1734,8 @@ List<Expression!>! decreases) { e = new SeqUpdateExpr(x, e, e0, e1);
}
- Expect(89);
- } else Error(134);
+ Expect(47);
+ } else Error(135);
}
static void QuantifierGuts(out Expression! q) {
@@ -1728,13 +1748,13 @@ List<Expression!>! decreases) { Triggers trigs = null;
Expression! body;
- if (t.kind == 93 || t.kind == 94) {
+ if (t.kind == 94 || t.kind == 95) {
Forall();
x = token; univ = true;
- } else if (t.kind == 95 || t.kind == 96) {
+ } else if (t.kind == 96 || t.kind == 97) {
Exists();
x = token;
- } else Error(135);
+ } else Error(136);
parseVarScope.PushMarker();
IdentTypeOptional(out bv);
bvars.Add(bv); parseVarScope.Push(bv.Name, bv.Name);
@@ -1758,19 +1778,19 @@ List<Expression!>! decreases) { }
static void Forall() {
- if (t.kind == 93) {
+ if (t.kind == 94) {
Get();
- } else if (t.kind == 94) {
+ } else if (t.kind == 95) {
Get();
- } else Error(136);
+ } else Error(137);
}
static void Exists() {
- if (t.kind == 95) {
+ if (t.kind == 96) {
Get();
- } else if (t.kind == 96) {
+ } else if (t.kind == 97) {
Get();
- } else Error(137);
+ } else Error(138);
}
static void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -1783,16 +1803,16 @@ List<Expression!>! decreases) { es = new List<Expression!>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else Error(138);
+ } else Error(139);
Expect(7);
}
static void QSep() {
- if (t.kind == 97) {
+ if (t.kind == 98) {
Get();
- } else if (t.kind == 98) {
+ } else if (t.kind == 99) {
Get();
- } else Error(139);
+ } else Error(140);
}
static void AttributeBody(ref Attributes attrs) {
@@ -1864,113 +1884,114 @@ List<Expression!>! decreases) { 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 = "` expected"; break;
- case 37: s = "match expected"; break;
- case 38: s = "case expected"; break;
- case 39: s = "=> expected"; break;
- case 40: s = "label expected"; break;
- case 41: s = "break expected"; break;
- case 42: s = "return expected"; break;
- case 43: s = ":= expected"; break;
- case 44: s = "new expected"; break;
- case 45: s = "havoc expected"; break;
- case 46: s = "if expected"; break;
- case 47: s = "else expected"; break;
- case 48: s = "while expected"; break;
- case 49: s = "invariant expected"; break;
- case 50: s = "call expected"; break;
- case 51: s = "foreach expected"; break;
- case 52: s = "in expected"; break;
- case 53: s = "| expected"; break;
- case 54: s = "assert expected"; break;
- case 55: s = "assume expected"; break;
- case 56: s = "use expected"; break;
- case 57: s = "print expected"; break;
- case 58: s = "then expected"; break;
- case 59: s = "<==> expected"; break;
- case 60: s = "\\u21d4 expected"; break;
- case 61: s = "==> expected"; break;
- case 62: s = "\\u21d2 expected"; break;
- case 63: s = "&& expected"; break;
- case 64: s = "\\u2227 expected"; break;
- case 65: s = "|| expected"; break;
- case 66: s = "\\u2228 expected"; break;
- case 67: s = "== expected"; break;
- case 68: s = "<= expected"; break;
- case 69: s = ">= expected"; break;
- case 70: s = "!= expected"; break;
- case 71: s = "!! expected"; break;
- case 72: s = "!in expected"; break;
- case 73: s = "\\u2260 expected"; break;
- case 74: s = "\\u2264 expected"; break;
- case 75: s = "\\u2265 expected"; break;
- case 76: s = "+ expected"; break;
- case 77: s = "- expected"; break;
- case 78: s = "/ expected"; break;
- case 79: s = "% expected"; break;
- case 80: s = "! expected"; break;
- case 81: s = "\\u00ac expected"; break;
- case 82: s = "false expected"; break;
- case 83: s = "true expected"; break;
- case 84: s = "null expected"; break;
- case 85: s = "# expected"; break;
- case 86: s = ". expected"; break;
- case 87: s = "fresh expected"; break;
- case 88: s = "[ expected"; break;
- case 89: s = "] expected"; break;
- case 90: s = ".. expected"; break;
- case 91: s = "this expected"; break;
- case 92: s = "old expected"; break;
- case 93: s = "forall expected"; break;
- case 94: s = "\\u2200 expected"; break;
- case 95: s = "exists expected"; break;
- case 96: s = "\\u2203 expected"; break;
- case 97: s = ":: expected"; break;
- case 98: s = "\\u2022 expected"; break;
- case 99: s = "??? expected"; break;
- case 100: s = "invalid ClassMemberDecl"; break;
- case 101: s = "invalid FunctionDecl"; break;
- case 102: s = "invalid MethodDecl"; break;
- case 103: s = "invalid TypeAndToken"; break;
- case 104: s = "invalid MethodSpec"; break;
+ case 33: s = "array expected"; break;
+ case 34: s = "function expected"; break;
+ case 35: s = "reads expected"; break;
+ case 36: s = "* expected"; break;
+ case 37: s = "` expected"; break;
+ case 38: s = "match expected"; break;
+ case 39: s = "case expected"; break;
+ case 40: s = "=> expected"; break;
+ case 41: s = "label expected"; break;
+ case 42: s = "break expected"; break;
+ case 43: s = "return expected"; break;
+ case 44: s = ":= expected"; break;
+ case 45: s = "new expected"; break;
+ case 46: s = "[ expected"; break;
+ case 47: s = "] expected"; break;
+ case 48: s = "havoc expected"; break;
+ case 49: s = "if expected"; break;
+ case 50: s = "else expected"; break;
+ case 51: s = "while expected"; break;
+ case 52: s = "invariant expected"; break;
+ case 53: s = "call expected"; break;
+ case 54: s = "foreach expected"; break;
+ case 55: s = "in expected"; break;
+ case 56: s = "| expected"; break;
+ case 57: s = "assert expected"; break;
+ case 58: s = "assume expected"; break;
+ case 59: s = "use expected"; break;
+ case 60: s = "print expected"; break;
+ case 61: s = "then expected"; break;
+ case 62: s = "<==> expected"; break;
+ case 63: s = "\\u21d4 expected"; break;
+ case 64: s = "==> expected"; break;
+ case 65: s = "\\u21d2 expected"; break;
+ case 66: s = "&& expected"; break;
+ case 67: s = "\\u2227 expected"; break;
+ case 68: s = "|| expected"; break;
+ case 69: s = "\\u2228 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 = "!in expected"; break;
+ case 76: s = "\\u2260 expected"; break;
+ case 77: s = "\\u2264 expected"; break;
+ case 78: s = "\\u2265 expected"; break;
+ case 79: s = "+ expected"; break;
+ case 80: s = "- expected"; break;
+ case 81: s = "/ expected"; break;
+ case 82: s = "% expected"; break;
+ case 83: s = "! expected"; break;
+ case 84: s = "\\u00ac expected"; break;
+ case 85: s = "false expected"; break;
+ case 86: s = "true expected"; break;
+ case 87: s = "null expected"; break;
+ case 88: s = "# expected"; break;
+ case 89: s = ". expected"; break;
+ case 90: s = "fresh expected"; break;
+ case 91: s = ".. expected"; break;
+ case 92: s = "this expected"; break;
+ case 93: s = "old expected"; break;
+ case 94: s = "forall expected"; break;
+ case 95: s = "\\u2200 expected"; break;
+ case 96: s = "exists expected"; break;
+ case 97: s = "\\u2203 expected"; break;
+ case 98: s = ":: expected"; break;
+ case 99: s = "\\u2022 expected"; break;
+ case 100: s = "??? expected"; break;
+ case 101: s = "invalid ClassMemberDecl"; break;
+ case 102: s = "invalid FunctionDecl"; break;
+ case 103: s = "invalid MethodDecl"; break;
+ case 104: s = "invalid TypeAndToken"; break;
case 105: s = "invalid MethodSpec"; break;
- case 106: s = "invalid Expression"; break;
- case 107: s = "invalid ReferenceType"; break;
- case 108: s = "invalid FunctionSpec"; break;
- case 109: s = "invalid FunctionBody"; break;
- case 110: s = "invalid PossiblyWildFrameExpression"; break;
- case 111: s = "invalid PossiblyWildExpression"; break;
- case 112: s = "invalid Stmt"; break;
- case 113: s = "invalid OneStmt"; break;
- case 114: s = "invalid IfStmt"; break;
- case 115: s = "invalid ForeachStmt"; break;
- case 116: s = "invalid AssignRhs"; break;
- case 117: s = "invalid SelectExpression"; break;
- case 118: s = "invalid Guard"; break;
- case 119: s = "invalid CallStmtSubExpr"; break;
- case 120: s = "invalid AttributeArg"; break;
- case 121: s = "invalid EquivOp"; break;
- case 122: s = "invalid ImpliesOp"; break;
- case 123: s = "invalid AndOp"; break;
- case 124: s = "invalid OrOp"; break;
- case 125: s = "invalid RelOp"; break;
- case 126: s = "invalid AddOp"; break;
- case 127: s = "invalid UnaryExpression"; break;
- case 128: s = "invalid MulOp"; break;
- case 129: s = "invalid NegOp"; break;
- case 130: s = "invalid ConstAtomExpression"; break;
- case 131: s = "invalid ObjectExpression"; break;
+ case 106: s = "invalid MethodSpec"; break;
+ case 107: s = "invalid Expression"; break;
+ case 108: s = "invalid ReferenceType"; break;
+ case 109: s = "invalid FunctionSpec"; break;
+ case 110: s = "invalid FunctionBody"; break;
+ case 111: s = "invalid PossiblyWildFrameExpression"; break;
+ case 112: s = "invalid PossiblyWildExpression"; break;
+ case 113: s = "invalid Stmt"; break;
+ case 114: s = "invalid OneStmt"; break;
+ case 115: s = "invalid IfStmt"; break;
+ case 116: s = "invalid ForeachStmt"; break;
+ case 117: s = "invalid AssignRhs"; break;
+ case 118: s = "invalid SelectExpression"; break;
+ case 119: s = "invalid Guard"; break;
+ case 120: s = "invalid CallStmtSubExpr"; break;
+ case 121: s = "invalid AttributeArg"; break;
+ case 122: s = "invalid EquivOp"; break;
+ case 123: s = "invalid ImpliesOp"; break;
+ case 124: s = "invalid AndOp"; break;
+ case 125: s = "invalid OrOp"; break;
+ case 126: s = "invalid RelOp"; break;
+ case 127: s = "invalid AddOp"; break;
+ case 128: s = "invalid UnaryExpression"; break;
+ case 129: s = "invalid MulOp"; break;
+ case 130: s = "invalid NegOp"; break;
+ case 131: s = "invalid ConstAtomExpression"; break;
case 132: s = "invalid ObjectExpression"; break;
- case 133: s = "invalid SelectOrCallSuffix"; break;
+ case 133: s = "invalid ObjectExpression"; break;
case 134: s = "invalid SelectOrCallSuffix"; break;
- case 135: s = "invalid QuantifierGuts"; break;
- case 136: s = "invalid Forall"; break;
- case 137: s = "invalid Exists"; break;
- case 138: s = "invalid AttributeOrTrigger"; break;
- case 139: s = "invalid QSep"; break;
+ case 135: s = "invalid SelectOrCallSuffix"; break;
+ case 136: s = "invalid QuantifierGuts"; break;
+ case 137: s = "invalid Forall"; break;
+ case 138: s = "invalid Exists"; break;
+ case 139: s = "invalid AttributeOrTrigger"; break;
+ case 140: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
@@ -1978,24 +1999,24 @@ 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,x, x},
- {x,x,x,x, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,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,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,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,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,x, x},
- {x,T,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, T,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,T,x,x, x,x,T,x, x,T,x,x, 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,T,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, 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,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, T,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,T,x,x, T,T,T,x, x,T,T,x, T,x,T,T, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, x,x,x,T, T,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {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, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, 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,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,x,T,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,T, T,T,x,T, 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, T,x,x,x, T,T,T,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,T,x, x,T,x,x, 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,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, x,x,x,x, T,T,x,T, x,T,T,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,x,T,x, x,T,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,x,T,x, T,T,x,x, x,x,x,x, x,x}
};
diff --git a/Source/Dafny/Printer.ssc b/Source/Dafny/Printer.ssc index 755c10b2..bf07e122 100644 --- a/Source/Dafny/Printer.ssc +++ b/Source/Dafny/Printer.ssc @@ -510,8 +510,14 @@ namespace Microsoft.Dafny { if (rhs is ExprRhs) {
PrintExpression(((ExprRhs)rhs).Expr);
} else if (rhs is TypeRhs) {
+ TypeRhs t = (TypeRhs)rhs;
wr.Write("new ");
- PrintType(((TypeRhs)rhs).Type);
+ PrintType(t.EType);
+ if (t.ArraySize != null) {
+ wr.Write("[");
+ PrintExpression(t.ArraySize);
+ wr.Write("]");
+ }
} else {
assert false; // unexpected RHS
}
diff --git a/Source/Dafny/Resolver.ssc b/Source/Dafny/Resolver.ssc index 0222b606..6e16aff6 100644 --- a/Source/Dafny/Resolver.ssc +++ b/Source/Dafny/Resolver.ssc @@ -577,7 +577,7 @@ namespace Microsoft.Dafny { } else {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
- } else {
+ } else if (t.ResolvedClass == null) { // this test is becausee 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')
TopLevelDecl d;
if (!classes.TryGetValue(t.Name, out d)) {
Error(t.tok, "Undeclared top-level type or type parameter: {0}", t.Name);
@@ -725,7 +725,7 @@ namespace Microsoft.Dafny { } else {
return false;
}
-
+
} else if (proxy is OperationTypeProxy) {
OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
if (t is IntType || t is SetType || (opProxy.AllowSeq && t is SeqType)) {
@@ -733,7 +733,22 @@ namespace Microsoft.Dafny { } else {
return false;
}
-
+
+ } else if (proxy is IndexableTypeProxy) {
+ IndexableTypeProxy iProxy = (IndexableTypeProxy)proxy;
+ if (t is SeqType) {
+ if (!UnifyTypes(iProxy.Arg, ((SeqType)t).Arg)) {
+ return false;
+ }
+ } else if (t.IsArrayType) {
+ Type elType = UserDefinedType.ArrayElementType(t);
+ if (!UnifyTypes(iProxy.Arg, elType)) {
+ return false;
+ }
+ } else {
+ return false;
+ }
+
} else {
assert false; // unexpected proxy type
}
@@ -759,6 +774,11 @@ namespace Microsoft.Dafny { // unify a and b by redirecting b to a, since a gives the stronger requirement
b.T = a;
return true;
+ } else if (b is IndexableTypeProxy) {
+ // the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
+ a.T = UserDefinedType.ArrayType(Token.NoToken, ((IndexableTypeProxy)b).Arg);
+ b.T = a.T;
+ return true;
} else {
return false;
}
@@ -770,8 +790,8 @@ namespace Microsoft.Dafny { return true;
} else if (b is CollectionTypeProxy) {
// fine provided b's collection-element-type can be unified with object or a class type
- a.T = new ObjectTypeProxy();
- return UnifyTypes(a.T, ((CollectionTypeProxy)b).Arg);
+ a.T = b;
+ return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());
} else if (b is OperationTypeProxy) {
// fine; restrict a to sets of object/class, and restrict b to set/seq of object/class
if (((OperationTypeProxy)b).AllowSeq) {
@@ -782,6 +802,14 @@ namespace Microsoft.Dafny { b.T = a.T;
}
return true;
+ } else if (b is IndexableTypeProxy) {
+ IndexableTypeProxy pb = (IndexableTypeProxy)b;
+ // the intersection of ObjectsTypeProxy and IndexableTypeProxy is
+ // EITHER a sequence of ObjectTypeProxy OR an array of anything
+ // TODO: here, only the first of the two cases is supported
+ b.T = new SeqType(pb.Arg);
+ a.T = b.T;
+ return UnifyTypes(pb.Arg, new ObjectTypeProxy());
} else {
assert false; // unexpected restricted-proxy type
}
@@ -799,18 +827,42 @@ namespace Microsoft.Dafny { b.T = a.T;
}
return true;
+ } else if (b is IndexableTypeProxy) {
+ CollectionTypeProxy pa = (CollectionTypeProxy)a;
+ IndexableTypeProxy pb = (IndexableTypeProxy)b;
+ // strengthen a and b to a sequence type
+ a.T = new SeqType(pa.Arg);
+ b.T = new SeqType(pb.Arg);
+ return UnifyTypes(pa.Arg, pb.Arg);
} else {
assert false; // unexpected restricted-proxy type
}
} else if (a is OperationTypeProxy) {
- assert b is OperationTypeProxy; // else we we have unexpected restricted-proxy type
- if (((OperationTypeProxy)a).AllowSeq ==> ((OperationTypeProxy)b).AllowSeq) {
- b.T = a;
+ OperationTypeProxy pa = (OperationTypeProxy)a;
+ if (b is OperationTypeProxy) {
+ if (pa.AllowSeq ==> ((OperationTypeProxy)b).AllowSeq) {
+ b.T = a;
+ } else {
+ a.T = b; // b has the stronger requirement
+ }
+ return true;
} else {
- a.T = b; // b has the stronger requirement
+ IndexableTypeProxy pb = (IndexableTypeProxy)b; // cast justification: lse we have unexpected restricted-proxy type
+ if (pa.AllowSeq) {
+ // strengthen a and b to a sequence type
+ b.T = new SeqType(pb.Arg);
+ a.T = b.T;
+ return true;
+ } else {
+ return false;
+ }
}
- return true;
+
+ } else if (a is IndexableTypeProxy) {
+ assert b is IndexableTypeProxy; // else we have unexpected restricted-proxy type
+ a.T = b;
+ return UnifyTypes(((IndexableTypeProxy)a).Arg, ((IndexableTypeProxy)b).Arg);
} else {
assert false; // unexpected restricted-proxy type
@@ -863,11 +915,15 @@ namespace Microsoft.Dafny { } else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
int prevErrorCount = ErrorCount;
- ResolveExpression(s.Lhs, true, true); // allow ghosts for now, but see FieldSelectExpr LHS case below
+ if (s.Lhs is SeqSelectExpr) {
+ ResolveSeqSelectExpr((SeqSelectExpr)s.Lhs, true, false, true);
+ } else {
+ ResolveExpression(s.Lhs, true, true); // allow ghosts for now, but see FieldSelectExpr LHS case below
+ }
bool lhsResolvedSuccessfully = ErrorCount == prevErrorCount;
assert s.Lhs.Type != null; // follows from postcondition of ResolveExpression
// check that LHS denotes a mutable variable or a field
- bool lvalueIsGhost = true;
+ bool lvalueIsGhost = false;
if (s.Lhs is IdentifierExpr) {
IVariable var = ((IdentifierExpr)s.Lhs).Var;
if (var == null) {
@@ -899,6 +955,23 @@ namespace Microsoft.Dafny { }
}
}
+ } else if (s.Lhs is SeqSelectExpr) {
+ SeqSelectExpr lhs = (SeqSelectExpr)s.Lhs;
+ // LHS is fine, provided the "sequence" is really an array
+ if (lhsResolvedSuccessfully) {
+ assert lhs.Seq.Type != null;
+ Type elementType = new InferredTypeProxy();
+ if (!UnifyTypes(lhs.Seq.Type, UserDefinedType.ArrayType(Token.NoToken, elementType))) {
+ Error(lhs.Seq, "LHS of array assignment must denote an array element (found {0})", lhs.Seq.Type);
+ }
+ if (specContextOnly) {
+ Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+ }
+ if (!(s.Rhs is ExprRhs)) {
+ Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");
+ }
+
} else {
Error(stmt, "LHS of assignment must denote a mutable variable or field");
}
@@ -908,16 +981,19 @@ namespace Microsoft.Dafny { ExprRhs rr = (ExprRhs)s.Rhs;
ResolveExpression(rr.Expr, true, lvalueIsGhost);
assert rr.Expr.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Lhs.Type, rr.Expr.Type)) {
+ Type lhsType = s.Lhs.Type;
+ if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {
+ assert lhsType.IsArrayType;
+ lhsType = UserDefinedType.ArrayElementType(lhsType);
+ }
+ if (!UnifyTypes(lhsType, rr.Expr.Type)) {
Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type);
}
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- ResolveType(rr.Type);
- if (!rr.Type.IsRefType) {
- Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
- } else if (!UnifyTypes(s.Lhs.Type, rr.Type)) {
- Error(stmt, "type {0} is not assignable to LHS (of type {1})", rr.Type, s.Lhs.Type);
+ Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost);
+ if (!UnifyTypes(s.Lhs.Type, t)) {
+ Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, s.Lhs.Type);
}
} else if (s.Rhs is HavocRhs) {
// nothing else to do
@@ -940,11 +1016,7 @@ namespace Microsoft.Dafny { rhsType = rr.Expr.Type;
} else if (s.Rhs is TypeRhs) {
TypeRhs rr = (TypeRhs)s.Rhs;
- ResolveType(rr.Type);
- if (!rr.Type.IsRefType) {
- Error(stmt, "new can be applied only to reference types (got {0})", rr.Type);
- }
- rhsType = rr.Type;
+ rhsType = ResolveTypeRhs(rr, stmt, s.IsGhost);
} else {
assert false; // unexpected RHS
}
@@ -1264,6 +1336,24 @@ namespace Microsoft.Dafny { assert false;
}
}
+
+ Type! ResolveTypeRhs(TypeRhs! rr, Statement! stmt, bool specContext) {
+ ResolveType(rr.EType);
+ if (rr.ArraySize == null) {
+ if (!rr.EType.IsRefType) {
+ Error(stmt, "new can be applied only to reference types (got {0})", rr.EType);
+ }
+ } else {
+ ResolveExpression(rr.ArraySize, true, specContext);
+ if (rr.ArraySize.Type is IntType) {
+ // all is good
+ return UserDefinedType.ArrayType(stmt.Tok, rr.EType);
+ } else {
+ Error(stmt, "new must use an integer expression for the array size (got {0})", rr.ArraySize.Type);
+ }
+ }
+ return rr.EType;
+ }
MemberDecl ResolveMember(Token! tok, Type! receiverType, string! memberName, out UserDefinedType ctype)
ensures result != null ==> ctype != null && ctype.ResolvedClass != null;
@@ -1499,35 +1589,7 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- bool seqErr = false;
- ResolveExpression(e.Seq, twoState, specContext);
- assert e.Seq.Type != null; // follows from postcondition of ResolveExpression
- Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(e.Seq.Type, new SeqType(elementType))) {
- Error(expr, "sequence selection requires a sequence (got {0})", e.Seq.Type);
- seqErr = true;
- }
- if (e.E0 != null) {
- ResolveExpression(e.E0, twoState, specContext);
- assert e.E0.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E0.Type, Type.Int)) {
- Error(e.E0, "sequence selection requires integer indices (got {0})", e.E0.Type);
- }
- }
- if (e.E1 != null) {
- ResolveExpression(e.E1, twoState, specContext);
- assert e.E1.Type != null; // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e.E1.Type, Type.Int)) {
- Error(e.E1, "sequence selection requires integer indices (got {0})", e.E1.Type);
- }
- }
- if (!seqErr) {
- if (e.SelectOne) {
- expr.Type = elementType;
- } else {
- expr.Type = e.Seq.Type;
- }
- }
+ ResolveSeqSelectExpr(e, twoState, specContext, false);
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
@@ -1665,8 +1727,8 @@ namespace Microsoft.Dafny { expr.Type = Type.Bool;
break;
case UnaryExpr.Opcode.SeqLength:
- if (!UnifyTypes(e.E.Type, new SeqType(new InferredTypeProxy()))) {
- Error(expr, "sequence-length operator expects a sequence argument (instead got {0})", e.E.Type);
+ if (!UnifyTypes(e.E.Type, new IndexableTypeProxy(new InferredTypeProxy()))) {
+ Error(expr, "length operator expects a sequence or array argument (instead got {0})", e.E.Type);
}
expr.Type = Type.Int;
break;
@@ -1933,6 +1995,44 @@ namespace Microsoft.Dafny { }
}
+ void ResolveSeqSelectExpr(SeqSelectExpr! e, bool twoState, bool specContext, bool allowNonUnitArraySelection) {
+ bool seqErr = false;
+ ResolveExpression(e.Seq, twoState, specContext);
+ assert e.Seq.Type != null; // follows from postcondition of ResolveExpression
+ Type elementType = new InferredTypeProxy();
+ Type expectedType;
+ if (e.SelectOne || allowNonUnitArraySelection) {
+ expectedType = new IndexableTypeProxy(elementType);
+ } else {
+ expectedType = new SeqType(elementType);
+ }
+ if (!UnifyTypes(e.Seq.Type, expectedType)) {
+ Error(e, "sequence/array selection requires a sequence or array (got {0})", e.Seq.Type);
+ seqErr = true;
+ }
+ if (e.E0 != null) {
+ ResolveExpression(e.E0, twoState, specContext);
+ assert e.E0.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E0.Type, Type.Int)) {
+ Error(e.E0, "sequence/array selection requires integer indices (got {0})", e.E0.Type);
+ }
+ }
+ if (e.E1 != null) {
+ ResolveExpression(e.E1, twoState, specContext);
+ assert e.E1.Type != null; // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e.E1.Type, Type.Int)) {
+ Error(e.E1, "sequence/array selection requires integer indices (got {0})", e.E1.Type);
+ }
+ }
+ if (!seqErr) {
+ if (e.SelectOne) {
+ e.Type = elementType;
+ } else {
+ e.Type = e.Seq.Type;
+ }
+ }
+ }
+
/// <summary>
/// Note: this method is allowed to be called even if "type" does not make sense for "op", as might be the case if
/// resolution of the binary expression failed. If so, an arbitrary resolved opcode is returned.
diff --git a/Source/Dafny/Scanner.ssc b/Source/Dafny/Scanner.ssc index cf759f84..5fdeefed 100644 --- a/Source/Dafny/Scanner.ssc +++ b/Source/Dafny/Scanner.ssc @@ -31,20 +31,20 @@ public class Scanner { [Microsoft.Contracts.Verify(false)]
static Scanner() {
start[0] = 55;
- start[33] = 33;
+ start[33] = 35;
start[34] = 3;
- start[35] = 46;
- start[37] = 44;
- start[38] = 27;
+ start[35] = 48;
+ start[37] = 46;
+ start[38] = 29;
start[39] = 1;
start[40] = 12;
start[41] = 13;
start[42] = 14;
- start[43] = 41;
+ start[43] = 43;
start[44] = 8;
- start[45] = 42;
- start[46] = 47;
- start[47] = 43;
+ start[45] = 44;
+ start[46] = 49;
+ start[47] = 45;
start[48] = 2;
start[49] = 2;
start[50] = 2;
@@ -87,9 +87,9 @@ public class Scanner { start[88] = 1;
start[89] = 1;
start[90] = 1;
- start[91] = 48;
+ start[91] = 19;
start[92] = 1;
- start[93] = 49;
+ start[93] = 20;
start[95] = 1;
start[96] = 15;
start[97] = 1;
@@ -119,21 +119,21 @@ public class Scanner { start[121] = 1;
start[122] = 1;
start[123] = 5;
- start[124] = 19;
+ start[124] = 21;
start[125] = 6;
- start[172] = 45;
+ start[172] = 47;
start[8226] = 54;
- start[8658] = 26;
- start[8660] = 23;
+ start[8658] = 28;
+ start[8660] = 25;
start[8704] = 51;
start[8707] = 52;
- start[8743] = 29;
- start[8744] = 31;
- start[8800] = 38;
- start[8804] = 39;
- start[8805] = 40;
+ start[8743] = 31;
+ start[8744] = 33;
+ start[8800] = 40;
+ start[8804] = 41;
+ start[8805] = 42;
}
- const int noSym = 99;
+ const int noSym = 100;
static short[] start = new short[16385];
@@ -295,35 +295,36 @@ public class Scanner { 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 = 37; break;
- case "case": t.kind = 38; break;
- case "label": t.kind = 40; break;
- case "break": t.kind = 41; break;
- case "return": t.kind = 42; break;
- case "new": t.kind = 44; break;
- case "havoc": t.kind = 45; break;
- case "if": t.kind = 46; break;
- case "else": t.kind = 47; break;
- case "while": t.kind = 48; break;
- case "invariant": t.kind = 49; break;
- case "call": t.kind = 50; break;
- case "foreach": t.kind = 51; break;
- case "in": t.kind = 52; break;
- case "assert": t.kind = 54; break;
- case "assume": t.kind = 55; break;
- case "use": t.kind = 56; break;
- case "print": t.kind = 57; break;
- case "then": t.kind = 58; break;
- case "false": t.kind = 82; break;
- case "true": t.kind = 83; break;
- case "null": t.kind = 84; break;
- case "fresh": t.kind = 87; break;
- case "this": t.kind = 91; break;
- case "old": t.kind = 92; break;
- case "forall": t.kind = 93; break;
- case "exists": t.kind = 95; break;
+ case "array": t.kind = 33; break;
+ case "function": t.kind = 34; break;
+ case "reads": t.kind = 35; break;
+ case "match": t.kind = 38; break;
+ case "case": t.kind = 39; break;
+ case "label": t.kind = 41; break;
+ case "break": t.kind = 42; break;
+ case "return": t.kind = 43; break;
+ case "new": t.kind = 45; break;
+ case "havoc": t.kind = 48; break;
+ case "if": t.kind = 49; break;
+ case "else": t.kind = 50; break;
+ case "while": t.kind = 51; break;
+ case "invariant": t.kind = 52; break;
+ case "call": t.kind = 53; break;
+ case "foreach": t.kind = 54; break;
+ case "in": t.kind = 55; break;
+ case "assert": t.kind = 57; break;
+ case "assume": t.kind = 58; break;
+ case "use": t.kind = 59; break;
+ case "print": t.kind = 60; break;
+ case "then": t.kind = 61; break;
+ case "false": t.kind = 85; break;
+ case "true": t.kind = 86; break;
+ case "null": t.kind = 87; break;
+ case "fresh": t.kind = 90; break;
+ case "this": t.kind = 92; break;
+ case "old": t.kind = 93; break;
+ case "forall": t.kind = 94; break;
+ case "exists": t.kind = 96; break;
default: break;
}
@@ -365,109 +366,109 @@ public class Scanner { else if (ch == ':') {buf.Append(ch); NextCh(); goto case 53;}
else {t.kind = 16; goto done;}
case 10:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 20;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 22;}
else {t.kind = 17; goto done;}
case 11:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 32;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
else {t.kind = 18; goto done;}
case 12:
{t.kind = 26; goto done;}
case 13:
{t.kind = 27; goto done;}
case 14:
- {t.kind = 35; goto done;}
- case 15:
{t.kind = 36; goto done;}
+ case 15:
+ {t.kind = 37; goto done;}
case 16:
if (ch == '>') {buf.Append(ch); NextCh(); goto case 17;}
- else if (ch == '=') {buf.Append(ch); NextCh(); goto case 24;}
+ else if (ch == '=') {buf.Append(ch); NextCh(); goto case 26;}
else {t.kind = noSym; goto done;}
case 17:
- {t.kind = 39; goto done;}
+ {t.kind = 40; goto done;}
case 18:
- {t.kind = 43; goto done;}
+ {t.kind = 44; goto done;}
case 19:
- if (ch == '|') {buf.Append(ch); NextCh(); goto case 30;}
- else {t.kind = 53; goto done;}
+ {t.kind = 46; goto done;}
case 20:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 21;}
- else {t.kind = 68; goto done;}
+ {t.kind = 47; goto done;}
case 21:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 22;}
- else {t.kind = noSym; goto done;}
+ if (ch == '|') {buf.Append(ch); NextCh(); goto case 32;}
+ else {t.kind = 56; goto done;}
case 22:
- {t.kind = 59; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 23;}
+ else {t.kind = 71; goto done;}
case 23:
- {t.kind = 60; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 24;}
+ else {t.kind = noSym; goto done;}
case 24:
- if (ch == '>') {buf.Append(ch); NextCh(); goto case 25;}
- else {t.kind = 67; goto done;}
+ {t.kind = 62; goto done;}
case 25:
- {t.kind = 61; goto done;}
+ {t.kind = 63; goto done;}
case 26:
- {t.kind = 62; goto done;}
+ if (ch == '>') {buf.Append(ch); NextCh(); goto case 27;}
+ else {t.kind = 70; goto done;}
case 27:
- if (ch == '&') {buf.Append(ch); NextCh(); goto case 28;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 64; goto done;}
case 28:
- {t.kind = 63; goto done;}
+ {t.kind = 65; goto done;}
case 29:
- {t.kind = 64; goto done;}
+ if (ch == '&') {buf.Append(ch); NextCh(); goto case 30;}
+ else {t.kind = noSym; goto done;}
case 30:
- {t.kind = 65; goto done;}
- case 31:
{t.kind = 66; goto done;}
+ case 31:
+ {t.kind = 67; goto done;}
case 32:
- {t.kind = 69; goto done;}
+ {t.kind = 68; goto done;}
case 33:
- if (ch == '=') {buf.Append(ch); NextCh(); goto case 34;}
- else if (ch == '!') {buf.Append(ch); NextCh(); goto case 35;}
- else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 36;}
- else {t.kind = 80; goto done;}
+ {t.kind = 69; goto done;}
case 34:
- {t.kind = 70; goto done;}
+ {t.kind = 72; goto done;}
case 35:
- {t.kind = 71; goto done;}
+ if (ch == '=') {buf.Append(ch); NextCh(); goto case 36;}
+ else if (ch == '!') {buf.Append(ch); NextCh(); goto case 37;}
+ else if (ch == 'i') {buf.Append(ch); NextCh(); goto case 38;}
+ else {t.kind = 83; goto done;}
case 36:
- if (ch == 'n') {buf.Append(ch); NextCh(); goto case 37;}
- else {t.kind = noSym; goto done;}
+ {t.kind = 73; goto done;}
case 37:
- {t.kind = 72; goto done;}
+ {t.kind = 74; goto done;}
case 38:
- {t.kind = 73; goto done;}
+ if (ch == 'n') {buf.Append(ch); NextCh(); goto case 39;}
+ else {t.kind = noSym; goto done;}
case 39:
- {t.kind = 74; goto done;}
- case 40:
{t.kind = 75; goto done;}
- case 41:
+ case 40:
{t.kind = 76; goto done;}
- case 42:
+ case 41:
{t.kind = 77; goto done;}
- case 43:
+ case 42:
{t.kind = 78; goto done;}
- case 44:
+ case 43:
{t.kind = 79; goto done;}
+ case 44:
+ {t.kind = 80; goto done;}
case 45:
{t.kind = 81; goto done;}
case 46:
- {t.kind = 85; goto done;}
+ {t.kind = 82; goto done;}
case 47:
- if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
- else {t.kind = 86; goto done;}
+ {t.kind = 84; goto done;}
case 48:
{t.kind = 88; goto done;}
case 49:
- {t.kind = 89; goto done;}
+ if (ch == '.') {buf.Append(ch); NextCh(); goto case 50;}
+ else {t.kind = 89; goto done;}
case 50:
- {t.kind = 90; goto done;}
+ {t.kind = 91; goto done;}
case 51:
- {t.kind = 94; goto done;}
+ {t.kind = 95; goto done;}
case 52:
- {t.kind = 96; goto done;}
- case 53:
{t.kind = 97; goto done;}
- case 54:
+ case 53:
{t.kind = 98; goto done;}
+ case 54:
+ {t.kind = 99; goto done;}
case 55: {t.kind = 0; goto done;}
}
done:
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc index c079db7e..778096e9 100644 --- a/Source/Dafny/Translator.ssc +++ b/Source/Dafny/Translator.ssc @@ -104,6 +104,7 @@ namespace Microsoft.Dafny { public readonly string! HeapVarName;
public readonly Bpl.Constant! CevHeapName;
public readonly Bpl.Type! ClassNameType;
+ public readonly Bpl.Type! FieldCategoryType;
public readonly Bpl.Type! DatatypeType;
public readonly Bpl.Type! DtCtorId;
public readonly Bpl.Expr! Null;
@@ -114,7 +115,8 @@ namespace Microsoft.Dafny { public PredefinedDecls(Bpl.TypeCtorDecl! refType, Bpl.TypeCtorDecl! boxType, Bpl.TypeCtorDecl! cevTokenType, Bpl.TypeCtorDecl! cevVariableKind, Bpl.TypeCtorDecl! cevEventType,
Bpl.TypeSynonymDecl! setTypeCtor, Bpl.TypeCtorDecl! seqTypeCtor, Bpl.TypeCtorDecl! fieldNameType,
- Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
+ Bpl.GlobalVariable! heap, Bpl.TypeCtorDecl! classNameType, Bpl.TypeCtorDecl! fieldCategoryType,
+ Bpl.TypeCtorDecl! datatypeType, Bpl.TypeCtorDecl! dtCtorId,
Bpl.Constant! allocField, Bpl.Constant! cevHeapNameConst) {
Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());
this.RefType = refT;
@@ -129,6 +131,7 @@ namespace Microsoft.Dafny { this.HeapVarName = heap.Name;
this.CevHeapName = cevHeapNameConst;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
+ this.FieldCategoryType = new Bpl.CtorType(Token.NoToken, fieldCategoryType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
@@ -150,6 +153,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
+ Bpl.TypeCtorDecl fieldCategoryType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
@@ -165,6 +169,8 @@ namespace Microsoft.Dafny { fieldNameType = dt;
} else if (dt.Name == "ClassName") {
classNameType = dt;
+ } else if (dt.Name == "FieldCategory") {
+ fieldCategoryType = dt;
} else if (dt.Name == "DatatypeType") {
datatypeType = dt;
} else if (dt.Name == "DtCtorId") {
@@ -207,6 +213,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
+ } else if (fieldCategoryType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type FieldCategory");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (dtCtorId == null) {
@@ -229,7 +237,7 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of constant #loc.$Heap");
} else {
return new PredefinedDecls(refType, boxType, cevTokenType, cevVariableKind, cevEventType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, fieldCategoryType, datatypeType, dtCtorId,
allocField, cevHeapNameConst);
}
return null;
@@ -623,7 +631,7 @@ namespace Microsoft.Dafny { Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.BoxType, oDotF, i);
Bpl.Expr unbox = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, oDotFsubI);
- Bpl.Expr range = InSeqRange(f.tok, i, oDotF, null, false);
+ Bpl.Expr range = InSeqRange(f.tok, i, oDotF, true, null, false);
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotFsubI));
@@ -652,16 +660,17 @@ namespace Microsoft.Dafny { }
}
- Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, Bpl.Expr lowerBound, bool includeUpperBound) {
+ Bpl.Expr! InSeqRange(Token! tok, Bpl.Expr! index, Bpl.Expr! seq, bool isSequence, Bpl.Expr lowerBound, bool includeUpperBound) {
if (lowerBound == null) {
lowerBound = Bpl.Expr.Literal(0);
}
Bpl.Expr lower = Bpl.Expr.Le(lowerBound, index);
+ Bpl.Expr length = FunctionCall(tok, isSequence ? BuiltinFunction.SeqLength : BuiltinFunction.ArrayLength, null, seq);
Bpl.Expr upper;
if (includeUpperBound) {
- upper = Bpl.Expr.Le(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
+ upper = Bpl.Expr.Le(index, length);
} else {
- upper = Bpl.Expr.Lt(index, FunctionCall(tok, BuiltinFunction.SeqLength, null, seq));
+ upper = Bpl.Expr.Lt(index, length);
}
return Bpl.Expr.And(lower, upper);
}
@@ -975,7 +984,7 @@ namespace Microsoft.Dafny { Bpl.Expr boxO = FunctionCall(tok, BuiltinFunction.Box, null, o);
Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);
- Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), null, false);
+ Bpl.Expr iBounds = InSeqRange(tok, i, etran.TrExpr(e), true, null, false);
Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i);
// TODO: the equality in the next line should be changed to one that understands extensionality
disjunct = new Bpl.ExistsExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(iBounds, Bpl.Expr.Eq(XsubI, boxO)));
@@ -1083,17 +1092,18 @@ namespace Microsoft.Dafny { }
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
+ bool isSequence = e.Seq.Type is SeqType;
Bpl.Expr total = IsTotal(e.Seq, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
total = BplAnd(total, IsTotal(e.E0, etran));
- total = BplAnd(total, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne));
+ total = BplAnd(total, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne));
}
if (e.E1 != null) {
total = BplAnd(total, IsTotal(e.E1, etran));
- total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true));
+ total = BplAnd(total, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true));
}
return total;
} else if (expr is SeqUpdateExpr) {
@@ -1102,7 +1112,7 @@ namespace Microsoft.Dafny { Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
total = BplAnd(total, IsTotal(e.Index, etran));
- total = BplAnd(total, InSeqRange(expr.tok, index, seq, null, false));
+ total = BplAnd(total, InSeqRange(expr.tok, index, seq, true, null, false));
total = BplAnd(total, IsTotal(e.Value, etran));
return total;
} else if (expr is FunctionCallExpr) {
@@ -1137,7 +1147,11 @@ namespace Microsoft.Dafny { return IsTotal(e.E, etran);
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
- return IsTotal(e.E, etran);
+ Bpl.Expr t = IsTotal(e.E, etran);
+ if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ return Bpl.Expr.And(t, Bpl.Expr.Neq(etran.TrExpr(e.E), predef.Null));
+ }
+ return t;
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
Bpl.Expr t0 = IsTotal(e.E0, etran);
@@ -1240,17 +1254,23 @@ namespace Microsoft.Dafny { }
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
+ bool isSequence = e.Seq.Type is SeqType;
CheckWellformed(e.Seq, func, Position.Neither, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
CheckWellformed(e.E0, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, null, !e.SelectOne), "index out of range"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range"));
}
if (e.E1 != null) {
CheckWellformed(e.E1, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, e0, true), "end-of-range beyond length of sequence"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array")));
+ }
+ if (func != null && ((!)e.Seq.Type).IsArrayType) {
+ assert e.E0 != null;
+ Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
+ builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element"));
}
} else if (expr is SeqUpdateExpr) {
SeqUpdateExpr e = (SeqUpdateExpr)expr;
@@ -1258,7 +1278,7 @@ namespace Microsoft.Dafny { Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr index = etran.TrExpr(e.Index);
CheckWellformed(e.Index, func, Position.Neither, locals, builder, etran);
- builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, null, false), "index out of range"));
+ builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range"));
CheckWellformed(e.Value, func, Position.Neither, locals, builder, etran);
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
@@ -1325,6 +1345,9 @@ namespace Microsoft.Dafny { } else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
CheckWellformed(e.E, func, e.Op == UnaryExpr.Opcode.Not ? Negate(pos) : Position.Neither, locals, builder, etran);
+ if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {
+ CheckNonNull(expr.tok, e.E, builder, etran);
+ }
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
CheckWellformed(e.E0, func, e.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp ? Negate(pos) : pos, locals, builder, etran);
@@ -1423,8 +1446,6 @@ namespace Microsoft.Dafny { if (classes.TryGetValue(cl, out cc)) {
assert cc != null;
} else {
- // TODO: make the following a function when the class has type parameters, so that different instantiations
- // of a class can be distinguished
cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.Name, predef.ClassNameType), true);
classes.Add(cl, cc);
}
@@ -1485,11 +1506,14 @@ namespace Microsoft.Dafny { if (fields.TryGetValue(f, out fc)) {
assert fc != null;
} else {
+ // const unique f: Field ty;
Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);
fields.Add(f, fc);
- // axiom DeclType(f) == C;
- Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass))));
+ // axiom FCat(f) == $NamedField && DeclType(f) == C;
+ Bpl.Expr fcat = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FCat, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, "$NamedField", predef.FieldCategoryType));
+ Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass((!)f.EnclosingClass)));
+ Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fcat, declType));
sink.TopLevelDeclarations.Add(ax);
}
return fc;
@@ -1849,6 +1873,8 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdate",
new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, v.Name), v),
new Bpl.IdentifierExprSeq()));
+ } else if (s.Lhs is SeqSelectExpr) {
+ // TODO: CEV
} else {
builder.Add(new Bpl.CallCmd(stmt.Tok, "CevUpdateHeap",
new Bpl.ExprSeq(CevLocation(stmt.Tok), CevVariable(stmt.Tok, predef.HeapVarName), etran.HeapExpr),
@@ -2013,6 +2039,30 @@ namespace Microsoft.Dafny { int loopId = loopHeapVarCount;
loopHeapVarCount++;
+ // use simple heuristics to create a default decreases clause, if none is given
+ List<Expression!> theDecreases = s.Decreases;
+ if (theDecreases.Count == 0) {
+ Expression guess = null;
+ BinaryExpr bin = s.Guard as BinaryExpr;
+ if (bin != null) {
+ switch (bin.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Lt:
+ case BinaryExpr.ResolvedOpcode.Le:
+ guess = IntSub(s.Tok, bin.E1, bin.E0);
+ break;
+ case BinaryExpr.ResolvedOpcode.Ge:
+ case BinaryExpr.ResolvedOpcode.Gt:
+ guess = IntSub(s.Tok, bin.E0, bin.E1);
+ break;
+ default:
+ break;
+ }
+ }
+ if (guess != null) {
+ theDecreases.Add(guess);
+ }
+ }
+
Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopHeap" + loopId, predef.HeapType));
locals.Add(preLoopHeapVar);
Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(stmt.Tok, preLoopHeapVar);
@@ -2055,7 +2105,7 @@ namespace Microsoft.Dafny { }
}
// check definedness of decreases clause
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
invDefinednessBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration")); // totality check
}
// include boilerplate invariants
@@ -2104,13 +2154,13 @@ namespace Microsoft.Dafny { new Bpl.ExprSeq(CevLocation(stmt.Tok), new Bpl.IdentifierExpr(stmt.Tok, "loop_entered", predef.CevEventType)),
new Bpl.IdentifierExprSeq()));
// termination checking
- if (exists{Expression e in s.Decreases; e is WildcardExpr}) {
+ if (exists{Expression e in theDecreases; e is WildcardExpr}) {
// omit termination checking for this loop
TrStmt(s.Body, loopBodyBuilder, locals, etran);
} else {
List<Bpl.Expr!> oldBfs = new List<Bpl.Expr!>();
int c = 0;
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, "$decr" + loopId + "$" + c, TrType((!)e.Type)));
locals.Add(bfVar);
Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar);
@@ -2127,7 +2177,7 @@ namespace Microsoft.Dafny { List<Token!> toks = new List<Token!>();
List<Type!> types = new List<Type!>();
List<Bpl.Expr!> decrs = new List<Bpl.Expr!>();
- foreach (Expression e in s.Decreases) {
+ foreach (Expression e in theDecreases) {
toks.Add(e.tok);
types.Add((!)e.Type);
decrs.Add(etran.TrExpr(e));
@@ -2171,7 +2221,7 @@ namespace Microsoft.Dafny { Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
Bpl.Expr S = etran.TrExpr(s.Collection);
- Bpl.Expr range = InSeqRange(stmt.Tok, i, S, null, false);
+ Bpl.Expr range = InSeqRange(stmt.Tok, i, S, true, null, false);
Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
// TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
@@ -2312,6 +2362,15 @@ namespace Microsoft.Dafny { }
}
+ static Expression! IntSub(Token! tok, Expression! e0, Expression! e1)
+ requires e0.Type is IntType && e1.Type is IntType;
+ {
+ BinaryExpr s = new BinaryExpr(tok, BinaryExpr.Opcode.Sub, e0, e1);
+ s.ResolvedOp = BinaryExpr.ResolvedOpcode.Sub;
+ s.Type = Type.Int;
+ return s;
+ }
+
void CheckCallTermination(Token! tok, List<Expression!>! contextDecreases, List<Expression!>! calleeDecreases,
Expression receiverReplacement, Dictionary<IVariable,Expression!>! substMap,
ExpressionTranslator! etran, Bpl.StmtListBuilder! builder)
@@ -2489,7 +2548,7 @@ namespace Microsoft.Dafny { Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);
Bpl.Expr unbox = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, xSubI);
- Bpl.Expr range = InSeqRange(tok, i, x, null, false);
+ Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));
@@ -2523,7 +2582,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs); // TODO: is this cast always justified?
Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, bLhs, bRhs);
builder.Add(cmd);
- } else {
+ } else if (lhs is FieldSelectExpr) {
FieldSelectExpr fse = (FieldSelectExpr)lhs;
assert fse.Field != null;
// check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj];
@@ -2535,6 +2594,38 @@ namespace Microsoft.Dafny { builder.Add(cmd);
// assume $IsGoodHeap($Heap);
builder.Add(AssumeGoodHeap(tok, etran));
+ } else {
+ SeqSelectExpr sel = (SeqSelectExpr)lhs;
+ assert sel.Seq.Type != null && sel.Seq.Type.IsArrayType;
+ bRhs = etran.BoxIfNecessary(tok, bRhs, UserDefinedType.ArrayElementType(sel.Seq.Type));
+ if (sel.SelectOne) {
+ assert sel.E0 != null;
+ Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0));
+ // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index];
+ builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName), "assignment may update an array not in the enclosing method's modifies clause"));
+
+ Bpl.IdentifierExpr h = (Bpl.IdentifierExpr!)etran.HeapExpr; // TODO: is this cast always justified?
+ Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, h, etran.TrExpr(sel.Seq), fieldName, bRhs);
+ builder.Add(cmd);
+ // assume $IsGoodHeap($Heap);
+ builder.Add(AssumeGoodHeap(tok, etran));
+ } else {
+ Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);
+ Bpl.Expr high = sel.E1 == null ? FunctionCall(tok, BuiltinFunction.ArrayLength, null, etran.TrExpr(sel.Seq)) : etran.TrExpr(sel.E1);
+ // check frame:
+ // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);
+ Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));
+ Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(tok, iVar);
+ Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Le(low, ie), Bpl.Expr.Lt(ie, high));
+ Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, ie);
+ Bpl.Expr cons = Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), etran.TrExpr(sel.Seq), fieldName);
+ Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), Bpl.Expr.Imp(ante, cons));
+ builder.Add(Assert(tok, q, "assignment may update an array not in the enclosing method's modifies clause"));
+ // do the update: call UpdateArrayRange(arr, low, high, rhs);
+ builder.Add(new Bpl.CallCmd(tok, "UpdateArrayRange",
+ new Bpl.ExprSeq(etran.TrExpr(sel.Seq), low, high, bRhs),
+ new Bpl.IdentifierExprSeq()));
+ }
}
} else if (rhs is HavocRhs) {
@@ -2544,13 +2635,35 @@ namespace Microsoft.Dafny { } else {
assert rhs is TypeRhs; // otherwise, an unexpected AssignmentRhs
+ TypeRhs tRhs = (TypeRhs)rhs;
assert lhs is IdentifierExpr; // for this kind of RHS, the LHS is restricted to be a simple variable
+ if (tRhs.ArraySize != null) {
+ CheckWellformed(tRhs.ArraySize, null, Position.Positive, locals, builder, etran);
+ builder.Add(Assert(tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(tRhs.ArraySize)), "array size might be negative"));
+ }
+
Bpl.IdentifierExpr nw = GetNewVar_IdExpr(tok, locals);
builder.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(nw)));
// assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;
Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);
- builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, etran.GoodRef_Class(tok, nw, (UserDefinedType)((TypeRhs)rhs).Type, true))));
+ Bpl.Expr rightType;
+ if (tRhs.ArraySize != null) {
+ // array allocation
+ List<Type!> typeArgs = new List<Type!>();
+ typeArgs.Add(tRhs.EType);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.array", predef.ClassNameType), typeArgs, true);
+ } else if (tRhs.EType is ObjectType) {
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class.object", predef.ClassNameType), new List<Type!>(), true);
+ } else {
+ rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
+ }
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));
+ if (tRhs.ArraySize != null) {
+ // assume Array#Length($nw) == arraySize;
+ Bpl.Expr arrayLength = FunctionCall(tok, BuiltinFunction.ArrayLength, null, nw);
+ builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(tRhs.ArraySize))));
+ }
// $Heap[$nw, alloc] := true;
Bpl.Expr alloc = predef.Alloc(tok);
Bpl.Cmd cmd = Bpl.Cmd.MapAssign(tok, (Bpl.IdentifierExpr/*TODO: this cast is dubious*/)etran.HeapExpr, nw, alloc, Bpl.Expr.True);
@@ -2685,13 +2798,26 @@ namespace Microsoft.Dafny { } else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
- Type elmtType = ((SeqType!)e.Seq.Type).Arg;
+ Type elmtType;
+ assert e.Seq.Type != null; // the expression has been successfully resolved
+ if (e.Seq.Type.IsArrayType) {
+ assert e.SelectOne; // resolution enforces that a non-unit array selections is allowed only as an assignment LHS
+ elmtType = UserDefinedType.ArrayElementType(e.Seq.Type);
+ } else {
+ elmtType = ((SeqType)e.Seq.Type).Arg;
+ }
Bpl.Type elType = translator.TrType(elmtType);
Bpl.Expr e0 = e.E0 == null ? null : TrExpr(e.E0);
Bpl.Expr e1 = e.E1 == null ? null : TrExpr(e.E1);
if (e.SelectOne) {
assert e1 == null;
- Bpl.Expr x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
+ Bpl.Expr x;
+ if (e.Seq.Type.IsArrayType) {
+ Bpl.Expr fieldName = translator.FunctionCall(expr.tok, BuiltinFunction.IndexField, null, e0);
+ x = Bpl.Expr.SelectTok(expr.tok, HeapExpr, TrExpr(e.Seq), fieldName);
+ } else {
+ x = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.BoxType, seq, e0);
+ }
if (!ModeledAsBoxType(elmtType)) {
x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x);
}
@@ -2773,7 +2899,7 @@ namespace Microsoft.Dafny { // TODO: trigger?
Bpl.Variable iVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, "$i", Bpl.Type.Int));
Bpl.Expr i = new Bpl.IdentifierExpr(expr.tok, iVar);
- Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), null, false);
+ Bpl.Expr iBounds = translator.InSeqRange(expr.tok, i, TrExpr(e.E), true, null, false);
Bpl.Expr XsubI = translator.FunctionCall(expr.tok, BuiltinFunction.SeqIndex, predef.RefType, TrExpr(e.E), i);
Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, XsubI, oldHeap));
Bpl.Expr xsubiNotNull = Bpl.Expr.Neq(translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, predef.RefType, XsubI), predef.Null);
@@ -2793,7 +2919,11 @@ namespace Microsoft.Dafny { case UnaryExpr.Opcode.Not:
return Bpl.Expr.Not(arg);
case UnaryExpr.Opcode.SeqLength:
- return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
+ if (e.E.Type is SeqType) {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.SeqLength, null, arg);
+ } else {
+ return translator.FunctionCall(expr.tok, BuiltinFunction.ArrayLength, null, arg);
+ }
default:
assert false; // unexpected unary expression
}
@@ -3087,6 +3217,10 @@ namespace Microsoft.Dafny { public Bpl.Expr! GoodRef_Class(Token! tok, Bpl.Expr! e, UserDefinedType! type, bool isNew)
requires type.ResolvedClass is ClassDecl;
{
+ return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);
+ }
+
+ public Bpl.Expr! GoodRef_Ref(Token! tok, Bpl.Expr! e, Bpl.Expr! type, List<Type!>! typeArgs, bool isNew) {
// Heap[e, alloc]
Bpl.Expr r = IsAlloced(tok, e);
if (isNew) {
@@ -3095,12 +3229,12 @@ namespace Microsoft.Dafny { // dtype(e) == C
Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);
- Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)));
+ Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);
r = Bpl.Expr.And(r, dtype);
// dtypeParams(e, #) == T
int n = 0;
- foreach (Type arg in type.TypeArgs) {
+ foreach (Type arg in typeArgs) {
Bpl.Expr tpFunc = translator.FunctionCall(tok, BuiltinFunction.TypeParams, null, e, Bpl.Expr.Literal(n));
Bpl.Expr ta = translator.GetTypeExpr(tok, arg);
if (ta != null) {
@@ -3180,6 +3314,9 @@ namespace Microsoft.Dafny { SeqEqual,
SeqSameUntil,
+ ArrayLength,
+ IndexField,
+
IfThenElse,
Box,
@@ -3192,6 +3329,7 @@ namespace Microsoft.Dafny { TypeParams, // type parameters to allocated type
TypeTuple,
DeclType,
+ FCat, // field category (indexed or named)
DatatypeCtorId,
DtRank,
@@ -3291,6 +3429,15 @@ namespace Microsoft.Dafny { assert typeInstantiation == null;
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
+ case BuiltinFunction.ArrayLength:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "Array#Length", Bpl.Type.Int, args);
+ case BuiltinFunction.IndexField:
+ assert args.Length == 1;
+ assert typeInstantiation == null;
+ return FunctionCall(tok, "IndexField", predef.FieldName(tok, predef.BoxType), args);
+
case BuiltinFunction.IfThenElse:
assert args.Length == 3;
assert typeInstantiation != null;
@@ -3330,6 +3477,10 @@ namespace Microsoft.Dafny { assert args.Length == 1;
assert typeInstantiation != null;
return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
+ case BuiltinFunction.FCat:
+ assert args.Length == 1;
+ assert typeInstantiation != null;
+ return FunctionCall(tok, "FCat", predef.FieldCategoryType, args);
case BuiltinFunction.DatatypeCtorId:
assert args.Length == 1;
diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc index f6e10e59..8920db94 100644 --- a/Source/DafnyDriver/DafnyDriver.ssc +++ b/Source/DafnyDriver/DafnyDriver.ssc @@ -230,7 +230,7 @@ namespace Microsoft.Boogie PipelineOutcome oc = BoogiePipelineWithRerun(boogieProgram, bplFilename, null/*new ErrorReporter()*/, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
switch (oc) {
case PipelineOutcome.VerificationCompleted:
- if (CommandLineOptions.Clo.Compile) {
+ if (CommandLineOptions.Clo.Compile && errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0) {
string targetFilename = "out.cs";
using (TextWriter target = new StreamWriter(new FileStream(targetFilename, System.IO.FileMode.Create))) {
Dafny.Compiler compiler = new Dafny.Compiler(target);
diff --git a/Test/VSI-Benchmarks/Answer b/Test/VSI-Benchmarks/Answer index 1efeba04..2a4587f4 100644 --- a/Test/VSI-Benchmarks/Answer +++ b/Test/VSI-Benchmarks/Answer @@ -5,7 +5,7 @@ Dafny program verifier finished with 10 verified, 0 errors -------------------- b2.dfy --------------------
-Dafny program verifier finished with 12 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
-------------------- b3.dfy --------------------
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index ec255ed1..fd20a72b 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -1,27 +1,23 @@ -// Note:Implemented arrays as Dafny does not provide them
-
class Benchmark2 {
- method BinarySearch(a: Array, key: int) returns (result: int)
+ method BinarySearch(a: array<int>, key: int) returns (result: int)
requires a != null;
- requires (forall i, j ::
- 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
- ensures -1 <= result && result < a.Length();
- ensures 0 <= result ==> a.Get(result) == key;
- ensures result == -1 ==>
- (forall i :: 0 <= i && i < a.Length() ==> a.Get(i) != key);
+ requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
+ ensures -1 <= result && result < |a|;
+ ensures 0 <= result ==> a[result] == key;
+ ensures result == -1 ==> (forall i :: 0 <= i && i < |a| ==> a[i] != key);
{
var low := 0;
- var high := a.Length();
+ var high := |a|;
while (low < high)
- invariant 0 <= low && low <= high && high <= a.Length();
- invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
- invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
+ invariant 0 <= low && low <= high && high <= |a|;
+ invariant (forall i :: 0 <= i && i < low ==> a[i] < key);
+ invariant (forall i :: high <= i && i < |a| ==> key < a[i]);
decreases high - low;
{
var mid := low + (high - low) / 2;
- var midVal := a.Get(mid);
+ var midVal := a[mid];
if (midVal < key) {
low := mid + 1;
@@ -36,47 +32,13 @@ class Benchmark2 { }
}
-class Array {
- var contents: seq<int>;
- method Init(n: int)
- requires 0 <= n;
- modifies this;
- ensures |contents| == n;
- {
- var i := 0;
- contents := [];
- while (i < n)
- invariant i <= n && i == |contents|;
- decreases n - i;
- {
- contents := contents + [0];
- i := i + 1;
- }
- }
- function method Length(): int
- reads this;
- { |contents| }
- function method Get(i: int): int
- requires 0 <= i && i < |contents|;
- reads this;
- { contents[i] }
- method Set(i: int, x: int)
- requires 0 <= i && i < |contents|;
- modifies this;
- ensures contents == old(contents)[i := x];
- {
- contents := contents[i := x];
- }
-}
-
method Main() {
- var a := new Array;
- call a.Init(5);
- call a.Set(0, -4);
- call a.Set(1, -2);
- call a.Set(2, -2);
- call a.Set(3, 0);
- call a.Set(4, 25);
+ var a := new int[5];
+ a[0] := -4;
+ a[1] := -2;
+ a[2] := -2;
+ a[3] := 0;
+ a[4] := 25;
call TestSearch(a, 4);
call TestSearch(a, -8);
call TestSearch(a, -2);
@@ -86,9 +48,9 @@ method Main() { call TestSearch(a, 27);
}
-method TestSearch(a: Array, key: int)
+method TestSearch(a: array<int>, key: int)
requires a != null;
- requires (forall i, j :: 0 <= i && i < j && j < a.Length() ==> a.Get(i) <= a.Get(j));
+ requires (forall i, j :: 0 <= i && i < j && j < |a| ==> a[i] <= a[j]);
{
var b := new Benchmark2;
call r := b.BinarySearch(a, key);
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 37b73cba..6d9c3ddd 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -64,7 +64,6 @@ class Benchmark3 { invariant n <= |q.contents|;
invariant n == |p|;
invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
- decreases |q.contents| - n;
{
p := p + [n];
n := n + 1;
@@ -121,7 +120,6 @@ class Benchmark3 { invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
invariant 0 <= k && k < |old(q.contents)| && old(q.contents)[k] == m;
invariant (forall i ::0<= i && i < j ==> m <= old(q.contents)[i]); //m is min so far
- decreases n-j;
{
call x:= q.Dequeue();
call q.Enqueue(x);
@@ -134,7 +132,6 @@ class Benchmark3 { while (j < k)
invariant j <= k;
invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j];
- decreases k-j;
{
call x := q.Dequeue();
call q.Enqueue(x);
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index ab1285f6..d2fca9bc 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -95,7 +95,6 @@ class Map<Key,Value> { while (j < |keys|)
invariant j <= |keys|;
invariant key !in keys[..j];
- decreases |keys| -j;
{
if (keys[j] == key) {
idx := j;
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index e5af6357..2304e602 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -142,7 +142,6 @@ class Client { call wr.Create();
while (0 < |q.contents|)
invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
- decreases |q.contents|;
{
call ch := q.Dequeue();
call wr.PutChar(ch);
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index d8ee2013..34e0cfef 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -104,7 +104,6 @@ class Glossary { invariant q !in wr.footprint;
invariant qcon == q.contents;
invariant (forall k :: k in q.contents ==> k in glossary.keys);
- decreases |definition| -i;
{
var w := definition[i];
call present, d := glossary.Find(w);
@@ -342,7 +341,6 @@ class Map<Key,Value> { while (j < |keys|)
invariant j <= |keys|;
invariant key !in keys[..j];
- decreases |keys| -j;
{
if (keys[j] == key) {
idx := j;
diff --git a/Test/alltests.txt b/Test/alltests.txt index 2648581c..6d44550e 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -21,4 +21,5 @@ houdini Postponed Test for Houdini decision procedure dafny0 Use Dafny programs
havoc0 Use HAVOC-generated bpl files
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
+vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
livevars Use STORM benchmarks for testing correctness of live variable analysis
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 726a6c13..59582de8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -78,7 +78,8 @@ TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 0 (expected i TypeTests.dfy(12,4): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(20,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Nothing' can be constructed
TypeTests.dfy(23,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
-9 resolution/type errors detected in TypeTests.dfy
+TypeTests.dfy(55,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+10 resolution/type errors detected in TypeTests.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,7): Error: RHS expression must be well defined
@@ -123,7 +124,7 @@ Execution trace: (0,0): anon4_Else
(0,0): anon3
-Dafny program verifier finished with 22 verified, 9 errors
+Dafny program verifier finished with 24 verified, 9 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
@@ -265,6 +266,50 @@ Execution trace: Dafny program verifier finished with 21 verified, 29 errors
+-------------------- Array.dfy --------------------
+Array.dfy(10,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Array.dfy(17,9): Error: RHS expression must be well defined
+Execution trace:
+ (0,0): anon0
+Array.dfy(24,10): Error: LHS expression must be well defined
+Execution trace:
+ (0,0): anon0
+Array.dfy(48,20): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Array.dfy(56,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Array.dfy(63,12): Error: assignment may update an array not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+Array.dfy(95,18): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Array.dfy(107,6): Error: insufficient reads clause to read array element
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+ (0,0): anon5_Then
+Array.dfy(115,6): Error: insufficient reads clause to read array element
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+ (0,0): anon5_Then
+Array.dfy(131,10): Error: assignment may update an array not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+Array.dfy(138,10): Error: assignment may update an array not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 22 verified, 11 errors
+
-------------------- Modules0.dfy --------------------
Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T
Modules0.dfy(13,7): Error: module T named among imports does not exist
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy new file mode 100644 index 00000000..928f2bc5 --- /dev/null +++ b/Test/dafny0/Array.dfy @@ -0,0 +1,156 @@ +class A {
+ method M() {
+ var y := new A[100];
+ y[5] := null;
+ }
+
+ method N0() {
+ var a;
+ if (a != null && 5 < |a|) {
+ a[5] := 12; // error: violates modifies clause
+ }
+ }
+
+ method N1(a: array<int>)
+ modifies a;
+ {
+ var b := |a|; // error: a may be null
+ }
+
+ method N2(a: array<int>)
+ requires a != null;
+ modifies a;
+ {
+ a[5] := 12; // error: index may be outside bounds
+ }
+
+ method N3(a: array<int>)
+ requires a != null && 5 < |a|;
+ modifies a;
+ ensures (forall i :: 0 <= i && i < |a| ==> a[i] == old(a[i]) || (i == 5 && a[i] == 12));
+ {
+ a[5] := 12; // all is good
+ }
+
+ var zz0: array<A>;
+ var zz1: array<B>;
+ method O() {
+ var zz2 := new A[25];
+ assert zz2 != zz0; // holds because zz2 is newly allocated
+ /****** These would be good things to be able to verify, but the current encoding is not up to the task
+ var o: object := zz0;
+ assert this != o; // holds because zz0 has a different type
+ if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {
+ o := zz1[1];
+ assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types
+ }
+ ******/
+ assert zz2[20] == null; // error: no reason that this must hold
+ }
+
+ var x: array<int>;
+ method P0()
+ modifies this;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // error: violates modifies clause
+ }
+ }
+ method P1()
+ modifies this`x;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // error: violates modifies clause
+ }
+ }
+ method P2()
+ modifies x;
+ {
+ if (x != null && 100 <= |x|) {
+ x[5] := 12; // fine
+ }
+ }
+
+ method Q() {
+ var y := new object[100];
+ y[5] := null;
+ y[0..] := null;
+ y[..83] := null;
+ y[0..|y|] := null;
+ }
+
+ method R() {
+ var y := new int[100];
+ y[55] := 80;
+ y[10..] := 25;
+ y[..83] := 30;
+ y[50..60] := 35;
+ y[55] := 90;
+
+ assert y[54] == 35;
+ assert y[55] == 90;
+ assert y[83] == 25;
+ assert y[8] == 30;
+ assert y[90] + y[91] + y[0] + 20 == |y|;
+ assert y[93] == 24; // error (it's 25)
+ }
+}
+
+class B { }
+
+// -------------------------------
+
+class ArrayTests {
+ function F0(a: array<int>): bool
+ {
+ a != null && 10 <= |a| &&
+ a[7] == 13 // error: reads on something outside reads clause
+ }
+
+ var b: array<int>;
+ function F1(): bool
+ reads this;
+ {
+ b != null && 10 <= |b| &&
+ b[7] == 13 // error: reads on something outside reads clause
+ }
+
+ function F2(a: array<int>): bool
+ reads this, b, a;
+ {
+ a != null && 10 <= |a| &&
+ a[7] == 13 // good
+ &&
+ b != null && 10 <= |b| &&
+ b[7] == 13 // good
+ }
+
+ method M0(a: array<int>)
+ requires a != null && 10 <= |a|;
+ {
+ a[7] := 13; // error: updates location not in modifies clause
+ }
+
+ method M1()
+ requires b != null && 10 <= |b|;
+ modifies this;
+ {
+ b[7] := 13; // error: updates location not in modifies clause
+ }
+
+ method M2()
+ modifies this;
+ {
+ var bb := new int[75];
+ b := bb; // fine
+ }
+
+ method M3(a: array<int>)
+ requires a != null && 10 <= |a|;
+ requires b != null && 10 <= |b|;
+ modifies this, b, a;
+ {
+ a[7] := 13; // good
+ b[7] := 13; // good
+ }
+}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index ba6c8e0c..4e3fab69 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -150,4 +150,14 @@ class Modifies { m.x := m.x + 1; // error: may violate modifies clause
}
}
+
+ method SetConstruction() {
+ var s := {1};
+ assert s != {};
+ if (*) {
+ assert s != {0,1};
+ } else {
+ assert s != {1,0};
+ }
+ }
}
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 1616234e..fe8644be 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -45,3 +45,13 @@ datatype ReverseOrder_TheCounterpart<T> { More(ReverseOrder_MutuallyRecursiveDataType<T>);
}
+// ---------------------
+
+class ArrayTests {
+ ghost method G(a: array<int>)
+ requires a != null && 10 <= |a|;
+ modifies a;
+ {
+ a[7] := 13; // error: array elements are not ghost locations
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index fd90e479..c43ea782 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -17,7 +17,7 @@ for %%f in (BQueue.bpl) do ( %BPLEXE% %* %%f
)
-for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy
+for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy Array.dfy
Modules0.dfy Modules1.dfy BadFunction.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
diff --git a/Test/vacid0/Answer b/Test/vacid0/Answer new file mode 100644 index 00000000..6f270f92 --- /dev/null +++ b/Test/vacid0/Answer @@ -0,0 +1,12 @@ +
+-------------------- LazyInitArray.dfy --------------------
+
+Dafny program verifier finished with 7 verified, 0 errors
+
+-------------------- SparseArray.dfy --------------------
+
+Dafny program verifier finished with 9 verified, 0 errors
+
+-------------------- Composite.dfy --------------------
+
+Dafny program verifier finished with 14 verified, 0 errors
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy new file mode 100644 index 00000000..28074c7b --- /dev/null +++ b/Test/vacid0/Composite.dfy @@ -0,0 +1,160 @@ +class Composite {
+ var left: Composite;
+ var right: Composite;
+ var parent: Composite;
+ var val: int;
+ var sum: int;
+
+ function Valid(S: set<Composite>): bool
+ reads this, parent, left, right;
+ {
+ this in S &&
+ (parent != null ==> parent in S && (parent.left == this || parent.right == this)) &&
+ (left != null ==> left in S && left.parent == this && left != right) &&
+ (right != null ==> right in S && right.parent == this && left != right) &&
+ sum == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum)
+ }
+
+ function Acyclic(S: set<Composite>): bool
+ reads S;
+ {
+ this in S &&
+ (parent != null ==> parent.Acyclic(S - {this}))
+ }
+
+ method Init(x: int)
+ modifies this;
+ ensures Valid({this}) && Acyclic({this}) && val == x && parent == null;
+ {
+ parent := null;
+ left := null;
+ right := null;
+ val := x;
+ sum := val;
+ }
+
+ method Update(x: int, ghost S: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ modifies S;
+ ensures (forall c :: c in S ==> c.Valid(S));
+ ensures (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent));
+ ensures (forall c :: c in S && c != this ==> c.val == old(c.val));
+ ensures val == x;
+ {
+ var delta := x - val;
+ val := x;
+ call Adjust(delta, S, S);
+ }
+
+ method Add(ghost S: set<Composite>, child: Composite, ghost U: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ requires child != null && child in U;
+ requires (forall c :: c in U ==> c != null && c.Valid(U));
+ requires S !! U;
+ requires left == null || right == null;
+ requires child.parent == null;
+ // modifies only one of this.left and this.right, and child.parent, and various sum fields:
+ modifies S, child;
+ ensures child.left == old(child.left) && child.right == old(child.right) && child.val == old(child.val);
+ ensures (forall c :: c in S && c != this ==> c.left == old(c.left) && c.right == old(c.right));
+ ensures old(left) != null ==> left == old(left);
+ ensures old(right) != null ==> right == old(right);
+ ensures (forall c :: c in S ==> c.parent == old(c.parent) && c.val == old(c.val));
+ // sets child.parent to this:
+ ensures child.parent == this;
+ // leaves everything in S+U valid:
+ ensures (forall c :: c in S+U ==> c.Valid(S+U));
+ {
+ if (left == null) {
+ left := child;
+ } else {
+ right := child;
+ }
+ child.parent := this;
+ call Adjust(child.sum, S, S+U);
+ }
+
+ method Dislodge(ghost S: set<Composite>)
+ requires this in S && Acyclic(S);
+ requires (forall c :: c in S ==> c != null && c.Valid(S));
+ modifies S;
+ ensures (forall c :: c in S ==> c.Valid(S));
+ ensures (forall c :: c in S ==> c.val == old(c.val));
+ ensures (forall c :: c in S && c != this ==> c.parent == old(c.parent));
+ ensures (forall c :: c in S ==> c.left == old(c.left) || (old(c.left) == this && c.left == null));
+ ensures (forall c :: c in S ==> c.right == old(c.right) || (old(c.right) == this && c.right == null));
+ ensures Acyclic({this});
+ {
+ var p := parent;
+ parent := null;
+ if (p != null) {
+ assert (p.left == this) != (p.right == this);
+ if (p.left == this) {
+ p.left := null;
+ } else {
+ p.right := null;
+ }
+ var delta := -sum;
+ call p.Adjust(delta, S - {this}, S);
+ }
+ }
+
+ /*private*/ method Adjust(delta: int, ghost U: set<Composite>, ghost S: set<Composite>)
+ requires U <= S && Acyclic(U);
+ // everything else is valid:
+ requires (forall c :: c in S && c != this ==> c != null && c.Valid(S));
+ // this is almost valid:
+ requires parent != null ==> parent in S && (parent.left == this || parent.right == this);
+ requires left != null ==> left in S && left.parent == this && left != right;
+ requires right != null ==> right in S && right.parent == this && left != right;
+ // ... except that sum needs to be adjusted by delta:
+ requires sum + delta == val + (if left == null then 0 else left.sum) + (if right == null then 0 else right.sum);
+ // modifies sum fields in U:
+ modifies U`sum;
+ // everything is valid, including this:
+ ensures (forall c :: c in S ==> c.Valid(S));
+ {
+ var p := this;
+ ghost var T := U;
+ while (p != null)
+ invariant T <= U;
+ invariant p == null || p.Acyclic(T);
+ invariant (forall c :: c in S && c != p ==> c.Valid(S));
+ invariant p != null ==> p.sum + delta == p.val + (if p.left == null then 0 else p.left.sum) + (if p.right == null then 0 else p.right.sum);
+ invariant (forall c :: c in S ==> c.left == old(c.left) && c.right == old(c.right) && c.parent == old(c.parent) && c.val == old(c.val));
+ decreases T;
+ {
+ p.sum := p.sum + delta;
+ T := T - {p};
+ p := p.parent;
+ }
+ }
+}
+
+method Main()
+{
+ var c0 := new Composite;
+ call c0.Init(57);
+
+ var c1 := new Composite;
+ call c1.Init(12);
+ call c0.Add({c0}, c1, {c1});
+
+ var c2 := new Composite;
+ call c2.Init(48);
+
+ var c3 := new Composite;
+ call c3.Init(48);
+ call c2.Add({c2}, c3, {c3});
+ call c0.Add({c0,c1}, c2, {c2,c3});
+
+ ghost var S := {c0, c1, c2, c3};
+ call c1.Update(100, S);
+ call c2.Update(102, S);
+
+ call c2.Dislodge(S);
+ call c2.Update(496, S);
+ call c0.Update(0, S);
+}
diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy new file mode 100644 index 00000000..6ae00e24 --- /dev/null +++ b/Test/vacid0/LazyInitArray.dfy @@ -0,0 +1,105 @@ +class LazyInitArray<T> {
+ ghost var Contents: seq<T>;
+ var Zero: T;
+ /*private*/ var a: array<T>;
+ /*private*/ var b: array<int>;
+ /*private*/ var c: array<int>;
+ /*private*/ var n: int;
+ /*private*/ ghost var d: seq<int>;
+ /*private*/ ghost var e: seq<int>;
+ function Valid(): bool
+ reads this, a, b, c;
+ {
+ a != null && b != null && c != null &&
+ |a| == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
+ |b| == |Contents| &&
+ |c| == |Contents| &&
+ b != c &&
+ 0 <= n && n <= |c| &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ ((exists j :: 0 <= j && j < n && c[j] == i)
+ <==>
+ 0 <= b[i] && b[i] < n && c[b[i]] == i)) &&
+ // The idea behind d and e is the following:
+ // * d is a permutation of the first |Contents| natural numbers
+ // * e describes which permutation d is
+ // * c[..n] == d[..n]
+ |d| == |Contents| &&
+ |e| == |Contents| &&
+ (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&
+ (forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&
+ (forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&
+ (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)
+ }
+
+ method Init(N: int, zero: T)
+ requires 0 <= N;
+ modifies this, a, b, c;
+ ensures Valid();
+ ensures |Contents| == N && Zero == zero;
+ ensures (forall x :: x in Contents ==> x == zero);
+ {
+ var aa := new T[N+1]; a := aa;
+ var ii := new int[N]; b := ii;
+ ii := new int[N]; c := ii;
+ n := 0;
+
+ // initialize ghost variable Contents to a sequence of length N containing only zero's,
+ // and ghost variables d and e to be the identity sequences of length N
+ ghost var s := [];
+ ghost var id := [];
+ ghost var k := 0;
+ while (k < N)
+ invariant k <= N;
+ invariant |s| == k && (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
+ invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
+ {
+ s := s + [zero];
+ id := id + [k];
+ k := k + 1;
+ }
+
+ d := id;
+ e := id;
+ Zero := zero;
+ Contents := s;
+ }
+
+ method Get(i: int) returns (x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ ensures x == Contents[i];
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ x := a[i];
+ } else {
+ x := Zero;
+ }
+ }
+
+ method Set(i: int, x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ modifies this, a, b, c;
+ ensures Valid();
+ ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];
+ ensures Zero == old(Zero);
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ } else {
+ assert n <= e[i];
+ b[i] := n;
+ c[n] := i;
+ ghost var t := d[n];
+ ghost var k := e[i];
+ d := d[n := i][k := t];
+ e := e[i := n][t := k];
+ n := n + 1;
+ }
+
+ a[i] := x;
+ Contents := Contents[i := x];
+ }
+}
diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy new file mode 100644 index 00000000..da1f63bb --- /dev/null +++ b/Test/vacid0/SparseArray.dfy @@ -0,0 +1,120 @@ +class SparseArray<T> {
+ ghost var Contents: seq<T>;
+ var zero: T;
+ /*private*/ var a: seq<T>; // should really be an array
+ /*private*/ var b: seq<int>; // should really be an array
+ /*private*/ var c: seq<int>; // should really be an array
+ /*private*/ var n: int;
+ /*private*/ ghost var d: seq<int>; // would be better as an array
+ /*private*/ ghost var e: seq<int>; // would be better as an array
+ function Valid(): bool
+ reads this;
+ {
+ |a| == |Contents| &&
+ |b| == |Contents| &&
+ |c| == |Contents| &&
+ 0 <= n && n <= |c| &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else zero)) &&
+ (forall i :: 0 <= i && i < |Contents| ==>
+ (i in c[..n] <==> 0 <= b[i] && b[i] < n && c[b[i]] == i)) &&
+ // The idea behind d and e is the following:
+ // * d is a permutation of the first |Contents| natural numbers
+ // * e describes which permutation d is
+ // * c[..n] == d[..n]
+ |d| == |Contents| &&
+ |e| == |Contents| &&
+ (forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&
+ (forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&
+ (forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&
+ (forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)
+ }
+
+ method Init(N: int, zero: T)
+ requires 0 <= N;
+ modifies this;
+ ensures Valid();
+ ensures |Contents| == N && this.zero == zero;
+ ensures (forall x :: x in Contents ==> x == zero);
+ {
+ var aa;
+ var ii;
+ call aa := AllocateArray(N); this.a := aa;
+ call ii := AllocateArray(N); this.b := ii;
+ call ii := AllocateArray(N); this.c := ii;
+ this.n := 0;
+
+ // initialize ghost variable Contents to a sequence of length N containing only zero's,
+ // and ghost variables d and e to be the identity sequences of length N
+ ghost var s := [];
+ ghost var id := [];
+ ghost var k := 0;
+ while (k < N)
+ invariant k <= N;
+ invariant |s| == k;
+ // TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero);
+ invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
+ invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
+ decreases N - k;
+ {
+ s := s + [zero];
+ id := id + [k];
+ k := k + 1;
+ }
+
+ this.zero := zero;
+ this.Contents := s;
+ this.d := id;
+ this.e := id;
+ }
+ method Get(i: int) returns (x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ ensures x == Contents[i];
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ x := a[i];
+ } else {
+ x := zero;
+ }
+ }
+ method Set(i: int, x: T)
+ requires Valid();
+ requires 0 <= i && i < |Contents|;
+ modifies this;
+ ensures Valid();
+ ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];
+ ensures zero == old(zero);
+ {
+ if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
+ } else {
+ assert n <= e[i];
+ b := b[i := n];
+ c := c[n := i];
+ ghost var t := d[n];
+ ghost var k := e[i];
+ d := d[n := i][k := t];
+ e := e[i := n][t := k];
+ n := n + 1;
+ }
+ a := a[i := x];
+ Contents := Contents[i := x];
+ }
+
+ /* The following method is here only to simulate support of arrays in Dafny */
+ /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+ requires 0 <= n;
+ ensures |arr| == n;
+ {
+ arr := [];
+ var i := 0;
+ while (i < n)
+ invariant i <= n && |arr| == i;
+ decreases n - i;
+ {
+ var g: G;
+ arr := arr + [g];
+ i := i + 1;
+ }
+ }
+}
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat new file mode 100644 index 00000000..d6af7b71 --- /dev/null +++ b/Test/vacid0/runtest.bat @@ -0,0 +1,12 @@ +@echo off
+setlocal
+
+set BOOGIEDIR=..\..\Binaries
+set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %DAFNY_EXE% /compile:0 %* %%f
+)
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 7b5de59a..20f4477b 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -39,7 +39,7 @@ "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"
"old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
- `(,(dafny-regexp-opt '("bool" "int" "object" "set" "seq")) . font-lock-type-face)
+ `(,(dafny-regexp-opt '("array" "bool" "int" "object" "set" "seq")) . font-lock-type-face)
)
"Minimal highlighting for Dafny mode")
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 1f891a71..dd44665a 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -5,7 +5,7 @@ \usepackage{listings}
\lstdefinelanguage{dafny}{
- morekeywords={class,datatype,bool,int,object,set,seq,%
+ morekeywords={class,datatype,bool,int,object,set,seq,array,%
function,unlimited,
ghost,var,static,
method,returns,module,imports,in,
|