diff options
| author |  leino <unknown> | 2014-12-12 20:46:48 -0800 |
|---|---|---|
| committer | leino <unknown> | 2014-12-12 20:46:48 -0800 |
| commit | 91c4d57eb84d5d15e011902a1da1b70131e5a222 (patch) | |
| tree | 6794bafdc71f6bc31c8d09496c3435658bbfc144 | |
| parent | 62a3e97eb61cbee0d523297ccad1f2d3bcf871c3 (diff) | |
Language change: All functions and methods declared lexically outside any class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
55 files changed, 946 insertions, 859 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index f1f203cb..cb41a75f 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -613,13 +613,13 @@ namespace Microsoft.Dafny }
if (f is Predicate) {
- return new Predicate(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, formals,
+ return new Predicate(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals,
req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), null);
} else if (f is CoPredicate) {
- return new CoPredicate(Tok(f.tok), newName, f.IsStatic, tps, formals,
+ return new CoPredicate(Tok(f.tok), newName, f.HasStaticKeyword, tps, formals,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
} else {
- return new Function(Tok(f.tok), newName, f.IsStatic, f.IsGhost, tps, formals, CloneType(f.ResultType),
+ return new Function(Tok(f.tok), newName, f.HasStaticKeyword, f.IsGhost, tps, formals, CloneType(f.ResultType),
req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);
}
}
@@ -640,13 +640,13 @@ namespace Microsoft.Dafny return new Constructor(Tok(m.tok), m.Name, tps, ins,
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else if (m is CoLemma) {
- return new CoLemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ return new CoLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else if (m is Lemma) {
- return new Lemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ return new Lemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else {
- return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
+ return new Method(Tok(m.tok), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
}
}
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index a716da96..c7ee28ac 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -486,7 +486,7 @@ Dafny | OtherTypeDecl<defaultModule, out td> (. defaultModule.TopLevelDecls.Add(td); .)
| IteratorDecl<defaultModule, out iter> (. defaultModule.TopLevelDecls.Add(iter); .)
| TraitDecl<defaultModule, out trait> (. defaultModule.TopLevelDecls.Add(trait); .)
- | ClassMemberDecl<membersDefaultClass, false>
+ | ClassMemberDecl<membersDefaultClass, false, true>
}
(. // find the default class in the default module, then append membersDefaultClass to its member list
DefaultClassDecl defaultClass = null;
@@ -529,7 +529,7 @@ SubModuleDecl<ModuleDefinition parent, out ModuleDecl submodule> | NewtypeDecl<module, out td> (. module.TopLevelDecls.Add(td); .)
| OtherTypeDecl<module, out td> (. module.TopLevelDecls.Add(td); .)
| IteratorDecl<module, out iter> (. module.TopLevelDecls.Add(iter); .)
- | ClassMemberDecl<namedModuleDefaultClassMembers, false>
+ | ClassMemberDecl<namedModuleDefaultClassMembers, false, true>
}
"}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
@@ -587,7 +587,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c> {"," Type<out trait> (. traits.Add(trait); .) }
]
"{" (. bodyStart = t; .)
- { ClassMemberDecl<members, true>
+ { ClassMemberDecl<members, true, false>
}
"}"
(. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);
@@ -611,7 +611,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c> NoUSIdent<out id>
[ GenericParameters<typeArgs> ]
"{" (. bodyStart = t; .)
- { ClassMemberDecl<members, true>
+ { ClassMemberDecl<members, true, false>
}
"}"
(. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
@@ -620,18 +620,34 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c> .)
.
-ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
+ClassMemberDecl<.List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
+ IToken staticToken = null;
.)
{ "ghost" (. mmod.IsGhost = true; .)
- | "static" (. mmod.IsStatic = true; .)
+ | "static" (. mmod.IsStatic = true; staticToken = t; .)
}
- ( FieldDecl<mmod, mm>
- | FunctionDecl<mmod, out f> (. mm.Add(f); .)
- | MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
+ ( (. if (moduleLevelDecl) {
+ SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration");
+ mmod.IsStatic = false;
+ }
+ .)
+ FieldDecl<mmod, mm>
+ | (. if (moduleLevelDecl && staticToken != null) {
+ errors.Warning(staticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here");
+ mmod.IsStatic = false;
+ }
+ .)
+ FunctionDecl<mmod, out f> (. mm.Add(f); .)
+ | (. if (moduleLevelDecl && staticToken != null) {
+ errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
+ mmod.IsStatic = false;
+ }
+ .)
+ MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
)
.
DatatypeDecl<ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt>
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 9277a954..1593aeb5 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2180,16 +2180,21 @@ namespace Microsoft.Dafny { }
public abstract class MemberDecl : Declaration {
- public readonly bool IsStatic;
+ public readonly bool HasStaticKeyword;
+ public bool IsStatic {
+ get {
+ return HasStaticKeyword || (EnclosingClass is ClassDecl && ((ClassDecl)EnclosingClass).IsDefaultClass);
+ }
+ }
public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
public MemberDecl RefinementBase; // filled in during the pre-resolution refinement transformation; null if the member is new here
public bool Inherited;
- public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
+ public MemberDecl(IToken tok, string name, bool hasStaticKeyword, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
- IsStatic = isStatic;
+ HasStaticKeyword = hasStaticKeyword;
IsGhost = isGhost;
}
/// <summary>
@@ -2803,11 +2808,11 @@ namespace Microsoft.Dafny { /// <summary>
/// Note, functions are "ghost" by default; a non-ghost function is called a "function method".
/// </summary>
- public Function(IToken tok, string name, bool isStatic, bool isGhost,
+ public Function(IToken tok, string name, bool hasStaticKeyword, bool isGhost,
List<TypeParameter> typeArgs, List<Formal> formals, Type resultType,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, isGhost, attributes) {
+ : base(tok, name, hasStaticKeyword, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -2853,11 +2858,11 @@ namespace Microsoft.Dafny { Extension // this predicate extends the definition of a predicate with a body in a module being refined
}
public readonly BodyOriginKind BodyOrigin;
- public Predicate(IToken tok, string name, bool isStatic, bool isGhost,
+ public Predicate(IToken tok, string name, bool hasStaticKeyword, bool isGhost,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, BodyOriginKind bodyOrigin, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {
+ : base(tok, name, hasStaticKeyword, isGhost, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);
BodyOrigin = bodyOrigin;
}
@@ -2870,11 +2875,11 @@ namespace Microsoft.Dafny { {
public readonly Formal K;
public readonly CoPredicate Co;
- public PrefixPredicate(IToken tok, string name, bool isStatic,
+ public PrefixPredicate(IToken tok, string name, bool hasStaticKeyword,
List<TypeParameter> typeArgs, Formal k, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, Attributes attributes, CoPredicate coPred)
- : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {
+ : base(tok, name, hasStaticKeyword, true, typeArgs, formals, new BoolType(), req, reads, ens, decreases, body, attributes, null) {
Contract.Requires(k != null);
Contract.Requires(coPred != null);
Contract.Requires(formals != null && 1 <= formals.Count && formals[0] == k);
@@ -2888,11 +2893,11 @@ namespace Microsoft.Dafny { public readonly List<FunctionCallExpr> Uses = new List<FunctionCallExpr>(); // filled in during resolution, used by verifier
public PrefixPredicate PrefixPredicate; // filled in during resolution (name registration)
- public CoPredicate(IToken tok, string name, bool isStatic,
+ public CoPredicate(IToken tok, string name, bool hasStaticKeyword,
List<TypeParameter> typeArgs, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens,
Expression body, Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, true, typeArgs, formals, new BoolType(),
+ : base(tok, name, hasStaticKeyword, true, typeArgs, formals, new BoolType(),
req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, attributes, signatureEllipsis) {
}
@@ -2956,7 +2961,7 @@ namespace Microsoft.Dafny { }
public Method(IToken tok, string name,
- bool isStatic, bool isGhost,
+ bool hasStaticKeyword, bool isGhost,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins, [Captured] List<Formal> outs,
[Captured] List<MaybeFreeExpression> req, [Captured] Specification<FrameExpression> mod,
@@ -2964,7 +2969,7 @@ namespace Microsoft.Dafny { [Captured] Specification<Expression> decreases,
[Captured] BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, isGhost, attributes) {
+ : base(tok, name, hasStaticKeyword, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
@@ -3016,7 +3021,7 @@ namespace Microsoft.Dafny { public class Lemma : Method
{
public Lemma(IToken tok, string name,
- bool isStatic,
+ bool hasStaticKeyword,
[Captured] List<TypeParameter> typeArgs,
[Captured] List<Formal> ins, [Captured] List<Formal> outs,
[Captured] List<MaybeFreeExpression> req, [Captured] Specification<FrameExpression> mod,
@@ -3024,7 +3029,7 @@ namespace Microsoft.Dafny { [Captured] Specification<Expression> decreases,
[Captured] BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+ : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
}
}
@@ -3063,11 +3068,11 @@ namespace Microsoft.Dafny { {
public readonly Formal K;
public readonly CoLemma Co;
- public PrefixLemma(IToken tok, string name, bool isStatic,
+ public PrefixLemma(IToken tok, string name, bool hasStaticKeyword,
List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,
List<MaybeFreeExpression> req, Specification<FrameExpression> mod, List<MaybeFreeExpression> ens, Specification<Expression> decreases,
BlockStmt body, Attributes attributes, CoLemma co)
- : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {
+ : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {
Contract.Requires(k != null);
Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k);
Contract.Requires(co != null);
@@ -3081,7 +3086,7 @@ namespace Microsoft.Dafny { public PrefixLemma PrefixLemma; // filled in during resolution (name registration)
public CoLemma(IToken tok, string name,
- bool isStatic,
+ bool hasStaticKeyword,
List<TypeParameter> typeArgs,
List<Formal> ins, [Captured] List<Formal> outs,
List<MaybeFreeExpression> req, [Captured] Specification<FrameExpression> mod,
@@ -3089,7 +3094,7 @@ namespace Microsoft.Dafny { Specification<Expression> decreases,
BlockStmt body,
Attributes attributes, IToken signatureEllipsis)
- : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+ : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 43df66c4..42627024 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -547,7 +547,7 @@ bool IsType(ref IToken pt) { break;
}
case 64: case 65: case 68: case 74: case 75: case 76: case 77: case 78: case 82: case 83: case 84: {
- ClassMemberDecl(membersDefaultClass, false);
+ ClassMemberDecl(membersDefaultClass, false, true);
break;
}
}
@@ -634,7 +634,7 @@ bool IsType(ref IToken pt) { break;
}
case 64: case 65: case 68: case 74: case 75: case 76: case 77: case 78: case 82: case 83: case 84: {
- ClassMemberDecl(namedModuleDefaultClassMembers, false);
+ ClassMemberDecl(namedModuleDefaultClassMembers, false, true);
break;
}
}
@@ -711,7 +711,7 @@ bool IsType(ref IToken pt) { Expect(38);
bodyStart = t;
while (StartOf(2)) {
- ClassMemberDecl(members, true);
+ ClassMemberDecl(members, true, false);
}
Expect(39);
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);
@@ -920,7 +920,7 @@ bool IsType(ref IToken pt) { Expect(38);
bodyStart = t;
while (StartOf(2)) {
- ClassMemberDecl(members, true);
+ ClassMemberDecl(members, true, false);
}
Expect(39);
trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
@@ -929,11 +929,12 @@ bool IsType(ref IToken pt) { }
- void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors) {
+ void ClassMemberDecl(List<MemberDecl> mm, bool allowConstructors, bool moduleLevelDecl) {
Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
+ IToken staticToken = null;
while (la.kind == 64 || la.kind == 65) {
if (la.kind == 64) {
@@ -941,15 +942,30 @@ bool IsType(ref IToken pt) { mmod.IsGhost = true;
} else {
Get();
- mmod.IsStatic = true;
+ mmod.IsStatic = true; staticToken = t;
}
}
if (la.kind == 68) {
+ if (moduleLevelDecl) {
+ SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration");
+ mmod.IsStatic = false;
+ }
+
FieldDecl(mmod, mm);
} else if (la.kind == 82 || la.kind == 83 || la.kind == 84) {
+ if (moduleLevelDecl && staticToken != null) {
+ errors.Warning(staticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here");
+ mmod.IsStatic = false;
+ }
+
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (StartOf(6)) {
+ if (moduleLevelDecl && staticToken != null) {
+ errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
+ mmod.IsStatic = false;
+ }
+
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
} else SynErr(146);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index b5cc3b2f..9a27c080 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -480,7 +480,7 @@ namespace Microsoft.Dafny { var isPredicate = f is Predicate || f is PrefixPredicate;
Indent(indent);
string k = isPredicate ? "predicate" : f is CoPredicate ? "copredicate" : "function";
- if (f.IsStatic) { k = "static " + k; }
+ if (f.HasStaticKeyword) { k = "static " + k; }
if (!f.IsGhost) { k += " method"; }
PrintClassMethodHelper(k, f.Attributes, f.Name, f.TypeArgs);
if (f.SignatureIsOmitted) {
@@ -549,7 +549,7 @@ namespace Microsoft.Dafny { if (PrintModeSkipFunctionOrMethod(method.IsGhost, method.Attributes, method.Name)) { return; }
Indent(indent);
string k = method is Constructor ? "constructor" : method is CoLemma ? "colemma" : method is Lemma ? "lemma" : "method";
- if (method.IsStatic) { k = "static " + k; }
+ if (method.HasStaticKeyword) { k = "static " + k; }
if (method.IsGhost && !(method is Lemma) && !(method is CoLemma)) { k = "ghost " + k; }
string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;
PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index ef59d00a..8234846e 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -309,8 +309,8 @@ namespace Microsoft.Dafny foreach (var m in d.Members) {
MemberDecl newMem;
if (map.TryGetValue(m.Name, out newMem)) {
- if (m.IsStatic != newMem.IsStatic) {
- reporter.Error(newMem, "member {0} must {1}", m.Name, m.IsStatic? "be static" : "not be static");
+ if (m.HasStaticKeyword != newMem.HasStaticKeyword) {
+ reporter.Error(newMem, "member {0} must {1}", m.Name, m.HasStaticKeyword ? "be static" : "not be static");
}
if (m is Field) {
if (newMem is Field) {
@@ -545,13 +545,13 @@ namespace Microsoft.Dafny }
if (f is Predicate) {
- return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, formals,
+ return new Predicate(tok, f.Name, f.HasStaticKeyword, isGhost, tps, formals,
req, reads, ens, decreases, body, bodyOrigin, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
} else if (f is CoPredicate) {
- return new CoPredicate(tok, f.Name, f.IsStatic, tps, formals,
+ return new CoPredicate(tok, f.Name, f.HasStaticKeyword, tps, formals,
req, reads, ens, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
} else {
- return new Function(tok, f.Name, f.IsStatic, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),
+ return new Function(tok, f.Name, f.HasStaticKeyword, isGhost, tps, formals, refinementCloner.CloneType(f.ResultType),
req, reads, ens, decreases, body, refinementCloner.MergeAttributes(f.Attributes, moreAttributes), null);
}
}
@@ -579,13 +579,13 @@ namespace Microsoft.Dafny return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
} else if (m is CoLemma) {
- return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
+ return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
} else if (m is Lemma) {
- return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
+ return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
} else {
- return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
+ return new Method(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),
req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);
}
}
@@ -705,7 +705,7 @@ namespace Microsoft.Dafny reporter.Error(f.Decreases.Expressions[0].tok, "decreases clause on refining {0} not supported", s);
}
- if (prevFunction.IsStatic != f.IsStatic) {
+ if (prevFunction.HasStaticKeyword != f.HasStaticKeyword) {
reporter.Error(f, "a function in a refining module cannot be changed from static to non-static or vice versa: {0}", f.Name);
}
if (!prevFunction.IsGhost && f.IsGhost) {
@@ -766,7 +766,7 @@ namespace Microsoft.Dafny }
decreases = m.Decreases;
}
- if (prevMethod.IsStatic != m.IsStatic) {
+ if (prevMethod.HasStaticKeyword != m.HasStaticKeyword) {
reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);
}
if (prevMethod.IsGhost && !m.IsGhost) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 8c72d276..483ff08f 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -122,7 +122,7 @@ namespace Microsoft.Dafny readonly MemberDecl A;
readonly MemberDecl B;
public AmbiguousMemberDecl(ModuleDefinition m, MemberDecl a, MemberDecl b)
- : base(a.tok, a.Name + "/" + b.Name, a.IsStatic, a.IsGhost, null) {
+ : base(a.tok, a.Name + "/" + b.Name, true, a.IsGhost, null) {
A = a;
B = b;
}
@@ -970,7 +970,7 @@ namespace Microsoft.Dafny List<TypeParameter> tyvars = cop.TypeArgs.ConvertAll(cloner.CloneTypeParam);
// create prefix predicate
- cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.IsStatic,
+ cop.PrefixPredicate = new PrefixPredicate(cop.tok, extraName, cop.HasStaticKeyword,
tyvars, k, formals,
cop.Req.ConvertAll(cloner.CloneExpr),
cop.Reads.ConvertAll(cloner.CloneFrameExpr),
@@ -991,7 +991,7 @@ namespace Microsoft.Dafny decr.Add(new IdentifierExpr(com.tok, k.Name));
decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));
// Create prefix lemma. Note that the body is not cloned, but simply shared.
- com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.IsStatic,
+ com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.HasStaticKeyword,
com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),
com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod),
new List<MaybeFreeExpression>(), // Note, the postconditions are filled in after the colemma's postconditions have been resolved
@@ -1018,9 +1018,10 @@ namespace Microsoft.Dafny {
Error(cl, "a trait is not allowed to declare a constructor");
}
- if (cl.IsDefaultClass) {
+ if (cl.IsDefaultClass) {
foreach (MemberDecl m in cl.Members) {
- if (m.IsStatic && (m is Function || m is Method)) {
+ Contract.Assert(!m.HasStaticKeyword); // note, the IsStatic value isn't available yet; when it becomes available, we expect it will have the value 'true'
+ if (m is Function || m is Method) {
sig.StaticMembers[m.Name] = m;
}
}
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 9356c6a6..9fba04e6 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -546,7 +546,7 @@ namespace Microsoft.Dafny // Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body
Attributes lemma_attrs = new Attributes("axiom", new List<Expression>(), null);
- var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.IsStatic, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
+ var reveal = new Lemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<MaybeFreeExpression>(),
new Specification<FrameExpression>(new List<FrameExpression>(), null), newEnsuresList,
new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
newDecls.Add(reveal);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 293dfdad..e836eca1 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -5343,16 +5343,18 @@ namespace Microsoft.Dafny { var fromArrowType = enclosingArrow != null;
Func<List<Bpl.Expr>, List<Bpl.Expr>> SnocSelf = x => x;
- Expression selfExpr = null;
- Dictionary<IVariable, Expression> rhs_dict = null;
- if (!f.IsStatic) {
+ Expression selfExpr;
+ Dictionary<IVariable, Expression> rhs_dict = new Dictionary<IVariable, Expression>();
+ if (f.IsStatic) {
+ // the value of 'selfExpr' won't be used, but it has to be non-null to satisfy the precondition of the call to InRWClause below
+ selfExpr = new ThisExpr(Token.NoToken);
+ } else {
var selfTy = fromArrowType ? predef.HandleType : predef.RefType;
var self = BplBoundVar("$self", selfTy, vars);
formals.Add(BplFormalVar(null, selfTy, true));
SnocSelf = xs => Snoc(xs, self);
selfExpr = new BoogieWrapper(self, fromArrowType ? f.Type : new ObjectType());
// ^ is this an ok type for this wrapper?
- rhs_dict = new Dictionary<IVariable, Expression>();
}
// F#Handle(Ty, .., Ty, LayerType, ref) : HandleType
@@ -5369,9 +5371,7 @@ namespace Microsoft.Dafny { lhs_args.Add(fe);
var be = UnboxIfBoxed(fe, fm.Type);
rhs_args.Add(be);
- if (rhs_dict != null) {
- rhs_dict[fm] = new BoogieWrapper(be, fm.Type);
- }
+ rhs_dict[fm] = new BoogieWrapper(be, fm.Type);
}
var h = BplBoundVar("$heap", predef.HeapType, vars);
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 23c25733..274d86de 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -49,7 +49,7 @@ method M(N: int, A: array<int>, B: array<int>) assert forall j,k :: 0 <= j < k < N ==> B[j] != B[k];
}
-static function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
+function inImage(i: int): bool { true } // this function is used to trigger the surjective quantification
method Main()
{
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy index 61bb2e3a..814e9067 100644 --- a/Test/VSComp2010/Problem3-FindZero.dfy +++ b/Test/VSComp2010/Problem3-FindZero.dfy @@ -56,7 +56,7 @@ class Node { }
}
-static method Search(ll: Node) returns (r: int)
+method Search(ll: Node) returns (r: int)
requires ll == null || ll.Valid();
ensures ll == null ==> r == 0;
ensures ll != null ==>
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 21fcc053..487dfdf2 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -47,7 +47,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) // Given a board, this function says whether or not the queen placed in column 'pos'
// is consistent with the queens placed in columns to its left.
-static function method IsConsistent(board: seq<int>, pos: int): bool
+function method IsConsistent(board: seq<int>, pos: int): bool
{
0 <= pos && pos < |board| &&
(forall q :: 0 <= q && q < pos ==>
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 9e0d3b63..99e8298e 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -270,44 +270,44 @@ module Matches { // Make sure :autoReq works with static functions
module StaticTest {
- static function f(x:int) : bool
+ function f(x:int) : bool
requires x > 3;
{
x > 7
}
- static function {:autoReq} g(z:int) : bool
+ function {:autoReq} g(z:int) : bool
requires f(z);
{
true
}
// Should succeed thanks to auto-generation based on f's requirements
- static function {:autoReq} h(y:int) : bool
+ function {:autoReq} h(y:int) : bool
{
g(y)
}
- static predicate IsEven(x:int)
+ predicate IsEven(x:int)
- static function EvenDoubler(x:int) : int
+ function EvenDoubler(x:int) : int
requires IsEven(x);
// Should succeed thanks to auto-generated requirement of IsEven
- static function {:autoReq} test(y:int) : int
+ function {:autoReq} test(y:int) : int
{
EvenDoubler(y)
}
}
module OpaqueTest {
- static function bar(x:int) : int
+ function bar(x:int) : int
requires x>7;
{
x-2
}
- static function {:autoReq} {:opaque} foo(x:int) : int
+ function {:autoReq} {:opaque} foo(x:int) : int
{
bar(x)
}
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 57a593fe..dfa99dd6 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -2,32 +2,34 @@ // RUN: %diff "%s.expect" "%t"
module TestModule {
- copredicate P(b: bool)
- {
- !b && Q(null)
- }
+ class TestClass {
+ copredicate P(b: bool)
+ {
+ !b && Q(null)
+ }
- copredicate Q(a: array<int>)
- {
- a == null && P(true)
- }
+ copredicate Q(a: array<int>)
+ {
+ a == null && P(true)
+ }
- copredicate S(d: set<int>)
- {
- this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
- this.S#[5](d) &&
- S#[5](d) &&
- S#[_k](d) // error: _k is not an identifier in scope
- }
+ copredicate S(d: set<int>)
+ {
+ this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ Undeclared#[5](d) && // error: 'Undeclared#' is undeclared
+ this.S#[5](d) &&
+ S#[5](d) &&
+ S#[_k](d) // error: _k is not an identifier in scope
+ }
- colemma CM(d: set<int>)
- {
- var b;
- b := this.S#[5](d);
- b := S#[5](d);
- this.CM#[5](d);
- CM#[5](d);
+ colemma CM(d: set<int>)
+ {
+ var b;
+ b := this.S#[5](d);
+ b := S#[5](d);
+ this.CM#[5](d);
+ CM#[5](d);
+ }
}
}
@@ -63,19 +65,21 @@ module GhostCheck2 { }
module Mojul0 {
- copredicate D()
- reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
- {
- true
- }
+ class MyClass {
+ copredicate D()
+ reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT?
+ {
+ true
+ }
- copredicate NoEnsuresPlease(m: nat)
- ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
- {
- m < 75
- }
+ copredicate NoEnsuresPlease(m: nat)
+ ensures NoEnsuresPlease(m) ==> m < 100; // error: a copredicate is not allowed to have an 'ensures' clause
+ {
+ m < 75
+ }
- // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
+ // Note, 'decreases' clauses are also disallowed on copredicates, but the parser takes care of that
+ }
}
module Mojul1 {
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 45d1e598..0eff4874 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -1,25 +1,25 @@ -CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default
-CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared#
-CoResolution.dfy(21,7): Error: unresolved identifier: _k
-CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
-CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause
-CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause
-CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass
+CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared#
+CoResolution.dfy(22,9): Error: unresolved identifier: _k
+CoResolution.dfy(41,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
+CoResolution.dfy(52,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+CoResolution.dfy(70,12): Error: a copredicate is not allowed to declare any reads clause
+CoResolution.dfy(76,33): Error: a copredicate is not allowed to declare any ensures clause
CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(95,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(115,24): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(121,28): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(135,26): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(141,30): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
-CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not be determined
-CoResolution.dfy(202,13): Error: the type of this expression is underspecified
-CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not be determined
+CoResolution.dfy(90,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(99,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(113,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(114,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(119,24): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(125,28): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(133,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(134,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(139,26): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(145,30): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(153,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(155,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(171,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A' could not be determined
+CoResolution.dfy(206,13): Error: the type of this expression is underspecified
+CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined
24 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy index d8ff3989..d515e559 100644 --- a/Test/dafny0/Compilation.dfy +++ b/Test/dafny0/Compilation.dfy @@ -79,7 +79,7 @@ module A { import X as S default T;
import Y as S default T;
import Z = T;
- static method run() {
+ method run() {
var x := new X.C;
x.m();
var y := new Y.C;
@@ -96,17 +96,17 @@ method NotMain() { abstract module S1 {
import B as S default T;
- static method do()
+ method do()
}
module T1 refines S1 {
- static method do() {
+ method do() {
var x := 3;
}
}
module A1 {
import X as S1 default T1;
- static method run() {
+ method run() {
X.do();
var x := new X.B.C;
x.m();
diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy index 80e5eeae..f7a449b8 100644 --- a/Test/dafny0/CompilationErrors.dfy +++ b/Test/dafny0/CompilationErrors.dfy @@ -5,13 +5,15 @@ type MyType // compile error: opaque type iterator Iter() // compile error: body-less iterator
ghost method M() // compile error: body-less ghost method
method P() // compile error: body-less method
-method Q()
-{
- if g == 0 {
- assume true; // compile error: assume
+class TestClass {
+ method Q()
+ {
+ if g == 0 {
+ assume true; // compile error: assume
+ }
}
+ ghost var g: int;
}
-ghost var g: int;
function F(): int // compile error: body-less ghost function
function method H(): int // compile error: body-less function method
diff --git a/Test/dafny0/CompilationErrors.dfy.expect b/Test/dafny0/CompilationErrors.dfy.expect index e5583f30..f04b5ef8 100644 --- a/Test/dafny0/CompilationErrors.dfy.expect +++ b/Test/dafny0/CompilationErrors.dfy.expect @@ -2,12 +2,12 @@ Dafny program verifier finished with 15 verified, 0 errors
Compilation error: Opaque type ('_module.MyType') cannot be compiled
Compilation error: Iterator _module.Iter has no body
+Compilation error: an assume statement cannot be compiled (line 12)
Compilation error: Method _module._default.M has no body
Compilation error: Method _module._default.P has no body
-Compilation error: an assume statement cannot be compiled (line 11)
Compilation error: Function _module._default.F has no body
Compilation error: Function _module._default.H has no body
-Compilation error: an assume statement cannot be compiled (line 20)
-Compilation error: an assume statement cannot be compiled (line 23)
-Compilation error: an assume statement cannot be compiled (line 28)
-Compilation error: an assume statement cannot be compiled (line 37)
+Compilation error: an assume statement cannot be compiled (line 22)
+Compilation error: an assume statement cannot be compiled (line 25)
+Compilation error: an assume statement cannot be compiled (line 30)
+Compilation error: an assume statement cannot be compiled (line 39)
diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy index 12a4353d..0c539117 100644 --- a/Test/dafny0/ComputationsNeg.dfy +++ b/Test/dafny0/ComputationsNeg.dfy @@ -25,12 +25,12 @@ ghost method test_ThProperty() }
// The following is a test that well-typedness antecednets are included in the literal axioms
-static function StaticFact(n: nat): nat
+function StaticFact(n: nat): nat
ensures 0 < StaticFact(n);
{
if n == 0 then 1 else n * StaticFact(n - 1)
}
-static method test_StaticFact()
+method test_StaticFact()
{
assert StaticFact(0) == 1;
assert 42 != 42; // error: this should fail
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index 1295da96..cfdc2897 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -12,7 +12,7 @@ module CoRecursion { }
function AscendingChainAndRead(n: nat): Stream<int>
- reads this; // with a reads clause, this function is not a co-recusvie function
+ reads null; // with a reads clause, this function is not a co-recusvie function
{
More(n, AscendingChainAndRead(n+1)) // error: cannot prove termination
}
diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy index b283756b..265fadb5 100644 --- a/Test/dafny0/DirtyLoops.dfy +++ b/Test/dafny0/DirtyLoops.dfy @@ -1,33 +1,35 @@ // RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"
// RUN: %diff "%s.expect" "%t"
-method M0(S: set<int>) {
- forall s | s in S ensures s < 0;
-}
+class MyClass {
+ method M0(S: set<int>) {
+ forall s | s in S ensures s < 0;
+ }
-method M1(x: int)
-{
- var i := x;
- while (0 < i)
- invariant i <= x;
-}
+ method M1(x: int)
+ {
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+ }
-method M2(x: int)
-{
- var i := x;
- while (0 < i)
- invariant i <= x;
- decreases i;
-}
+ method M2(x: int)
+ {
+ var i := x;
+ while (0 < i)
+ invariant i <= x;
+ decreases i;
+ }
-var f: int;
+ var f: int;
-method M3(x: int)
- requires f <= x;
- modifies `f;
-{
- while (0 < f)
- invariant f <= x;
- decreases f;
+ method M3(x: int)
+ requires f <= x;
modifies `f;
+ {
+ while (0 < f)
+ invariant f <= x;
+ decreases f;
+ modifies `f;
+ }
}
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index 366cdfcc..aec38387 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -31,7 +31,7 @@ module Mx { }
}
- static method StaticM(k: nat) returns (m: int)
+ method StaticM(k: nat) returns (m: int)
{
m := k;
}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 14a71178..4814f26f 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -178,11 +178,11 @@ iterator AllocationIterator(x: Cell) }
}
-static method SomeMethod()
+method SomeMethod()
{
}
-static method AnotherMethod() returns (u: Cell, v: Cell)
+method AnotherMethod() returns (u: Cell, v: Cell)
ensures u != null && fresh(u);
{
u := new Cell;
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index dfa09b1e..b9f6a2c5 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -65,49 +65,51 @@ method M4(a: array<int>) returns (r: int) assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];
}
-var index: int;
-method P(a: array<int>) returns (b: bool, ii: int)
- requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
- modifies this, a;
- ensures ii == index;
- // The following uses a variable with a non-old definition inside an old expression:
- ensures 0 <= index < a.Length && old(a[ii]) == 19;
- ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;
- // The following places both the variable and the body inside an old:
- ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);
- // Here, the definition of the variable is old, and it's used both inside and
- // inside an old expression:
- ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;
-{
- b := 0 <= index < a.Length && a[index] == 17;
- var i, j := 0, -1;
- while (i < a.Length)
- invariant 0 <= i <= a.Length;
- invariant forall k :: 0 <= k < i ==> a[k] == 21;
- invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);
- invariant (0 <= j < i && old(a[j]) == 19) ||
- (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);
+class AClass {
+ var index: int;
+ method P(a: array<int>) returns (b: bool, ii: int)
+ requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
+ modifies this, a;
+ ensures ii == index;
+ // The following uses a variable with a non-old definition inside an old expression:
+ ensures 0 <= index < a.Length && old(a[ii]) == 19;
+ ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;
+ // The following places both the variable and the body inside an old:
+ ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);
+ // Here, the definition of the variable is old, and it's used both inside and
+ // inside an old expression:
+ ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;
{
- if (a[i] == 19) { j := i; }
- i, a[i] := i + 1, 21;
+ b := 0 <= index < a.Length && a[index] == 17;
+ var i, j := 0, -1;
+ while (i < a.Length)
+ invariant 0 <= i <= a.Length;
+ invariant forall k :: 0 <= k < i ==> a[k] == 21;
+ invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);
+ invariant (0 <= j < i && old(a[j]) == 19) ||
+ (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);
+ {
+ if (a[i] == 19) { j := i; }
+ i, a[i] := i + 1, 21;
+ }
+ index := j;
+ ii := index;
}
- index := j;
- ii := index;
-}
-method PMain(a: array<int>)
- requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
- modifies this, a;
-{
- var s := a[..];
- var b17, ii := P(a);
- assert s == old(a[..]);
- assert s[index] == 19;
- if (*) {
- assert a[index] == 19; // error (a can have changed in P)
- } else {
- assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;
- assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
+ method PMain(a: array<int>)
+ requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;
+ modifies this, a;
+ {
+ var s := a[..];
+ var b17, ii := P(a);
+ assert s == old(a[..]);
+ assert s[index] == 19;
+ if (*) {
+ assert a[index] == 19; // error (a can have changed in P)
+ } else {
+ assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;
+ assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;
+ }
}
}
diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect index 11a7aebe..b82e06ad 100644 --- a/Test/dafny0/LetExpr.dfy.expect +++ b/Test/dafny0/LetExpr.dfy.expect @@ -1,31 +1,31 @@ -LetExpr.dfy(8,12): Error: assertion violation
+LetExpr.dfy(108,23): Error: assertion violation
Execution trace:
(0,0): anon0
-LetExpr.dfy(107,21): Error: assertion violation
+ (0,0): anon11_Then
+LetExpr.dfy(8,12): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon11_Then
-LetExpr.dfy(251,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(253,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon5_Then
-LetExpr.dfy(254,19): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(256,19): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Then
-LetExpr.dfy(256,24): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(258,24): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-LetExpr.dfy(285,14): Error: RHS is not certain to look like the pattern 'Agnes'
+LetExpr.dfy(287,14): Error: RHS is not certain to look like the pattern 'Agnes'
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-LetExpr.dfy(302,42): Error: value assigned to a nat must be non-negative
+LetExpr.dfy(304,42): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-LetExpr.dfy(304,12): Error: assertion violation
+LetExpr.dfy(306,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon6_Else
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index ac466af2..51e7fe29 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -132,18 +132,20 @@ class Ghosty { ghost method Theorem(a: int) { }
}
-var SomeField: int;
+class AClassWithSomeField {
+ var SomeField: int;
-method SpecialFunctions()
- modifies this;
-{
- SomeField := SomeField + 4;
- var a := old(SomeField); // error: old can only be used in ghost contexts
- var b := fresh(this); // error: fresh can only be used in ghost contexts
- var c := allocated(this); // error: allocated can only be used in ghost contexts
- if (fresh(this)) { // this guard makes the if statement a ghost statement
- ghost var x := old(SomeField); // this is a ghost context, so it's okay
- ghost var y := allocated(this); // this is a ghost context, so it's okay
+ method SpecialFunctions()
+ modifies this;
+ {
+ SomeField := SomeField + 4;
+ var a := old(SomeField); // error: old can only be used in ghost contexts
+ var b := fresh(this); // error: fresh can only be used in ghost contexts
+ var c := allocated(this); // error: allocated can only be used in ghost contexts
+ if (fresh(this)) { // this guard makes the if statement a ghost statement
+ ghost var x := old(SomeField); // this is a ghost context, so it's okay
+ ghost var y := allocated(this); // this is a ghost context, so it's okay
+ }
}
}
@@ -323,3 +325,12 @@ module Q_M { }
class Node { }
}
+
+// ------- top-level statics -----------------
+
+module TopLevelStatics {
+ static function F(): int // error/warning: static keyword does not belong here
+ { 0 }
+ static method M() // error/warning: static keyword does not belong here
+ { }
+}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index 90436ed8..0d9d44de 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -1,3 +1,5 @@ +Modules0.dfy(332,3): warning: module-level functions are always non-instance, so the 'static' keyword is not allowed here
+Modules0.dfy(334,3): warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
Modules0.dfy(8,8): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(9,11): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupA
@@ -14,24 +16,24 @@ Modules0.dfy(79,13): Error: expected method call, found expression Modules0.dfy(84,8): Error: type MyClassY does not have a member M
Modules0.dfy(84,9): Error: expected method call, found expression
Modules0.dfy(92,19): Error: Undeclared top-level type or type parameter: ClassG (did you forget to qualify a name?)
-Modules0.dfy(224,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-Modules0.dfy(224,8): Error: new can be applied only to reference types (got X)
-Modules0.dfy(233,13): Error: Undeclared type X in module B
-Modules0.dfy(243,13): Error: unresolved identifier: X
-Modules0.dfy(244,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(283,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
-Modules0.dfy(283,12): Error: new can be applied only to reference types (got D)
-Modules0.dfy(286,25): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(287,17): Error: expected method call, found expression
-Modules0.dfy(288,16): Error: type of the receiver is not fully determined at this program point
-Modules0.dfy(288,17): Error: expected method call, found expression
-Modules0.dfy(310,24): Error: module Q_Imp does not exist
+Modules0.dfy(226,15): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+Modules0.dfy(226,8): Error: new can be applied only to reference types (got X)
+Modules0.dfy(235,13): Error: Undeclared type X in module B
+Modules0.dfy(245,13): Error: unresolved identifier: X
+Modules0.dfy(246,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(285,19): Error: Undeclared top-level type or type parameter: D (did you forget to qualify a name?)
+Modules0.dfy(285,12): Error: new can be applied only to reference types (got D)
+Modules0.dfy(288,25): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(289,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(289,17): Error: expected method call, found expression
+Modules0.dfy(290,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(290,17): Error: expected method call, found expression
+Modules0.dfy(312,24): Error: module Q_Imp does not exist
Modules0.dfy(102,6): Error: type MyClassY does not have a member M
Modules0.dfy(102,7): Error: expected method call, found expression
Modules0.dfy(127,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(141,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(142,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(143,11): Error: unresolved identifier: allocated
-Modules0.dfy(146,19): Error: unresolved identifier: allocated
+Modules0.dfy(142,13): Error: old expressions are allowed only in specification and ghost contexts
+Modules0.dfy(143,13): Error: fresh expressions are allowed only in specification and ghost contexts
+Modules0.dfy(144,13): Error: unresolved identifier: allocated
+Modules0.dfy(147,21): Error: unresolved identifier: allocated
36 resolution/type errors detected in Modules0.dfy
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index 2f38e39e..c134bb9a 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -19,7 +19,7 @@ class C { method MyMethod() { }
-var MyField: int;
+
module Babble {
class Z {
@@ -30,7 +30,7 @@ module Babble { }
}
-static function MyFunction(): int { 5 }
+function MyFunction(): int { 5 }
class D { }
diff --git a/Test/dafny0/Modules2.dfy b/Test/dafny0/Modules2.dfy index 8b2ff570..6a68c38e 100644 --- a/Test/dafny0/Modules2.dfy +++ b/Test/dafny0/Modules2.dfy @@ -6,14 +6,14 @@ module A { var f: int;
}
datatype D = E(int) | F(int);
- static function f(n:nat): nat
+ function f(n:nat): nat
}
module B {
class C {
var f: int;
}
datatype D = E(int) | F(int);
- static function f(n:nat): nat
+ function f(n:nat): nat
}
module Test {
import opened A; // nice shorthand for import opened A = A; (see below)
@@ -49,7 +49,7 @@ module Test3 { var d := E(i); // bad, as both A and B give a definition of E
var d' := D.E(i); // bad, as D is still itself ambiguous.
var d'':= B.D.E(i); // good, just use the B version
- assert f(3) >= 0; // bad because A and be both define f statically.
+ assert f(3) >= 0; // bad because A and B both define f statically.
}
}
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 78049387..86f8c127 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -10,28 +10,30 @@ method Main() { M(-25); // error: cannot pass -25 as a nat
}
-var f: nat;
+class MyClass {
+ var f: nat;
-method CheckField(x: nat, y: int)
- requires 0 <= y;
- modifies this;
-{
- var y: nat := y;
-
- assert 0 <= f;
- while (0 < y)
+ method CheckField(x: nat, y: int)
+ requires 0 <= y;
+ modifies this;
{
- f := f + 1;
- if (15 < f) {
- f := f - 12;
+ var y: nat := y;
+
+ assert 0 <= f;
+ while (0 < y)
+ {
+ f := f + 1;
+ if (15 < f) {
+ f := f - 12;
+ }
+ y := y - 1;
}
- y := y - 1;
- }
- assert 0 <= f;
+ assert 0 <= f;
- f := x; // no problem
- f := x + 3; // no problem here either
- f := x - 3; // error: cannot prove RHS is a nat
+ f := x; // no problem
+ f := x + 3; // no problem here either
+ f := x - 3; // error: cannot prove RHS is a nat
+ }
}
method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
diff --git a/Test/dafny0/NatTypes.dfy.expect b/Test/dafny0/NatTypes.dfy.expect index 7bee017c..99fa16e5 100644 --- a/Test/dafny0/NatTypes.dfy.expect +++ b/Test/dafny0/NatTypes.dfy.expect @@ -1,41 +1,41 @@ -NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative
-Execution trace:
- (0,0): anon0
-NatTypes.dfy(34,10): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(35,12): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
- NatTypes.dfy(22,3): anon10_LoopHead
+ NatTypes.dfy(23,5): anon10_LoopHead
(0,0): anon10_LoopBody
- NatTypes.dfy(22,3): anon11_Else
+ NatTypes.dfy(23,5): anon11_Else
(0,0): anon12_Then
-NatTypes.dfy(41,14): Error: assertion violation
+NatTypes.dfy(10,5): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
- (0,0): anon4_Then
NatTypes.dfy(43,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
-NatTypes.dfy(60,16): Error: assertion violation
+NatTypes.dfy(45,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+NatTypes.dfy(62,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(74,16): Error: assertion violation
+NatTypes.dfy(76,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon5_Else
(0,0): anon6_Then
-NatTypes.dfy(92,22): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(94,22): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-NatTypes.dfy(107,45): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(109,45): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-NatTypes.dfy(130,35): Error: value assigned to a nat must be non-negative
+NatTypes.dfy(132,35): Error: value assigned to a nat must be non-negative
Execution trace:
(0,0): anon0
(0,0): anon3_Then
diff --git a/Test/dafny0/Newtypes.dfy b/Test/dafny0/Newtypes.dfy index db737f68..93caa7ab 100644 --- a/Test/dafny0/Newtypes.dfy +++ b/Test/dafny0/Newtypes.dfy @@ -53,7 +53,7 @@ module Constraints { newtype B = x: A | x < 100
newtype C = B // the constraints 0 <= x < 100 still apply
- static predicate IsEven(x: int) // note that this is a ghost predicate
+ predicate IsEven(x: int) // note that this is a ghost predicate
{
x % 2 == 0
}
diff --git a/Test/dafny0/NewtypesResolution.dfy b/Test/dafny0/NewtypesResolution.dfy index dbf9a175..9ae657b7 100644 --- a/Test/dafny0/NewtypesResolution.dfy +++ b/Test/dafny0/NewtypesResolution.dfy @@ -80,7 +80,7 @@ module Constraints { newtype B = x: A | x < 100
newtype C = B // the constraints 0 <= x < 100 still apply
- static predicate IsEven(x: int) // note that this is a ghost predicate
+ predicate IsEven(x: int) // note that this is a ghost predicate
{
x % 2 == 0
}
@@ -103,7 +103,7 @@ module WrongNumberOfArguments { module CyclicDependencies {
newtype Cycle = x: int | (BadLemma(); false) // error: cycle
- static lemma BadLemma()
+ lemma BadLemma()
ensures false;
{
var c: Cycle;
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index d343a84d..030eb350 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -209,7 +209,7 @@ class TwoState_C { ghost var data: int; } // It is not possible to achieve this postcondition in a ghost method, because ghost
// contexts are not allowed to allocate state. Callers of this ghost method will know
// that the postcondition is tantamount to 'false'.
-ghost static method TwoState0(y: int)
+ghost method TwoState0(y: int)
ensures exists o: TwoState_C :: o != null && fresh(o);
method TwoState_Main0() {
@@ -261,39 +261,41 @@ method TwoState_Main3() // ------- empty forall statement -----------------------------------------
-var emptyPar: int;
+class EmptyForallStatement {
+ var emptyPar: int;
-method Empty_Parallel0()
- modifies this;
- ensures emptyPar == 8;
-{
- forall () {
- this.emptyPar := 8;
+ method Empty_Parallel0()
+ modifies this;
+ ensures emptyPar == 8;
+ {
+ forall () {
+ this.emptyPar := 8;
+ }
}
-}
-function EmptyPar_P(x: int): bool
-ghost method EmptyPar_Lemma(x: int)
- ensures EmptyPar_P(x);
+ function EmptyPar_P(x: int): bool
+ ghost method EmptyPar_Lemma(x: int)
+ ensures EmptyPar_P(x);
-method Empty_Parallel1()
- ensures EmptyPar_P(8);
-{
- forall {
- EmptyPar_Lemma(8);
+ method Empty_Parallel1()
+ ensures EmptyPar_P(8);
+ {
+ forall {
+ EmptyPar_Lemma(8);
+ }
}
-}
-method Empty_Parallel2()
-{
- forall
- ensures exists k :: EmptyPar_P(k);
+ method Empty_Parallel2()
{
- var y := 8;
- assume EmptyPar_P(y);
+ forall
+ ensures exists k :: EmptyPar_P(k);
+ {
+ var y := 8;
+ assume EmptyPar_P(y);
+ }
+ assert exists k :: EmptyPar_P(k); // yes
+ assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this
}
- assert exists k :: EmptyPar_P(k); // yes
- assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this
}
// ---------------------------------------------------------------------
diff --git a/Test/dafny0/Parallel.dfy.expect b/Test/dafny0/Parallel.dfy.expect index 6b726cd5..db551bba 100644 --- a/Test/dafny0/Parallel.dfy.expect +++ b/Test/dafny0/Parallel.dfy.expect @@ -1,3 +1,7 @@ +Parallel.dfy(297,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
Parallel.dfy(34,10): Error BP5002: A precondition for this call might not hold.
Parallel.dfy(60,14): Related location: This is the precondition that might not hold.
Execution trace:
@@ -60,9 +64,5 @@ Execution trace: (0,0): anon19_Then
(0,0): anon20_Then
(0,0): anon5
-Parallel.dfy(296,20): Error: assertion violation
-Execution trace:
- (0,0): anon0
- (0,0): anon4_Else
Dafny program verifier finished with 43 verified, 9 errors
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index 1a9a3257..a92e647a 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -38,30 +38,36 @@ module B refines A { // ------------------------------------------------ module A_AnonymousClass { - var x: int; - method Increment(d: int) - modifies this; - { - x := x + d; + class XX { + var x: int; + method Increment(d: int) + modifies this; + { + x := x + d; + } } } module B_AnonymousClass refines A_AnonymousClass { - method Increment... - ensures x <= old(x) + d; + class XX { + method Increment... + ensures x <= old(x) + d; + } } module C_AnonymousClass refines B_AnonymousClass { - method Increment(d: int) - ensures old(x) + d <= x; - method Main() - modifies this; - { - x := 25; - Increment(30); - assert x == 55; - Increment(12); - assert x == 66; // error: it's 67 + class XX { + method Increment(d: int) + ensures old(x) + d <= x; + method Main() + modifies this; + { + x := 25; + Increment(30); + assert x == 55; + Increment(12); + assert x == 66; // error: it's 67 + } } } diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect index d214565b..93d59873 100644 --- a/Test/dafny0/Refinement.dfy.expect +++ b/Test/dafny0/Refinement.dfy.expect @@ -6,35 +6,35 @@ Refinement.dfy[B](15,5): Error BP5003: A postcondition might not hold on this re Refinement.dfy(33,20): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(64,14): Error: assertion violation
+Refinement.dfy(69,16): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(74,17): Error: assertion violation
+Refinement.dfy(80,17): Error: assertion violation
Execution trace:
(0,0): anon0
-Refinement.dfy(93,12): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(72,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(99,12): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(78,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Refinement.dfy(96,3): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy(77,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(102,3): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(83,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](115,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(180,9): Related location
+Refinement.dfy(189,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](121,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,9): Related location
Execution trace:
(0,0): anon0
-Refinement.dfy(187,5): Error BP5003: A postcondition might not hold on this return path.
-Refinement.dfy[IncorrectConcrete](123,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(180,9): Related location
+Refinement.dfy(193,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy[IncorrectConcrete](129,15): Related location: This is the postcondition that might not hold.
+Refinement.dfy(186,9): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Refinement.dfy(193,7): Error: assertion violation
-Refinement.dfy[IncorrectConcrete](131,24): Related location
+Refinement.dfy(199,7): Error: assertion violation
+Refinement.dfy[IncorrectConcrete](137,24): Related location
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/RefinementModificationChecking.dfy b/Test/dafny0/RefinementModificationChecking.dfy index 70d0b989..052918d0 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy +++ b/Test/dafny0/RefinementModificationChecking.dfy @@ -2,25 +2,29 @@ // RUN: %diff "%s.expect" "%t"
abstract module R1 {
- var f: int;
- method m(y: set<int>) returns (r: int)
- modifies this;
- {
- var t := y;
+ class HappyBay {
+ var f: int;
+ method m(y: set<int>) returns (r: int)
+ modifies this;
+ {
+ var t := y;
+ }
}
}
module R2 refines R1 {
- var g: nat;
- method m ...
- {
- ...;
- var x := 3;
- t := {1}; // error: previous local
- r := 3; // error: out parameter
- f := 4; // error: previously defined field
- x := 6; // fine: new local
- g := 34;// fine: new field
+ class HappyBay {
+ var g: nat;
+ method m ...
+ {
+ ...;
+ var x := 3;
+ t := {1}; // error: previous local
+ r := 3; // error: out parameter
+ f := 4; // error: previously defined field
+ x := 6; // fine: new local
+ g := 34;// fine: new field
+ }
}
}
diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect index 675d244e..1a5df922 100644 --- a/Test/dafny0/RefinementModificationChecking.dfy.expect +++ b/Test/dafny0/RefinementModificationChecking.dfy.expect @@ -1,6 +1,6 @@ -RefinementModificationChecking.dfy(19,4): Error: refinement method cannot assign to variable defined in parent module ('t')
-RefinementModificationChecking.dfy(20,4): Error: refinement method cannot assign to variable defined in parent module ('r')
-RefinementModificationChecking.dfy(21,4): Error: refinement method cannot assign to a field defined in parent module ('f')
-RefinementModificationChecking.dfy(47,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
-RefinementModificationChecking.dfy(49,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
+RefinementModificationChecking.dfy(22,6): Error: refinement method cannot assign to variable defined in parent module ('t')
+RefinementModificationChecking.dfy(23,6): Error: refinement method cannot assign to variable defined in parent module ('r')
+RefinementModificationChecking.dfy(24,6): Error: refinement method cannot assign to a field defined in parent module ('f')
+RefinementModificationChecking.dfy(51,15): Error: assignment RHS in refinement method is not allowed to affect previously defined state
+RefinementModificationChecking.dfy(53,11): Error: new assignments in a refinement method can only assign to state that the module defines (which never includes array elements)
5 resolution/type errors detected in RefinementModificationChecking.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 2f340557..4b290bb7 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -78,25 +78,27 @@ datatype Xyz = Alberta | Benny | Constantine(y: int) | David(x: int); datatype Rst = David(x: int, y: int);
function Tuv(arg0: Abc, arg1: bool): int { 10 }
-var Eleanor: bool;
-
-method TestNameResolution1() {
- var a0 := Abel;
- var a1 := Alberta;
- var b0 := Benny; // error: there's more than one constructor with the name Benny; needs qualification
- var b1 := Abc.Benny;
- var b2 := Xyz.Benny;
- var Benny := 15; // introduce a local variable with the name 'Benny'
- var b3 := Benny;
- var d0 := David(20); // error: constructor name David is ambiguous
- var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does
- // not match either of them)
- var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given
- // parameters match the signature of only one of those constructors)
- var d3 := Abc.David(20, 40); // error: wrong number of parameters
- var d4 := Rst.David(20, 40);
- var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
- assert Tuv(Abc.Eleanor, e) == 10;
+
+class EE {
+ var Eleanor: bool;
+ method TestNameResolution1() {
+ var a0 := Abel;
+ var a1 := Alberta;
+ var b0 := Benny; // error: there's more than one constructor with the name Benny; needs qualification
+ var b1 := Abc.Benny;
+ var b2 := Xyz.Benny;
+ var Benny := 15; // introduce a local variable with the name 'Benny'
+ var b3 := Benny;
+ var d0 := David(20); // error: constructor name David is ambiguous
+ var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does
+ // not match either of them)
+ var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given
+ // parameters match the signature of only one of those constructors)
+ var d3 := Abc.David(20, 40); // error: wrong number of parameters
+ var d4 := Rst.David(20, 40);
+ var e := Eleanor; // this resolves to the field, not the Abc datatype constructor
+ assert Tuv(Abc.Eleanor, e) == 10;
+ }
}
// --------------- ghost tests -------------------------------------
@@ -386,34 +388,35 @@ method TestCalc(m: int, n: int, a: bool, b: bool) }
}
-/* Side-effect checks */
-ghost var ycalc: int;
+class SideEffectChecks {
+ ghost var ycalc: int;
-ghost method Mod(a: int)
- modifies this;
- ensures ycalc == a;
-{
- ycalc := a;
-}
+ ghost method Mod(a: int)
+ modifies this;
+ ensures ycalc == a;
+ {
+ ycalc := a;
+ }
-ghost method Bad()
- modifies this;
- ensures 0 == 1;
-{
- var x: int;
- calc {
- 0;
- { Mod(0); } // methods with side-effects are not allowed
- ycalc;
- { ycalc := 1; } // heap updates are not allowed
- 1;
- { x := 1; } // updates to locals defined outside of the hint are not allowed
- x;
- {
- var x: int;
- x := 1; // this is OK
+ ghost method Bad()
+ modifies this;
+ ensures 0 == 1;
+ {
+ var x: int;
+ calc {
+ 0;
+ { Mod(0); } // methods with side-effects are not allowed
+ ycalc;
+ { ycalc := 1; } // heap updates are not allowed
+ 1;
+ { x := 1; } // updates to locals defined outside of the hint are not allowed
+ x;
+ {
+ var x: int;
+ x := 1; // this is OK
+ }
+ 1;
}
- 1;
}
}
@@ -648,9 +651,9 @@ module UnderspecifiedTypes { // ------------------------- lemmas ------------------------------
// a lemma is allowed to have out-parameters, but not a modifies clause
-lemma MyLemma(x: int) returns (y: int)
+lemma MyLemma(x: int, l: Lamb) returns (y: int)
requires 0 <= x;
- modifies this;
+ modifies l;
ensures 0 <= y;
{
y := x;
@@ -659,110 +662,112 @@ lemma MyLemma(x: int) returns (y: int) // ------------------------- statements in expressions ------------------------------
module StatementsInExpressions {
- ghost method SideEffect()
- modifies this;
- {
- }
-
- method NonGhostMethod()
- {
- }
+ class MyClass {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
- ghost method M()
- modifies this;
- {
- calc {
- 5;
- { SideEffect(); } // error: cannot call method with side effects
- 5;
+ method NonGhostMethod()
+ {
}
- }
- function F(): int
- {
- calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects
+ 5;
}
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
+ }
+
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
- 6;
+ 5
}
- 5
- }
- var MyField: int;
- ghost var MyGhostField: int;
+ var MyField: int;
+ ghost var MyGhostField: int;
- method N()
- {
- var y :=
- calc {
- 6;
- { assert 6 < 8; }
- { NonGhostMethod(); } // error: cannot call non-ghost method
- { var x := 8;
- while x != 0
- decreases *; // error: cannot use 'decreases *' in a ghost context
- {
- x := x - 1;
- }
- }
- { MyField := 12; } // error: cannot assign to a field
- { MyGhostField := 12; } // error: cannot assign to any field
- { M(); } // error: cannot call (ghost) method with a modifies clause
- { var x := 8;
- while x != 0
- modifies this; // error: cannot use a modifies clause on a loop
- {
- x := x - 1;
- }
- }
- { var x := 8;
- while x != 0
- {
- x := x - 1;
- }
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
}
- 6;
+ 5;
}
- 5;
- }
- ghost method MyLemma()
- ghost method MyGhostMethod()
- modifies this;
- method OrdinaryMethod()
- ghost method OutParamMethod() returns (y: int)
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
- function UseLemma(): int
- {
- MyLemma();
- MyGhostMethod(); // error: modifies state
- OrdinaryMethod(); // error: not a ghost
- OutParamMethod(); // error: has out-parameters
- 10
+ function UseLemma(): int
+ {
+ MyLemma();
+ MyGhostMethod(); // error: modifi2es state
+ OrdinaryMethod(); // error: not a ghost
+ OutParamMethod(); // error: has out-parameters
+ 10
+ }
}
}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 9ba6a1b3..55a4b1e6 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -1,125 +1,133 @@ -ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
-ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
-ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
-ResolutionErrors.dfy(558,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(565,25): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be determined
-ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements
-ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context
-ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(619,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(686,22): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(700,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(700,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(702,18): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(724,22): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(732,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(732,16): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(734,9): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(762,17): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(764,18): Error: wrong number of method result arguments (got 0, expected 1)
-ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object)
-ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object)
-ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object)
-ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
-ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq<int>)
-ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field
-ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
-ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
-ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
-ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2
-ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
-ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
-ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1000,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
-ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1019,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
+ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
+ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
+ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
+ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
+ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
+ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(611,10): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
+ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(704,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(736,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
+ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
+ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
+ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
+ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
+ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
+ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
+ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
+ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
+ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
+ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
+ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
+ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
+ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
+ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
-ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
-ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
-ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
-ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
-ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
-ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
-ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
-ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)
-ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)
-ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1113,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1115,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
-ResolutionErrors.dfy(1220,26): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1286,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
-ResolutionErrors.dfy(1296,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor
+ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
+ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
+ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
+ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
+ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
+ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
+ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
+ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
+ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
+ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
+ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
+ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
+ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
-ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(117,10): Error: actual out-parameter 0 is required to be a ghost variable
-ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(149,10): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
-ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
-ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor
-ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
-ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x
-ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x
-ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x
-ResolutionErrors.dfy(1041,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
+ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
+ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
+ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
+ResolutionErrors.dfy(446,9): Error: class Lamb does not have a anonymous constructor
+ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
+ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
+ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
+ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
+ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
@@ -133,53 +141,45 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
-ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
-ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
-ResolutionErrors.dfy(96,16): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
-ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
-ResolutionErrors.dfy(263,2): Error: duplicate label
-ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
-ResolutionErrors.dfy(292,9): Error: a constructor is allowed to be called only when an object is being allocated
-ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
-ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
-ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(345,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
-ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
-ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
-ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(384,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ResolutionErrors.dfy(406,9): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint
-ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
-ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
-ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
-ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
-ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
-ResolutionErrors.dfy(931,16): Error: condition is expected to be of type bool, but is int
-ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
-ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
-ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
-ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
-ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
-ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
-ResolutionErrors.dfy(1129,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
-ResolutionErrors.dfy(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(265,2): Error: duplicate label
+ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
+ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
+ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
+ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
+ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
+ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
+ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
+ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
+ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(386,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(544,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(546,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(548,7): Error: let-such-that expressions are allowed only in ghost contexts
+ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
+ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
+ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
+ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
+ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
+ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
+ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
+ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
+ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
+ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
+ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
+ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
+ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
184 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7d8628a9..13f56383 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -511,7 +511,7 @@ class AttributeTests { // ----------------------- test attributes on variable declarations --------
-static method TestAttributesVarDecls()
+method TestAttributesVarDecls()
{
var {:foo foo} foo := null;
var {:bar bar} bar := 0;
@@ -521,7 +521,7 @@ static method TestAttributesVarDecls() // ----------------------- Pretty printing of !(!expr) --------
-static method TestNotNot()
+method TestNotNot()
{
assert !(!true); // Shouldn't pretty print as "!!true".
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 70c30aa6..0e51ade2 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -201,50 +201,51 @@ method DecreasesYieldsAnInvariant(z: int) { // ----------------------- top elements --------------------------------------
-var count: int;
+class TopElements {
+ var count: int;
-// Here is the old way that this had to be specified:
+ // Here is the old way that this had to be specified:
-method OuterOld(a: int)
- modifies this;
- decreases a, true;
-{
- count := count + 1;
- InnerOld(a, count);
-}
+ method OuterOld(a: int)
+ modifies this;
+ decreases a, true;
+ {
+ count := count + 1;
+ InnerOld(a, count);
+ }
-method InnerOld(a: int, b: int)
- modifies this;
- decreases a, false, b;
-{
- count := count + 1;
- if (b == 0 && 1 <= a) {
- OuterOld(a - 1);
- } else if (1 <= b) {
- InnerOld(a, b - 1);
+ method InnerOld(a: int, b: int)
+ modifies this;
+ decreases a, false, b;
+ {
+ count := count + 1;
+ if (b == 0 && 1 <= a) {
+ OuterOld(a - 1);
+ } else if (1 <= b) {
+ InnerOld(a, b - 1);
+ }
}
-}
-// Now the default specifications ("decreases a;" and "decreases a, b;") suffice:
+ // Now the default specifications ("decreases a;" and "decreases a, b;") suffice:
-method Outer(a: int)
- modifies this;
-{
- count := count + 1;
- Inner(a, count);
-}
+ method Outer(a: int)
+ modifies this;
+ {
+ count := count + 1;
+ Inner(a, count);
+ }
-method Inner(a: int, b: int)
- modifies this;
-{
- count := count + 1;
- if (b == 0 && 1 <= a) {
- Outer(a - 1);
- } else if (1 <= b) {
- Inner(a, b - 1);
+ method Inner(a: int, b: int)
+ modifies this;
+ {
+ count := count + 1;
+ if (b == 0 && 1 <= a) {
+ Outer(a - 1);
+ } else if (1 <= b) {
+ Inner(a, b - 1);
+ }
}
}
-
// -------------------------- decrease either datatype value -----------------
function Zipper0<T>(a: List<T>, b: List<T>): List<T>
diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect index fd86c8cb..98aa0cd8 100644 --- a/Test/dafny0/Termination.dfy.expect +++ b/Test/dafny0/Termination.dfy.expect @@ -1,7 +1,7 @@ -Termination.dfy[TerminationRefinement1](440,6): Error: failure to decrease termination measure
+Termination.dfy[TerminationRefinement1](441,6): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Termination.dfy(360,47): Error: failure to decrease termination measure
+Termination.dfy(361,47): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
(0,0): anon7_Else
@@ -41,18 +41,18 @@ Execution trace: (0,0): anon10_Then
(0,0): anon5
Termination.dfy(125,3): anon11_Else
-Termination.dfy(254,35): Error: cannot prove termination; try supplying a decreases clause
+Termination.dfy(255,35): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon6_Else
(0,0): anon7_Else
(0,0): anon8_Then
-Termination.dfy(295,3): Error: decreases expression might not decrease
+Termination.dfy(296,3): Error: decreases expression might not decrease
Execution trace:
- Termination.dfy(295,3): anon9_LoopHead
+ Termination.dfy(296,3): anon9_LoopHead
(0,0): anon9_LoopBody
- Termination.dfy(295,3): anon10_Else
- Termination.dfy(295,3): anon11_Else
+ Termination.dfy(296,3): anon10_Else
+ Termination.dfy(296,3): anon11_Else
(0,0): anon12_Else
Dafny program verifier finished with 62 verified, 8 errors
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index d5c6a9d2..1e4f928a 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -28,7 +28,7 @@ method BadLemma(c0: Color, c1: Color) var w1 := Wrapper.Wrap(c1);
// Manually, add the following assertions in Boogie. (These would
- // be ill-typed in Dafny.)
+ // b93e ill-typed in Dafny.)
// assert _default.F($Heap, this, w#06);
// assert _default.F($Heap, this, w#17);
@@ -68,7 +68,8 @@ method M(list: List, S: set<MyClass>) returns (ret: int) }
var k := N();
assert k.H() == 5;
- ghost var l := NF();
+ var st := new State;
+ ghost var l := st.NF();
assert l != null ==> l.H() == 5;
forall s | s in S ensures true; { assert s == null || s.H() == 5; }
@@ -90,8 +91,11 @@ method N() returns (k: MyClass) {
k := new MyClass;
}
-var a: MyClass;
-function NF(): MyClass reads this; { a }
+
+class State {
+ var a: MyClass;
+ function NF(): MyClass reads this; { a }
+}
function TakesADatatype(a: List): int { 12 }
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index aa3d7671..f066d13f 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -105,7 +105,7 @@ class CClient { // -------------------------
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+function IsCelebrity<Person>(c: Person, people: set<Person>): bool
requires c == c || c in people;
{
false
@@ -119,7 +119,7 @@ method FindCelebrity3(people: set<int>, ghost c: int) b := F(c, people);
}
-static function F(c: int, people: set<int>): bool
+function F(c: int, people: set<int>): bool
requires IsCelebrity(c, people);
{
false
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index 3a0828d4..75277b8b 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -7,11 +7,11 @@ Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); Dafny program verifier finished with 3 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
- >>> added axiom: (forall call1old#AT#$Heap: Heap :: { ##extracted_function##1(call1old#AT#$Heap) } ##extracted_function##1(call1old#AT#$Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap)))
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call1old#AT#$Heap);
+ >>> added axiom: (forall call0old#AT#$Heap: Heap :: { ##extracted_function##1(call0old#AT#$Heap) } ##extracted_function##1(call0old#AT#$Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
+ >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);
Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call1old#AT#$Heap);
+Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
>>> MarkAsPartiallyVerified
@@ -49,13 +49,13 @@ Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f >>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,11)) assert this == this;
+Processing command (at Snapshots2.v0.dfy(11,11)) assert true;
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this));
+Processing command (at Snapshots2.v0.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,11)) assert this == this;
+Processing command (at Snapshots2.v0.dfy(14,11)) assert true;
>>> DoNothingToAssert
-Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this));
+Processing command (at Snapshots2.v0.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Processing command (at Snapshots2.v0.dfy(18,3)) assert true;
>>> DoNothingToAssert
@@ -72,13 +72,13 @@ Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); Snapshots2.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
-Processing command (at Snapshots2.v1.dfy(11,11)) assert this == this;
+Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this));
+Processing command (at Snapshots2.v1.dfy(11,15)) assert Lit(_module.__default.P($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap));
>>> DoNothingToAssert
-Processing command (at Snapshots2.v1.dfy(14,11)) assert this == this;
+Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
>>> MarkAsFullyVerified
-Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this));
+Processing command (at Snapshots2.v1.dfy(14,15)) assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap)) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 360c5aba..fb7a5fab 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -3,10 +3,10 @@ // Celebrity example, inspired by the Rodin tutorial
-static function method Knows<X>(a: X, b: X): bool
+function method Knows<X>(a: X, b: X): bool
requires a != b; // forbid asking about the reflexive case
-static function IsCelebrity<Y>(c: Y, people: set<Y>): bool
+function IsCelebrity<Y>(c: Y, people: set<Y>): bool
{
c in people &&
(forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy index 10b70e09..174e71c8 100644 --- a/Test/dafny1/Substitution.dfy +++ b/Test/dafny1/Substitution.dfy @@ -8,7 +8,7 @@ datatype Expr = Var(int) |
Nary(int, List);
-static function Subst(e: Expr, v: int, val: int): Expr
+function Subst(e: Expr, v: int, val: int): Expr
{
match e
case Const(c) => e
@@ -16,14 +16,14 @@ static function Subst(e: Expr, v: int, val: int): Expr case Nary(op, args) => Expr.Nary(op, SubstList(args, v, val))
}
-static function SubstList(l: List, v: int, val: int): List
+function SubstList(l: List, v: int, val: int): List
{
match l
case Nil => l
case Cons(e, tail) => Cons(Subst(e, v, val), SubstList(tail, v, val))
}
-static ghost method Theorem(e: Expr, v: int, val: int)
+lemma Theorem(e: Expr, v: int, val: int)
ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
{
match e {
@@ -34,7 +34,7 @@ static ghost method Theorem(e: Expr, v: int, val: int) }
}
-static ghost method Lemma(l: List, v: int, val: int)
+lemma Lemma(l: List, v: int, val: int)
ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
{
match l {
@@ -52,7 +52,7 @@ datatype Expression = Var(int) |
Nary(int, seq<Expression>);
-static function Substitute(e: Expression, v: int, val: int): Expression
+function Substitute(e: Expression, v: int, val: int): Expression
decreases e;
{
match e
@@ -61,7 +61,7 @@ static function Substitute(e: Expression, v: int, val: int): Expression case Nary(op, args) => Expression.Nary(op, SubstSeq(e, args, v, val))
}
-static function SubstSeq(/*ghost*/ parent: Expression,
+function SubstSeq(/*ghost*/ parent: Expression,
q: seq<Expression>, v: int, val: int): seq<Expression>
requires (forall a :: a in q ==> a < parent);
decreases parent, q;
@@ -70,7 +70,7 @@ static function SubstSeq(/*ghost*/ parent: Expression, SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
}
-static ghost method TheoremSeq(e: Expression, v: int, val: int)
+lemma TheoremSeq(e: Expression, v: int, val: int)
ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
{
match e {
@@ -97,7 +97,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int) }
}
-static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
+lemma LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index 763cef1b..beb1597e 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -7,13 +7,13 @@ datatype List<T> = Nil | Cons(T, List<T>); datatype Tree = Node(int, List<Tree>);
-static function Inc(t: Tree): Tree
+function Inc(t: Tree): Tree
{
match t
case Node(n, children) => Tree.Node(n+1, ForestInc(children))
}
-static function ForestInc(forest: List<Tree>): List<Tree>
+function ForestInc(forest: List<Tree>): List<Tree>
{
match forest
case Nil => forest
@@ -24,13 +24,13 @@ static function ForestInc(forest: List<Tree>): List<Tree> datatype GTree<T> = Node(T, List<GTree<T>>);
-static function GInc(t: GTree<int>): GTree<int>
+function GInc(t: GTree<int>): GTree<int>
{
match t
case Node(n, children) => GTree.Node(n+1, GForestInc(children))
}
-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
+function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
{
match forest
case Nil => forest
@@ -43,13 +43,13 @@ datatype TreeList = Nil | Cons(OneTree, TreeList); datatype OneTree = Node(int, TreeList);
-static function XInc(t: OneTree): OneTree
+function XInc(t: OneTree): OneTree
{
match t
case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
}
-static function XForestInc(forest: TreeList): TreeList
+function XForestInc(forest: TreeList): TreeList
{
match forest
case Nil => forest
diff --git a/Test/dafny2/Intervals.dfy b/Test/dafny2/Intervals.dfy index df14c1e9..ef40910e 100644 --- a/Test/dafny2/Intervals.dfy +++ b/Test/dafny2/Intervals.dfy @@ -4,63 +4,65 @@ // The RoundDown and RoundUp methods in this file are the ones in the Boogie
// implementation Source/AbsInt/IntervalDomain.cs.
-var thresholds: array<int>;
+class Rounding {
+ var thresholds: array<int>;
-function Valid(): bool
- reads this, thresholds;
-{
- thresholds != null &&
- forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
-}
-
-method RoundDown(k: int) returns (r: int)
- requires Valid();
- ensures -1 <= r < thresholds.Length;
- ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
- ensures 0 <= r ==> thresholds[r] <= k;
-{
- if (thresholds.Length == 0 || k < thresholds[0]) {
- return -1;
+ function Valid(): bool
+ reads this, thresholds;
+ {
+ thresholds != null &&
+ forall m,n :: 0 <= m < n < thresholds.Length ==> thresholds[m] <= thresholds[n]
}
- var i, j := 0, thresholds.Length - 1;
- while (i < j)
- invariant 0 <= i <= j < thresholds.Length;
- invariant thresholds[i] <= k;
- invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
+
+ method RoundDown(k: int) returns (r: int)
+ requires Valid();
+ ensures -1 <= r < thresholds.Length;
+ ensures forall m :: r < m < thresholds.Length ==> k < thresholds[m];
+ ensures 0 <= r ==> thresholds[r] <= k;
{
- var mid := i + (j - i + 1) / 2;
- assert i < mid <= j;
- if (thresholds[mid] <= k) {
- i := mid;
- } else {
- j := mid - 1;
+ if (thresholds.Length == 0 || k < thresholds[0]) {
+ return -1;
}
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant thresholds[i] <= k;
+ invariant forall m :: j < m < thresholds.Length ==> k < thresholds[m];
+ {
+ var mid := i + (j - i + 1) / 2;
+ assert i < mid <= j;
+ if (thresholds[mid] <= k) {
+ i := mid;
+ } else {
+ j := mid - 1;
+ }
+ }
+ return i;
}
- return i;
-}
-method RoundUp(k: int) returns (r: int)
- requires Valid();
- ensures 0 <= r <= thresholds.Length;
- ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
- ensures r < thresholds.Length ==> k <= thresholds[r];
-{
- if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
- return thresholds.Length;
- }
- var i, j := 0, thresholds.Length - 1;
- while (i < j)
- invariant 0 <= i <= j < thresholds.Length;
- invariant k <= thresholds[j];
- invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
+ method RoundUp(k: int) returns (r: int)
+ requires Valid();
+ ensures 0 <= r <= thresholds.Length;
+ ensures forall m :: 0 <= m < r ==> thresholds[m] < k;
+ ensures r < thresholds.Length ==> k <= thresholds[r];
{
- var mid := i + (j - i) / 2;
- assert i <= mid < j;
- if (thresholds[mid] < k) {
- i := mid + 1;
- } else {
- j := mid;
+ if (thresholds.Length == 0 || thresholds[thresholds.Length-1] < k) {
+ return thresholds.Length;
+ }
+ var i, j := 0, thresholds.Length - 1;
+ while (i < j)
+ invariant 0 <= i <= j < thresholds.Length;
+ invariant k <= thresholds[j];
+ invariant forall m :: 0 <= m < i ==> thresholds[m] < k;
+ {
+ var mid := i + (j - i) / 2;
+ assert i <= mid < j;
+ if (thresholds[mid] < k) {
+ i := mid + 1;
+ } else {
+ j := mid;
+ }
}
+ return i;
}
- return i;
}
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 2244f37f..7ea038be 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -3,23 +3,23 @@ abstract module TotalOrder {
type T // the type to be compared
- static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
+ predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
// Three properties of total orders. Here, they are given as unproved
// lemmas, that is, as axioms.
- static lemma Antisymmetry(a: T, b: T)
+ lemma Antisymmetry(a: T, b: T)
requires Leq(a, b) && Leq(b, a);
ensures a == b;
- static lemma Transitivity(a: T, b: T, c: T)
+ lemma Transitivity(a: T, b: T, c: T)
requires Leq(a, b) && Leq(b, c);
ensures Leq(a, c);
- static lemma Totality(a: T, b: T)
+ lemma Totality(a: T, b: T)
ensures Leq(a, b) || Leq(b, a);
}
abstract module Sort {
import O as TotalOrder // let O denote some module that has the members of TotalOrder
- static predicate Sorted(a: array<O.T>, low: int, high: int)
+ predicate Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
// The body of the predicate is hidden outside the module, but the postcondition is
@@ -32,7 +32,7 @@ abstract module Sort { // In the insertion sort routine below, it's more convenient to keep track of only that
// neighboring elements of the array are sorted...
- static predicate NeighborSorted(a: array<O.T>, low: int, high: int)
+ predicate NeighborSorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
reads a;
{
@@ -40,7 +40,7 @@ abstract module Sort { }
// ...but we show that property to imply all pairs to be sorted. The proof of this
// lemma uses the transitivity property.
- static lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)
+ lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)
requires a != null && 0 <= low <= high <= a.Length;
requires NeighborSorted(a, low, high);
ensures Sorted(a, low, high);
@@ -56,7 +56,7 @@ abstract module Sort { }
// Standard insertion sort method
- static method InsertionSort(a: array<O.T>)
+ method InsertionSort(a: array<O.T>)
requires a != null;
modifies a;
ensures Sorted(a, 0, a.Length);
@@ -96,30 +96,30 @@ module IntOrder refines TotalOrder { // (If there were type synonyms, we could perhaps have written just "type T = int".)
datatype T = Int(i: int)
// Define the ordering on these integers
- static predicate method Leq ...
+ predicate method Leq ...
ensures Leq(a, b) ==> a.i <= b.i;
{
a.i <= b.i
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
// Another example of a TotalOrder. Now we can sort pairs of integers.
// Lexiographic ordering of pairs of integers
module IntLexOrder refines TotalOrder {
datatype T = Int(i: int, j: int)
- static predicate method Leq ... {
+ predicate method Leq ... {
if a.i < b.i then true
else if a.i == b.i then a.j <= b.j
else false
}
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
@@ -129,7 +129,7 @@ module Client { import O = IntOrder
}
import I = IntOrder
- static method TheMain() {
+ method TheMain() {
var a := new I.T[4];
a[0] := I.T.Int(6); // alternatively, we could have written the RHS as: IntSort.O.T.Int(6)
a[1] := I.T.Int(1);
@@ -155,16 +155,16 @@ module intOrder refines TotalOrder { // Instantiate type T with a datatype wrapper around an integer.
type T = int
// Define the ordering on these integers
- static predicate method Leq ...
+ predicate method Leq ...
ensures Leq(a, b) ==> a <= b;
{
a <= b
}
// The three required properties of the order are proved here as lemmas.
// The proofs are automatic and don't require any further assistance.
- static lemma Antisymmetry ... { }
- static lemma Transitivity ... { }
- static lemma Totality ... { }
+ lemma Antisymmetry ... { }
+ lemma Transitivity ... { }
+ lemma Totality ... { }
}
module AnotherClient {
@@ -172,7 +172,7 @@ module AnotherClient { import O = intOrder
}
import I = intOrder
- static method TheMain() {
+ method TheMain() {
var a := new int[4]; // alternatively, could have written 'new I.T[4]'
a[0] := 6;
a[1] := 1;
diff --git a/Test/hofs/Monads.dfy b/Test/hofs/Monads.dfy index 9e7c5460..a221f818 100644 --- a/Test/hofs/Monads.dfy +++ b/Test/hofs/Monads.dfy @@ -4,22 +4,22 @@ abstract module Monad { type M<A>; - static function method Return(x: A): M<A> - static function method Bind(m: M<A>, f:A -> M<B>):M<B> + function method Return(x: A): M<A> + function method Bind(m: M<A>, f:A -> M<B>):M<B> reads f.reads; requires forall a :: f.requires(a); // return x >>= f = f x - static lemma LeftIdentity(x : A, f : A -> M<B>) + lemma LeftIdentity(x : A, f : A -> M<B>) requires forall a :: f.requires(a); ensures Bind(Return(x),f) == f(x); // m >>= return = m - static lemma RightIdentity(m : M<A>) + lemma RightIdentity(m : M<A>) ensures Bind(m,Return) == m; // (m >>= f) >>= g = m >>= (x => f(x) >>= g) - static lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity(m : M<A>, f:A -> M<B>, g: B -> M<C>) requires forall a :: f.requires(a); requires forall b :: g.requires(b); ensures Bind(Bind(m,f),g) == @@ -32,24 +32,24 @@ abstract module Monad { module Identity refines Monad { datatype M<A> = I(A); - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { I(x) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { var I(x) := m; f(x) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { assert Bind(m,Return) == m; } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { assert Bind(Bind(m,f),g) == @@ -64,26 +64,26 @@ module Identity refines Monad { module Maybe refines Monad { datatype M<A> = Just(A) | Nothing; - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { Just(x) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { match m case Nothing => Nothing case Just(x) => f(x) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { assert Bind(m,Return) == m; } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { assert Bind(Bind(m,f),g) == @@ -98,24 +98,24 @@ module Maybe refines Monad { module List refines Monad { datatype M<A> = Cons(hd: A,tl: M<A>) | Nil; - static function method Return<A>(x: A): M<A> + function method Return<A>(x: A): M<A> { Cons(x,Nil) } - static function method Concat(xs: M<A>, ys: M<A>): M<A> + function method Concat(xs: M<A>, ys: M<A>): M<A> { match xs case Nil => ys case Cons(x,xs) => Cons(x,Concat(xs,ys)) } - static function method Join(xss: M<M<A>>) : M<A> + function method Join(xss: M<M<A>>) : M<A> { match xss case Nil => Nil case Cons(xs,xss) => Concat(xs,Join(xss)) } - static function method Map(xs: M<A>, f: A -> B):M<B> + function method Map(xs: M<A>, f: A -> B):M<B> reads f.reads; requires forall a :: f.requires(a); { @@ -124,12 +124,12 @@ module List refines Monad { case Cons(x,xs) => Cons(f(x),Map(xs,f)) } - static function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> + function method Bind<A,B>(m: M<A>, f:A -> M<B>):M<B> { Join(Map(m,f)) } - static lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) + lemma LeftIdentity<A,B>(x : A, f : A -> M<B>) { calc { Bind(Return(x),f); @@ -141,7 +141,7 @@ module List refines Monad { } } - static lemma RightIdentity<A>(m : M<A>) + lemma RightIdentity<A>(m : M<A>) { match m case Nil => calc { @@ -166,11 +166,11 @@ module List refines Monad { } } - static lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>) + lemma ConcatAssociativity<A>(xs : M<A>, ys : M<A>, zs: M<A>) ensures Concat(Concat(xs,ys),zs) == Concat(xs,Concat(ys,zs)); {} - static lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>) + lemma BindMorphism(xs : M<A>, ys: M<A>, f : A -> M<B>) requires forall a :: f.requires(a); ensures Bind(Concat(xs,ys),f) == Concat(Bind(xs,f),Bind(ys,f)); { @@ -194,7 +194,7 @@ module List refines Monad { } } - static lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) + lemma Associativity<A,B,C>(m : M<A>, f:A -> M<B>, g: B -> M<C>) { match m case Nil => calc { diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 1e54f02f..e9280a9a 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -104,7 +104,7 @@ class SparseArray<T> { }
/* The following method is here only to simulate support of arrays in Dafny */
-/*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+/*private*/ method AllocateArray<G>(n: int) returns (arr: seq<G>)
requires 0 <= n;
ensures |arr| == n;
{
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index 2d724b54..b111a438 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -231,21 +231,21 @@ class BreadthFirstSearch<Vertex(==)> }
}
-static function domain<T, U>(m: map<T, U>): set<T>
+function domain<T, U>(m: map<T, U>): set<T>
{
set t | t in m
}
datatype List<T> = Nil | Cons(head: T, tail: List)
-static function length(list: List): nat
+function length(list: List): nat
{
match list
case Nil => 0
case Cons(_, tail) => 1 + length(tail)
}
-static function elements<T>(list: List<T>): set<T>
+function elements<T>(list: List<T>): set<T>
{
match list
case Nil => {}
|