From cb20c2a781055190994851bb375828db642fa271 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 11 Jul 2011 19:08:48 -0700 Subject: Dafny: allow constructors only inside classes, removed semi-colons at end of body-less functions/methods --- Source/Dafny/Dafny.atg | 35 ++-- Source/Dafny/Parser.cs | 363 +++++++++++++++++++--------------------- Source/Dafny/Printer.cs | 4 +- Source/Dafny/Scanner.cs | 102 ++++++----- Test/VSI-Benchmarks/b3.dfy | 9 +- Test/VSI-Benchmarks/b7.dfy | 8 +- Test/VSI-Benchmarks/b8.dfy | 30 ++-- Test/dafny0/Definedness.dfy | 8 +- Test/dafny0/NatTypes.dfy | 2 +- Test/dafny0/Termination.dfy | 2 +- Test/dafny0/TypeAntecedents.dfy | 2 +- Test/dafny0/TypeParameters.dfy | 10 +- Test/dafny1/Celebrity.dfy | 2 +- Test/dafny1/Rippling.dfy | 4 +- Test/dafny1/UltraFilter.dfy | 2 +- 15 files changed, 284 insertions(+), 299 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f6e40722..15d39460 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -188,7 +188,7 @@ Dafny theModules.Add(module); .) | ClassDecl (. defaultModule.TopLevelDecls.Add(c); .) | DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .) - | ClassMemberDecl + | ClassMemberDecl } (. if (defaultModuleCreatedHere) { defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass)); @@ -225,7 +225,7 @@ ClassDecl [ "refines" Ident (. optionalId = idRefined; .) ] "{" (. bodyStart = t; .) - { ClassMemberDecl + { ClassMemberDecl } "}" (. if (optionalId == null) @@ -237,7 +237,7 @@ ClassDecl .) . -ClassMemberDecl<.List/*!*/ mm.> +ClassMemberDecl<.List/*!*/ mm, bool allowConstructors.> = (. Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -248,8 +248,8 @@ ClassMemberDecl<.List/*!*/ mm.> | "unlimited" (. mmod.IsUnlimited = true; .) } ( FieldDecl - | FunctionDecl (. mm.Add(f); .) - | MethodDecl (. mm.Add(m); .) + | FunctionDecl (. mm.Add(f); .) + | MethodDecl (. mm.Add(m); .) | CouplingInvDecl ) . @@ -404,7 +404,7 @@ GenericParameters<.List/*!*/ typeArgs.> /*------------------------------------------------------------------------*/ -MethodDecl +MethodDecl = (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null); IToken/*!*/ id; Attributes attrs = null; @@ -422,8 +422,13 @@ MethodDecl IToken bodyEnd = Token.NoToken; .) ( "method" - | "constructor" (. isConstructor = true; .) - | "refines" (. isRefinement = true; .) + | "constructor" (. if (allowConstructor) { + isConstructor = true; + } else { + SemErr(t, "constructors are only allowed in classes"); + } + .) + | "refines" (. isRefinement = true; .) ) (. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); } if (isConstructor) { @@ -443,9 +448,9 @@ MethodDecl Formals ] - ( ";" { MethodSpec } - | { MethodSpec } BlockStmt (. body = (BlockStmt)bb; .) - ) + { MethodSpec } + [ BlockStmt (. body = (BlockStmt)bb; .) + ] (. if (isRefinement) m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs); @@ -588,11 +593,9 @@ FunctionDecl Formals ":" Type - ( ";" - { FunctionSpec } - | { FunctionSpec } - FunctionBody (. body = bb; .) - ) + { FunctionSpec } + [ FunctionBody (. body = bb; .) + ] (. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs); f.BodyStartTok = bodyStart; f.BodyEndTok = bodyEnd; diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index e12ab7e3..42014762 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -25,7 +25,7 @@ public class Parser { const bool T = true; const bool x = false; const int minErrDist = 2; - + public Scanner/*!*/ scanner; public Errors/*!*/ errors; @@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List= minErrDist) errors.SemErr(t, msg); errDist = 0; } - - public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { - Contract.Requires(tok != null); - Contract.Requires(msg != null); + + public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); errors.SemErr(tok, msg); } @@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List theImports; @@ -246,7 +246,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ mm) { + void ClassMemberDecl(List/*!*/ mm, bool allowConstructors) { Contract.Requires(cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; @@ -383,7 +383,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; Expect(33); - if (StartOf(7)) { + if (StartOf(5)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); while (la.kind == 19) { @@ -734,7 +729,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List/*!*/ decreases) { if (la.kind == 28) { Get(); - if (StartOf(8)) { + if (StartOf(6)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 19) { @@ -785,12 +780,12 @@ List/*!*/ decreases) { Expression(out e); Expect(17); ens.Add(new MaybeFreeExpression(e, isFree)); - } else SynErr(110); + } else SynErr(108); } else if (la.kind == 32) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(111); + } else SynErr(109); } void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -799,7 +794,7 @@ List/*!*/ decreases) { Expect(7); bodyStart = t; - while (StartOf(9)) { + while (StartOf(7)) { Stmt(body); } Expect(8); @@ -880,7 +875,7 @@ List/*!*/ decreases) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt); - } else SynErr(112); + } else SynErr(110); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { @@ -893,7 +888,7 @@ List/*!*/ decreases) { reqs.Add(e); } else if (la.kind == 42) { Get(); - if (StartOf(10)) { + if (StartOf(8)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); while (la.kind == 19) { @@ -912,7 +907,7 @@ List/*!*/ decreases) { Get(); DecreasesList(decreases, false); Expect(17); - } else SynErr(113); + } else SynErr(111); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -929,9 +924,9 @@ List/*!*/ decreases) { if (la.kind == 43) { Get(); fe = new FrameExpression(new WildcardExpr(t), null); - } else if (StartOf(8)) { + } else if (StartOf(6)) { FrameExpression(out fe); - } else SynErr(114); + } else SynErr(112); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -940,9 +935,9 @@ List/*!*/ decreases) { if (la.kind == 43) { Get(); e = new WildcardExpr(t); - } else if (StartOf(8)) { + } else if (StartOf(6)) { Expression(out e); - } else SynErr(115); + } else SynErr(113); } void Stmt(List/*!*/ ss) { @@ -1019,7 +1014,7 @@ List/*!*/ decreases) { Get(); breakCount++; } - } else SynErr(116); + } else SynErr(114); Expect(17); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; @@ -1028,7 +1023,7 @@ List/*!*/ decreases) { ReturnStmt(out s); break; } - default: SynErr(117); break; + default: SynErr(115); break; } } @@ -1099,7 +1094,7 @@ List/*!*/ decreases) { } else if (la.kind == 22) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(118); + } else SynErr(116); s = new UpdateStmt(x, lhss, rhss); } @@ -1172,13 +1167,13 @@ List/*!*/ decreases) { } else if (la.kind == 7) { BlockStmt(out s, out bodyStart, out bodyEnd); els = s; - } else SynErr(119); + } else SynErr(117); } ifStmt = new IfStmt(x, guard, thn, els); } else if (la.kind == 7) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(120); + } else SynErr(118); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1200,11 +1195,11 @@ List/*!*/ decreases) { LoopSpec(out invariants, out decreases, out mod); BlockStmt(out body, out bodyStart, out bodyEnd); stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); - } else if (StartOf(11)) { + } else if (StartOf(9)) { LoopSpec(out invariants, out decreases, out mod); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); - } else SynErr(121); + } else SynErr(119); } void MatchStmt(out Statement/*!*/ s) { @@ -1278,7 +1273,7 @@ List/*!*/ decreases) { Expect(47); returnTok = t; - if (StartOf(12)) { + if (StartOf(10)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); while (la.kind == 19) { @@ -1316,7 +1311,7 @@ List/*!*/ decreases) { Ident(out x); Expect(33); args = new List(); - if (StartOf(8)) { + if (StartOf(6)) { Expressions(args); } Expect(34); @@ -1338,10 +1333,10 @@ List/*!*/ decreases) { } else if (la.kind == 43) { Get(); r = new HavocRhs(t); - } else if (StartOf(8)) { + } else if (StartOf(6)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(122); + } else SynErr(120); } void Lhs(out Expression e) { @@ -1352,13 +1347,13 @@ List/*!*/ decreases) { while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } - } else if (StartOf(13)) { + } else if (StartOf(11)) { ConstAtomExpression(out e); Suffix(ref e); while (la.kind == 50 || la.kind == 52) { Suffix(ref e); } - } else SynErr(123); + } else SynErr(121); } void Expressions(List/*!*/ args) { @@ -1378,10 +1373,10 @@ List/*!*/ decreases) { if (la.kind == 43) { Get(); e = null; - } else if (StartOf(8)) { + } else if (StartOf(6)) { Expression(out ee); e = ee; - } else SynErr(124); + } else SynErr(122); Expect(34); } @@ -1398,7 +1393,7 @@ List/*!*/ decreases) { Expression(out e); Expect(57); body = new List(); - while (StartOf(9)) { + while (StartOf(7)) { Stmt(body); } alternatives.Add(new GuardedAlternative(x, e, body)); @@ -1412,7 +1407,7 @@ List/*!*/ decreases) { decreases = new List(); mod = null; - while (StartOf(14)) { + while (StartOf(12)) { if (la.kind == 29 || la.kind == 59) { isFree = false; if (la.kind == 29) { @@ -1430,7 +1425,7 @@ List/*!*/ decreases) { } else { Get(); mod = mod ?? new List(); - if (StartOf(8)) { + if (StartOf(6)) { FrameExpression(out fe); mod.Add(fe); while (la.kind == 19) { @@ -1465,7 +1460,7 @@ List/*!*/ decreases) { Expect(34); } Expect(57); - while (StartOf(9)) { + while (StartOf(7)) { Stmt(body); } c = new MatchCaseStmt(x, id.val, arguments, body); @@ -1476,10 +1471,10 @@ List/*!*/ decreases) { if (la.kind == 4) { Get(); arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); - } else if (StartOf(8)) { + } else if (StartOf(6)) { Expression(out e); arg = new Attributes.Argument(e); - } else SynErr(125); + } else SynErr(123); } void EquivExpression(out Expression/*!*/ e0) { @@ -1509,13 +1504,13 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 67) { Get(); - } else SynErr(126); + } else SynErr(124); } void LogicalExpression(out Expression/*!*/ e0) { Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; RelationalExpression(out e0); - if (StartOf(15)) { + if (StartOf(13)) { if (la.kind == 70 || la.kind == 71) { AndOp(); x = t; @@ -1547,7 +1542,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 69) { Get(); - } else SynErr(127); + } else SynErr(125); } void RelationalExpression(out Expression/*!*/ e) { @@ -1564,15 +1559,15 @@ List/*!*/ decreases) { Term(out e0); e = e0; - if (StartOf(16)) { + if (StartOf(14)) { RelOp(out x, out op); firstOpTok = x; Term(out e1); e = new BinaryExpr(x, op, e0, e1); if (op == BinaryExpr.Opcode.Disjoint) - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands. - while (StartOf(16)) { + while (StartOf(14)) { if (chain == null) { chain = new List(); ops = new List(); @@ -1603,36 +1598,35 @@ List/*!*/ decreases) { break; case BinaryExpr.Opcode.Neq: if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); } - if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); } - hasSeenNeq = true; break; - case BinaryExpr.Opcode.Lt: - case BinaryExpr.Opcode.Le: - if (kind == 0) { kind = 1; } - else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); } - break; - case BinaryExpr.Opcode.Gt: - case BinaryExpr.Opcode.Ge: - if (kind == 0) { kind = 2; } - else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); } - break; - case BinaryExpr.Opcode.Disjoint: - if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; } - break; - default: - SemErr(x, "this operator cannot be part of a chain"); - kind = 3; break; - } - + if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); } + hasSeenNeq = true; break; + case BinaryExpr.Opcode.Lt: + case BinaryExpr.Opcode.Le: + if (kind == 0) { kind = 1; } + else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); } + break; + case BinaryExpr.Opcode.Gt: + case BinaryExpr.Opcode.Ge: + if (kind == 0) { kind = 2; } + else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); } + break; + case BinaryExpr.Opcode.Disjoint: + if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; } + break; + default: + SemErr(x, "this operator cannot be part of a chain"); + kind = 3; break; + } + Term(out e1); ops.Add(op); chain.Add(e1); - if (op == BinaryExpr.Opcode.Disjoint) - { + if (op == BinaryExpr.Opcode.Disjoint) { e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1)); - acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. - } - else - e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); - + acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added. + } + else + e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1)); + } } if (chain != null) { @@ -1646,7 +1640,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 71) { Get(); - } else SynErr(128); + } else SynErr(126); } void OrOp() { @@ -1654,7 +1648,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 73) { Get(); - } else SynErr(129); + } else SynErr(127); } void Term(out Expression/*!*/ e0) { @@ -1730,7 +1724,7 @@ List/*!*/ decreases) { x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(130); break; + default: SynErr(128); break; } } @@ -1752,7 +1746,7 @@ List/*!*/ decreases) { } else if (la.kind == 84) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(131); + } else SynErr(129); } void UnaryExpression(out Expression/*!*/ e) { @@ -1794,7 +1788,7 @@ List/*!*/ decreases) { } break; } - default: SynErr(132); break; + default: SynErr(130); break; } } @@ -1809,7 +1803,7 @@ List/*!*/ decreases) { } else if (la.kind == 86) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(133); + } else SynErr(131); } void NegOp() { @@ -1817,7 +1811,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 88) { Get(); - } else SynErr(134); + } else SynErr(132); } void EndlessExpression(out Expression e) { @@ -1836,11 +1830,11 @@ List/*!*/ decreases) { e = new ITEExpr(x, e, e0, e1); } else if (la.kind == 60) { MatchExpression(out e); - } else if (StartOf(17)) { + } else if (StartOf(15)) { QuantifierGuts(out e); } else if (la.kind == 38) { ComprehensionExpr(out e); - } else SynErr(135); + } else SynErr(133); } void DottedIdentifiersAndFunction(out Expression e) { @@ -1858,7 +1852,7 @@ List/*!*/ decreases) { if (la.kind == 33) { Get(); openParen = t; args = new List(); - if (StartOf(8)) { + if (StartOf(6)) { Expressions(args); } Expect(34); @@ -1878,7 +1872,7 @@ List/*!*/ decreases) { if (la.kind == 33) { Get(); args = new List(); func = true; - if (StartOf(8)) { + if (StartOf(6)) { Expressions(args); } Expect(34); @@ -1888,13 +1882,13 @@ List/*!*/ decreases) { } else if (la.kind == 50) { Get(); x = t; - if (StartOf(8)) { + if (StartOf(6)) { Expression(out ee); e0 = ee; if (la.kind == 97) { Get(); anyDots = true; - if (StartOf(8)) { + if (StartOf(6)) { Expression(out ee); e1 = ee; } @@ -1913,12 +1907,12 @@ List/*!*/ decreases) { multipleIndices.Add(ee); } - } else SynErr(136); + } else SynErr(134); } else if (la.kind == 97) { Get(); Expression(out ee); anyDots = true; e1 = ee; - } else SynErr(137); + } else SynErr(135); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -1942,7 +1936,7 @@ List/*!*/ decreases) { } Expect(51); - } else SynErr(138); + } else SynErr(136); } void DisplayExpr(out Expression e) { @@ -1953,7 +1947,7 @@ List/*!*/ decreases) { if (la.kind == 7) { Get(); x = t; elements = new List(); - if (StartOf(8)) { + if (StartOf(6)) { Expressions(elements); } e = new SetDisplayExpr(x, elements); @@ -1961,12 +1955,12 @@ List/*!*/ decreases) { } else if (la.kind == 50) { Get(); x = t; elements = new List(); - if (StartOf(8)) { + if (StartOf(6)) { Expressions(elements); } e = new SeqDisplayExpr(x, elements); Expect(51); - } else SynErr(139); + } else SynErr(137); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2043,7 +2037,7 @@ List/*!*/ decreases) { Expect(34); break; } - default: SynErr(140); break; + default: SynErr(138); break; } } @@ -2088,7 +2082,7 @@ List/*!*/ decreases) { } else if (la.kind == 100 || la.kind == 101) { Exists(); x = t; - } else SynErr(141); + } else SynErr(139); IdentTypeOptional(out bv); bvars.Add(bv); while (la.kind == 19) { @@ -2170,7 +2164,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 99) { Get(); - } else SynErr(142); + } else SynErr(140); } void Exists() { @@ -2178,7 +2172,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 101) { Get(); - } else SynErr(143); + } else SynErr(141); } void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) { @@ -2187,11 +2181,11 @@ List/*!*/ decreases) { Expect(7); if (la.kind == 22) { AttributeBody(ref attrs); - } else if (StartOf(8)) { + } else if (StartOf(6)) { es = new List(); Expressions(es); trigs = new Triggers(es, trigs); - } else SynErr(144); + } else SynErr(142); Expect(8); } @@ -2200,7 +2194,7 @@ List/*!*/ decreases) { Get(); } else if (la.kind == 103) { Get(); - } else SynErr(145); + } else SynErr(143); } void AttributeBody(ref Attributes attrs) { @@ -2211,7 +2205,7 @@ List/*!*/ decreases) { Expect(22); Expect(1); aName = t.val; - if (StartOf(18)) { + if (StartOf(16)) { AttributeArg(out aArg); aArgs.Add(aArg); while (la.kind == 19) { @@ -2227,21 +2221,19 @@ List/*!*/ decreases) { public void Parse() { la = new Token(); - la.val = ""; + la.val = ""; Get(); Dafny(); - Expect(0); + Expect(0); } - + static readonly bool[,]/*!*/ set = { {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, - {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x}, {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}, {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}, @@ -2262,20 +2254,18 @@ List/*!*/ decreases) { public class Errors { public int count = 0; // number of errors detected public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream - public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text - public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text - + public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text + public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text + public void SynErr(string filename, int line, int col, int n) { - SynErr(filename, line, col, GetSyntaxErrorString(n)); - } - - public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + SynErr(filename, line, col, GetSyntaxErrorString(n)); + } + public virtual void SynErr(string filename, int line, int col, string msg) { + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; - } - - string GetSyntaxErrorString(int n) { + } + string GetSyntaxErrorString(int n) { string s; switch (n) { case 0: s = "EOF expected"; break; @@ -2384,50 +2374,48 @@ public class Errors { case 103: s = "\"\\u2022\" expected"; break; case 104: s = "??? expected"; break; case 105: s = "invalid ClassMemberDecl"; break; - case 106: s = "invalid FunctionDecl"; break; - case 107: s = "invalid MethodDecl"; break; - case 108: s = "invalid MethodDecl"; break; - case 109: s = "invalid TypeAndToken"; break; - case 110: s = "invalid MethodSpec"; break; - case 111: s = "invalid MethodSpec"; break; - case 112: s = "invalid ReferenceType"; break; - case 113: s = "invalid FunctionSpec"; break; - case 114: s = "invalid PossiblyWildFrameExpression"; break; - case 115: s = "invalid PossiblyWildExpression"; break; - case 116: s = "invalid OneStmt"; break; - case 117: s = "invalid OneStmt"; break; - case 118: s = "invalid UpdateStmt"; break; - case 119: s = "invalid IfStmt"; break; - case 120: s = "invalid IfStmt"; break; - case 121: s = "invalid WhileStmt"; break; - case 122: s = "invalid Rhs"; break; - case 123: s = "invalid Lhs"; break; - case 124: s = "invalid Guard"; break; - case 125: s = "invalid AttributeArg"; break; - case 126: s = "invalid EquivOp"; break; - case 127: s = "invalid ImpliesOp"; break; - case 128: s = "invalid AndOp"; break; - case 129: s = "invalid OrOp"; break; - case 130: s = "invalid RelOp"; break; - case 131: s = "invalid AddOp"; break; - case 132: s = "invalid UnaryExpression"; break; - case 133: s = "invalid MulOp"; break; - case 134: s = "invalid NegOp"; break; - case 135: s = "invalid EndlessExpression"; break; + case 106: s = "invalid MethodDecl"; break; + case 107: s = "invalid TypeAndToken"; break; + case 108: s = "invalid MethodSpec"; break; + case 109: s = "invalid MethodSpec"; break; + case 110: s = "invalid ReferenceType"; break; + case 111: s = "invalid FunctionSpec"; break; + case 112: s = "invalid PossiblyWildFrameExpression"; break; + case 113: s = "invalid PossiblyWildExpression"; break; + case 114: s = "invalid OneStmt"; break; + case 115: s = "invalid OneStmt"; break; + case 116: s = "invalid UpdateStmt"; break; + case 117: s = "invalid IfStmt"; break; + case 118: s = "invalid IfStmt"; break; + case 119: s = "invalid WhileStmt"; break; + case 120: s = "invalid Rhs"; break; + case 121: s = "invalid Lhs"; break; + case 122: s = "invalid Guard"; break; + case 123: s = "invalid AttributeArg"; break; + case 124: s = "invalid EquivOp"; break; + case 125: s = "invalid ImpliesOp"; break; + case 126: s = "invalid AndOp"; break; + case 127: s = "invalid OrOp"; break; + case 128: s = "invalid RelOp"; break; + case 129: s = "invalid AddOp"; break; + case 130: s = "invalid UnaryExpression"; break; + case 131: s = "invalid MulOp"; break; + case 132: s = "invalid NegOp"; break; + case 133: s = "invalid EndlessExpression"; break; + case 134: s = "invalid Suffix"; break; + case 135: s = "invalid Suffix"; break; case 136: s = "invalid Suffix"; break; - case 137: s = "invalid Suffix"; break; - case 138: s = "invalid Suffix"; break; - case 139: s = "invalid DisplayExpr"; break; - case 140: s = "invalid ConstAtomExpression"; break; - case 141: s = "invalid QuantifierGuts"; break; - case 142: s = "invalid Forall"; break; - case 143: s = "invalid Exists"; break; - case 144: s = "invalid AttributeOrTrigger"; break; - case 145: s = "invalid QSep"; break; + case 137: s = "invalid DisplayExpr"; break; + case 138: s = "invalid ConstAtomExpression"; break; + case 139: s = "invalid QuantifierGuts"; break; + case 140: s = "invalid Forall"; break; + case 141: s = "invalid Exists"; break; + case 142: s = "invalid AttributeOrTrigger"; break; + case 143: s = "invalid QSep"; break; default: s = "error " + n; break; } - return s; + return s; } public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors @@ -2435,9 +2423,8 @@ public class Errors { Contract.Requires(msg != null); SemErr(tok.filename, tok.line, tok.col, msg); } - public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) { - Contract.Requires(msg != null); + Contract.Requires(msg != null); errorStream.WriteLine(errMsgFormat, filename, line, col, msg); count++; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index e49ce6e9..b9c8601e 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -230,7 +230,7 @@ namespace Microsoft.Dafny { PrintFormals(f.Formals); wr.Write(": "); PrintType(f.ResultType); - wr.WriteLine(f.Body == null ? ";" : ""); + wr.WriteLine(); int ind = indent + IndentAmount; PrintSpec("requires", f.Req, ind); @@ -277,7 +277,7 @@ namespace Microsoft.Dafny { } PrintFormals(method.Outs); } - wr.WriteLine(method.Body == null ? ";" : ""); + wr.WriteLine(); int ind = indent + IndentAmount; PrintSpec("requires", method.Req, ind); diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 81f556c8..19157a32 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -19,7 +19,7 @@ public class Buffer { // a) whole stream in buffer // b) part of stream in buffer // 2) non seekable stream (network, console) - + public const int EOF = 65535 + 1; // char.MaxValue + 1; const int MIN_BUFFER_LENGTH = 1024; // 1KB const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB @@ -31,17 +31,15 @@ public class Buffer { Stream/*!*/ stream; // input stream (seekable) bool isUserStream; // was the stream opened by the user? - [ContractInvariantMethod] - void ObjectInvariant(){ - Contract.Invariant(buf != null); - Contract.Invariant(stream != null); - } - -// [NotDelayed] - public Buffer (Stream/*!*/ s, bool isUserStream) : base() { +[ContractInvariantMethod] +void ObjectInvariant(){ + Contract.Invariant(buf != null); + Contract.Invariant(stream != null);} + [NotDelayed] + public Buffer (Stream/*!*/ s, bool isUserStream) :base() { Contract.Requires(s != null); stream = s; this.isUserStream = isUserStream; - + int fl, bl; if (s.CanSeek) { fl = (int) s.Length; @@ -53,12 +51,12 @@ public class Buffer { buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH]; fileLen = fl; bufLen = bl; - + if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start) else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid if (bufLen == fileLen && s.CanSeek) Close(); } - + protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor Contract.Requires(b != null); buf = b.buf; @@ -75,14 +73,14 @@ public class Buffer { } ~Buffer() { Close(); } - + protected void Close() { if (!isUserStream && stream != null) { stream.Close(); //stream = null; } } - + public virtual int Read () { if (bufPos < bufLen) { return buf[bufPos++]; @@ -102,7 +100,7 @@ public class Buffer { Pos = curPos; return ch; } - + public string/*!*/ GetString (int beg, int end) { Contract.Ensures(Contract.Result() != null); int len = 0; @@ -141,7 +139,7 @@ public class Buffer { } } } - + // Read the next chunk of bytes from the stream, increases the buffer // if needed and updates the fields fileLen and bufLen. // Returns the number of bytes read. @@ -215,20 +213,19 @@ public class Scanner { const int noSym = 104; - [ContractInvariantMethod] - void objectInvariant(){ - Contract.Invariant(buffer!=null); - Contract.Invariant(t != null); - Contract.Invariant(start != null); - Contract.Invariant(tokens != null); - Contract.Invariant(pt != null); - Contract.Invariant(tval != null); - Contract.Invariant(Filename != null); - Contract.Invariant(errorHandler != null); - } - +[ContractInvariantMethod] +void objectInvariant(){ + Contract.Invariant(buffer!=null); + Contract.Invariant(t != null); + Contract.Invariant(start != null); + Contract.Invariant(tokens != null); + Contract.Invariant(pt != null); + Contract.Invariant(tval != null); + Contract.Invariant(Filename != null); + Contract.Invariant(errorHandler != null); +} public Buffer/*!*/ buffer; // scanner buffer - + Token/*!*/ t; // current token int ch; // current input character int pos; // byte position of current character @@ -239,13 +236,13 @@ public class Scanner { Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy) Token/*!*/ pt; // current peek token - + char[]/*!*/ tval = new char[128]; // text of current token int tlen; // length of current token - + private string/*!*/ Filename; private Errors/*!*/ errorHandler; - + static Scanner() { start = new Hashtable(128); for (int i = 39; i <= 39; ++i) start[i] = 1; @@ -293,9 +290,9 @@ public class Scanner { start[Buffer.EOF] = -1; } - -// [NotDelayed] - public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() { + + [NotDelayed] + public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){ Contract.Requires(fileName != null); Contract.Requires(errorHandler != null); this.errorHandler = errorHandler; @@ -305,14 +302,15 @@ public class Scanner { Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read); buffer = new Buffer(stream, false); Filename = fileName; + Init(); } catch (IOException) { throw new FatalError("Cannot open file " + fileName); } } - -// [NotDelayed] - public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() { + + [NotDelayed] + public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){ Contract.Requires(s != null); Contract.Requires(errorHandler != null); Contract.Requires(fileName != null); @@ -321,9 +319,10 @@ public class Scanner { buffer = new Buffer(s, true); this.errorHandler = errorHandler; this.Filename = fileName; + Init(); } - + void Init() { pos = -1; line = 1; col = 0; oldEols = 0; @@ -344,11 +343,11 @@ public class Scanner { Contract.Ensures(Contract.Result() != null); int p = buffer.Pos; int ch = buffer.Read(); - // replace isolated '\r' by '\n' in order to make + // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; while (ch != EOL && ch != Buffer.EOF){ - ch = buffer.Read(); + ch = buffer.Read(); // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; @@ -359,7 +358,7 @@ public class Scanner { } void NextCh() { - if (oldEols > 0) { ch = EOL; oldEols--; } + if (oldEols > 0) { ch = EOL; oldEols--; } else { // pos = buffer.Pos; // ch = buffer.Read(); col++; @@ -367,9 +366,9 @@ public class Scanner { // // eol handling uniform across Windows, Unix and Mac // if (ch == '\r' && buffer.Peek() != '\n') ch = EOL; // if (ch == EOL) { line++; col = 0; } - + while (true) { - pos = buffer.Pos; + pos = buffer.Pos; ch = buffer.Read(); col++; // replace isolated '\r' by '\n' in order to make // eol handling uniform across Windows, Unix and Mac @@ -419,7 +418,7 @@ public class Scanner { return; } - + } } @@ -556,13 +555,10 @@ public class Scanner { t.pos = pos; t.col = col; t.line = line; t.filename = this.Filename; int state; - if (start.ContainsKey(ch)) { - Contract.Assert(start[ch] != null); - state = (int) start[ch]; - } + if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); } else { state = 0; } tlen = 0; AddCh(); - + switch (state) { case -1: { t.kind = eofSym; break; } // NextCh already done case 0: { @@ -768,14 +764,14 @@ public class Scanner { t.val = new String(tval, 0, tlen); return t; } - + private void SetScannerBehindT() { buffer.Pos = t.pos; NextCh(); line = t.line; col = t.col; for (int i = 0; i < tlen; i++) NextCh(); } - + // get the next token (possibly a token already seen during peeking) public Token/*!*/ Scan () { Contract.Ensures(Contract.Result() != null); @@ -796,7 +792,7 @@ public class Scanner { } pt = pt.next; } while (pt.kind > maxT); // skip pragmas - + return pt; } diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 3de94555..7cf3de07 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -12,13 +12,13 @@ class Queue { var contents: seq; - method Init(); + method Init() modifies this; ensures |contents| == 0; - method Enqueue(x: T); + method Enqueue(x: T) modifies this; ensures contents == old(contents) + [x]; - method Dequeue() returns (x: T); + method Dequeue() returns (x: T) requires 0 < |contents|; modifies this; ensures contents == old(contents)[1..] && x == old(contents)[0]; @@ -33,7 +33,7 @@ class Queue { } class Comparable { - function AtMost(c: Comparable): bool; + function AtMost(c: Comparable): bool reads this, c; } @@ -96,7 +96,6 @@ class Benchmark3 { } - method RemoveMin(q: Queue) returns (m: int, k: int) //m is the min, k is m's index in q requires q != null && |q.contents| != 0; modifies q; diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index f34f5c00..d6759c5f 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -8,13 +8,13 @@ class Queue { var contents: seq; - method Init(); + method Init() modifies this; ensures |contents| == 0; - method Enqueue(x: T); + method Enqueue(x: T) modifies this; ensures contents == old(contents) + [x]; - method Dequeue() returns (x: T); + method Dequeue() returns (x: T) requires 0 < |contents|; modifies this; ensures contents == old(contents)[1..] && x == old(contents)[0]; @@ -101,7 +101,7 @@ class Stream { class Client { - method Sort(q: Queue) returns (r: Queue, perm:seq); + method Sort(q: Queue) returns (r: Queue, perm:seq) requires q != null; modifies q; ensures r != null && fresh(r); diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 0c9d1186..383bccfd 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -6,13 +6,13 @@ class Queue { var contents: seq; - method Init(); + method Init() modifies this; ensures |contents| == 0; - method Enqueue(x: T); + method Enqueue(x: T) modifies this; ensures contents == old(contents) + [x]; - method Dequeue() returns (x: T); + method Dequeue() returns (x: T) requires 0 < |contents|; modifies this; ensures contents == old(contents)[1..] && x == old(contents)[0]; @@ -28,7 +28,7 @@ class Queue { class Glossary { - method Sort(q: Queue) returns (r: Queue, perm:seq); + method Sort(q: Queue) returns (r: Queue, perm:seq) requires q != null; modifies q; ensures r != null && fresh(r); @@ -149,29 +149,29 @@ class Glossary { class Word { - function AtMost(w:Word) :bool; + function AtMost(w: Word): bool } class ReaderStream { - ghost var footprint:set; - var isOpen:bool; + ghost var footprint: set; + var isOpen: bool; - function Valid():bool - reads this, footprint; + function Valid(): bool + reads this, footprint; { null !in footprint && this in footprint && isOpen } method Open() //reading - modifies this; - ensures Valid() && fresh(footprint -{this}); + modifies this; + ensures Valid() && fresh(footprint -{this}); { footprint := {this}; isOpen :=true; } - method GetWord()returns(x:Word) - requires Valid() ; + method GetWord() returns (x: Word) + requires Valid(); modifies footprint; ensures Valid() && fresh(footprint - old(footprint)); { @@ -190,8 +190,8 @@ class WriterStream { var stream:seq; var isOpen:bool; - function Valid():bool - reads this, footprint; + function Valid(): bool + reads this, footprint; { null !in footprint && this in footprint && isOpen } diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 8df1a7c5..2063eec4 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -44,17 +44,17 @@ class SoWellformed { c := true; } - method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed); + method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed) requires next != null; modifies this; ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null) - method Q(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed); + method Q(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed) requires next != null; modifies s; ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null) - method R(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed); + method R(a: SoWellformed, s: set) returns (c: bool, d: SoWellformed) requires next != null && this !in s; modifies s; ensures next.xyz < 100; // fine @@ -175,7 +175,7 @@ class StatementTwoShoes { } function G(w: int): int { 5 } - function method H(x: int): int; + function method H(x: int): int method V(s: set, a: int, b: int) modifies s; diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 53d3bf03..e56b4122 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -42,7 +42,7 @@ method Generic(i: int, t0: T, t1: T) returns (r: T) { r := t1; } -function method FenEric(t0: T, t1: T): T; +function method FenEric(t0: T, t1: T): T datatype Pair = Pr(T, T); diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index d4d1dfcf..f31935af 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -87,7 +87,7 @@ class Termination { } } - method Traverse(a: List) returns (val: T, b: List); + method Traverse(a: List) returns (val: T, b: List) requires a != List.Nil; ensures a == List.Cons(val, b); } diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index 2bedd37d..710e9838 100644 --- a/Test/dafny0/TypeAntecedents.dfy +++ b/Test/dafny0/TypeAntecedents.dfy @@ -88,7 +88,7 @@ method N() returns (k: MyClass) k := new MyClass; } -function NF(): MyClass; +function NF(): MyClass function TakesADatatype(a: List): int { 12 } diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index a3698dc0..8f3f8b87 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -17,7 +17,7 @@ class C { assert kz && (G() || !G()); } - function G(): Y; + function G(): Y } class SetTest { @@ -99,7 +99,7 @@ class CClient { // ------------------------- -static function IsCelebrity(c: Person, people: set): bool; +static function IsCelebrity(c: Person, people: set): bool requires c == c || c in people; method FindCelebrity3(people: set, ghost c: int) @@ -110,7 +110,7 @@ method FindCelebrity3(people: set, ghost c: int) b := F(c, people); } -static function F(c: int, people: set): bool; +static function F(c: int, people: set): bool requires IsCelebrity(c, people); function RogerThat(g: G): G @@ -153,8 +153,8 @@ method LoopyRoger(n: int) class TyKn_C { var x: T; - function G(): T; - method M() returns (t: T); + function G(): T + method M() returns (t: T) } class TyKn_K { diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 74512e01..21b895aa 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -1,6 +1,6 @@ // Celebrity example, inspired by the Rodin tutorial -static function method Knows(a: Person, b: Person): bool; +static function method Knows(a: Person, b: Person): bool requires a != b; // forbid asking about the reflexive case static function IsCelebrity(c: Person, people: set): bool diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index fdce6dc7..39e14ea5 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -163,7 +163,7 @@ function mapF(xs: List): List case Nil => Nil case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys)) } -function HardcodedUninterpretedFunction(n: Nat): Nat; +function HardcodedUninterpretedFunction(n: Nat): Nat function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List { @@ -195,7 +195,7 @@ function filterP(xs: List): List then Cons(y, filterP(ys)) else filterP(ys) } -function HardcodedUninterpretedPredicate(n: Nat): Bool; +function HardcodedUninterpretedPredicate(n: Nat): Bool function insort(n: Nat, xs: List): List { diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index 189ff2b5..c8419890 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -29,7 +29,7 @@ class UltraFilter { } // Dafny currently does not have a set comprehension expression, so this method stub will have to do - method H(f: set>, S: set, M: set) returns (h: set>); + method H(f: set>, S: set, M: set) returns (h: set>) ensures (forall X :: X in h <==> M + X in f); method Lemma_HIsFilter(h: set>, f: set>, S: set, M: set) -- cgit v1.2.3