diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 15 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 20 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 14 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 22 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 31 | ||||
| -rw-r--r-- | Test/dafny0/Computations.dfy | 23 | ||||
| -rw-r--r-- | Test/dafny0/Computations.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 22 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 32 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite-stages.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny4/NumberRepresentations.dfy | 34 |
14 files changed, 145 insertions, 90 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 5b8f8cc5..9b6d12c0 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -64,18 +64,13 @@ namespace Microsoft.Dafny body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis);
return iter;
} else if (d is ClassDecl) {
+ var dd = (ClassDecl)d;
+ var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
+ var mm = dd.Members.ConvertAll(CloneMember);
if (d is DefaultClassDecl) {
- var dd = (ClassDecl)d;
- var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
- var mm = dd.Members.ConvertAll(CloneMember);
- var cl = new DefaultClassDecl(m, mm);
- return cl;
+ return new DefaultClassDecl(m, mm);
} else {
- var dd = (ClassDecl)d;
- var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
- var mm = dd.Members.ConvertAll(CloneMember);
- var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));
- return cl;
+ return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));
}
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5c1148c6..c8f410c9 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -795,21 +795,15 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type/*!*/>/*!*/ gt;
+ List<Type> gt;
List<IToken> path;
.)
( "object" (. tok = t; ty = new ObjectType(); .)
- | arrayToken (. tok = t; gt = new List<Type/*!*/>(); .)
- GenericInstantiation<gt> (. if (gt.Count != 1) {
- SemErr("array type expects exactly one type argument");
- }
- int dims = 1;
- if (tok.val.Length != 5) {
- dims = int.Parse(tok.val.Substring(5));
- }
- ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
+ | arrayToken (. tok = t; gt = new List<Type>(); .)
+ [ GenericInstantiation<gt> ] (. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
+ ty = theBuiltIns.ArrayType(tok, dims, gt, true);
.)
- | Ident<out tok> (. gt = new List<Type/*!*/>();
+ | Ident<out tok> (. gt = new List<Type>();
path = new List<IToken>(); .)
{ (. path.Add(tok); .)
"." Ident<out tok>
@@ -1135,7 +1129,7 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall> [ "[" (. ee = new List<Expression>(); .)
Expressions<ee>
"]" (. // make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
+ var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
.)
| (. x = null; args = new List<Expression/*!*/>(); .)
[ "." Ident<out x> ]
@@ -2205,7 +2199,7 @@ Suffix<ref Expression e> (. if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
+ var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);
} else {
if (!anyDots && e0 == null) {
/* a parsing error occurred */
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 55dc973f..d72db478 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -99,7 +99,7 @@ namespace Microsoft.Dafny { SystemModule.TopLevelDecls.Add(ObjectDecl);
// add one-dimensional arrays, since they may arise during type checking
// Arrays of other dimensions may be added during parsing as the parser detects the need for these
- UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
+ UserDefinedType tmp = ArrayType(1, Type.Int, true);
// add real number functions
Function RealToInt = new Function(Token.NoToken, "RealToInt", true, true, new List<TypeParameter>(), Token.NoToken,
new List<Formal> { new Formal(Token.NoToken, "x", Type.Real, true, true) }, Type.Int, new List<Expression>(),
@@ -125,17 +125,17 @@ namespace Microsoft.Dafny { return new Attributes("compile", new List<Attributes.Argument>() { flse }, null);
}
- public UserDefinedType ArrayType(int dims, Type arg) {
- return ArrayType(Token.NoToken, dims, arg, false);
+ public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass = false) {
+ Contract.Requires(1 <= dims);
+ Contract.Requires(arg != null);
+ return ArrayType(Token.NoToken, dims, new List<Type>() { arg }, allowCreationOfNewClass);
}
- public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {
+ public UserDefinedType ArrayType(IToken tok, int dims, List<Type> typeArgs, bool allowCreationOfNewClass) {
Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
- Contract.Requires(arg != null);
+ Contract.Requires(typeArgs != null);
Contract.Ensures(Contract.Result<UserDefinedType>() != null);
- List<Type> typeArgs = new List<Type>();
- typeArgs.Add(arg);
UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule, DontCompile());
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index a7f058db..750c04d0 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1472,7 +1472,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
- List<Type/*!*/>/*!*/ gt;
+ List<Type> gt;
List<IToken> path;
if (la.kind == 60) {
@@ -1480,20 +1480,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo tok = t; ty = new ObjectType();
} else if (la.kind == 5) {
Get();
- tok = t; gt = new List<Type/*!*/>();
- GenericInstantiation(gt);
- if (gt.Count != 1) {
- SemErr("array type expects exactly one type argument");
- }
- int dims = 1;
- if (tok.val.Length != 5) {
- dims = int.Parse(tok.val.Substring(5));
+ tok = t; gt = new List<Type>();
+ if (la.kind == 38) {
+ GenericInstantiation(gt);
}
- ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
+ int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
+ ty = theBuiltIns.ArrayType(tok, dims, gt, true);
} else if (la.kind == 1) {
Ident(out tok);
- gt = new List<Type/*!*/>();
+ gt = new List<Type>();
path = new List<IToken>();
while (la.kind == 61) {
path.Add(tok);
@@ -2262,7 +2258,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ee = new List<Expression>();
Expressions(ee);
Expect(75);
- UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
+ var tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
} else {
x = null; args = new List<Expression/*!*/>();
@@ -3192,7 +3188,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);
+ var tmp = theBuiltIns.ArrayType(multipleIndices.Count, new IntType(), true);
} else {
if (!anyDots && e0 == null) {
/* a parsing error occurred */
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 73925aef..af4cad41 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3252,8 +3252,9 @@ namespace Microsoft.Dafny void ResolveCtorSignature(DatatypeCtor ctor, List<TypeParameter> dtTypeArguments) {
Contract.Requires(ctor != null);
Contract.Requires(dtTypeArguments != null);
+ var option = dtTypeArguments.Count == 0 ? ResolveTypeOption.AllowPrefixExtend : ResolveTypeOption.AllowPrefix;
foreach (Formal p in ctor.Formals) {
- ResolveType(p.tok, p.Type, ResolveTypeOption.AllowExact, dtTypeArguments);
+ ResolveType(p.tok, p.Type, option, dtTypeArguments);
}
}
@@ -3515,10 +3516,6 @@ namespace Microsoft.Dafny /// </summary>
InferTypeProxies,
/// <summary>
- /// if exactly defaultTypeArguments.Count type arguments are needed, use defaultTypeArguments
- /// </summary>
- AllowExact,
- /// <summary>
/// if at most defaultTypeArguments.Count type arguments are needed, use a prefix of defaultTypeArguments
/// </summary>
AllowPrefix,
@@ -3635,7 +3632,7 @@ namespace Microsoft.Dafny } else {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
- } else if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string')
+ } else {
TopLevelDecl d = null;
int j;
@@ -3715,8 +3712,6 @@ namespace Microsoft.Dafny for (int i = 0; i < n; i++) {
typeArgs.Add(new InferredTypeProxy());
}
- } else if (option == ResolveTypeOption.AllowExact && defaultTypeArguments.Count != n) {
- // the number of default arguments is not exactly what we need, so don't add anything
} else if (option == ResolveTypeOption.AllowPrefix && defaultTypeArguments.Count < n) {
// there aren't enough default arguments, so don't do anything
} else {
@@ -7030,7 +7025,7 @@ namespace Microsoft.Dafny // ----- root is a local variable, parameter, or bound variable
r = new IdentifierExpr(id, id.val);
ResolveExpression(r, twoState, codeContext);
- r = ResolveSuffix(r, e, 1, twoState, codeContext, allowMethodCall, out call);
+ r = ResolveSuffix(r, e, 1, twoState, codeContext, allowMethodCall, out call);
} else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 854883c8..7f29a25a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1854,7 +1854,7 @@ namespace Microsoft.Dafny { bodyWithSubst = PrefixSubstitution(pp, bodyWithSubst);
}
var etranBody = layer == null ? etran : etran.LimitedFunctions(f, new Bpl.IdentifierExpr(f.tok, layer));
- meat = BplAnd(CanCallAssumption(bodyWithSubst, etran),
+ meat = BplAnd(CanCallAssumption(bodyWithSubst, etranBody),
Bpl.Expr.Eq(funcAppl, etranBody.TrExpr(bodyWithSubst)));
}
QKeyValue kv = null;
@@ -8349,10 +8349,16 @@ namespace Microsoft.Dafny { } else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
+ bool isLit = true;
foreach (Expression ee in e.Elements) {
- Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ var rawElement = TrExpr(ee);
+ isLit = isLit && translator.IsLit(rawElement);
+ Bpl.Expr elt = BoxIfNecessary(expr.tok, rawElement, ee.Type);
s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt);
}
+ if (isLit) {
+ s = translator.Lit(s, predef.BoxType);
+ }
return s;
} else if (expr is MapDisplayExpr) {
@@ -8428,13 +8434,20 @@ namespace Microsoft.Dafny { if (e.Seq.Type.IsArrayType) {
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqFromArray, elType, HeapExpr, seq);
}
+ var isLit = translator.IsLit(seq);
if (e1 != null) {
+ isLit = isLit && translator.IsLit(e1);
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqTake, elType, seq, e1);
}
if (e0 != null) {
+ isLit = isLit && translator.IsLit(e0);
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0);
}
// if e0 == null && e1 == null, then we have the identity operation seq[..] == seq;
+ if (isLit && (e0 != null || e1 != null)) {
+ // Lit-lift the expression
+ seq = translator.Lit(seq, translator.TrType(expr.Type));
+ }
return seq;
}
@@ -8528,7 +8541,7 @@ namespace Microsoft.Dafny { args.Add(translator.CondApplyBox(expr.tok, bArg, cce.NonNull(arg.Type), t));
}
Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(dtv.tok, dtv.Ctor.FullName, predef.DatatypeType);
- Expr ret = new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
+ Bpl.Expr ret = new Bpl.NAryExpr(dtv.tok, new Bpl.FunctionCall(id), args);
if (isLit) {
ret = translator.Lit(ret, predef.DatatypeType);
}
@@ -8923,9 +8936,9 @@ namespace Microsoft.Dafny { } else if (expr is ITEExpr) {
ITEExpr e = (ITEExpr)expr;
- Bpl.Expr g = translator.RemoveLit(TrExpr(e.Test));
- Bpl.Expr thn = translator.RemoveLit(TrExpr(e.Thn));
- Bpl.Expr els = translator.RemoveLit(TrExpr(e.Els));
+ var g = translator.RemoveLit(TrExpr(e.Test));
+ var thn = translator.RemoveLit(TrExpr(e.Thn));
+ var els = translator.RemoveLit(TrExpr(e.Els));
return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List<Bpl.Expr> { g, thn, els });
} else if (expr is MatchExpr) {
@@ -9463,11 +9476,7 @@ namespace Microsoft.Dafny { }
Bpl.Expr RemoveLit(Bpl.Expr expr) {
- var e = GetLit(expr);
- if (e == null) {
- e = expr;
- }
- return e;
+ return GetLit(expr) ?? expr;
}
bool IsLit(Bpl.Expr expr) {
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy index 8050aded..83b2a571 100644 --- a/Test/dafny0/Computations.dfy +++ b/Test/dafny0/Computations.dfy @@ -184,3 +184,26 @@ ghost method test_fib3(k: nat, m: nat) var y := 12;
assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
}
+
+module NeedsAllLiteralsAxiom {
+ // The following test shows that there exist an example that
+ // benefits from the all-literals axiom. (It's not clear how
+ // important such an example is, nor is it clear what the cost
+ // of including the all-literals axiom is.)
+
+ function trick(n: nat, m: nat): nat
+ decreases n; // note that m is not included
+ {
+ if n < m || m==0 then n else trick(n-m, m) + m
+ }
+
+ lemma lemma_trick(n: nat, m: nat)
+ ensures trick(n, m) == n;
+ {
+ }
+
+ lemma calc_trick(n: nat, m: nat)
+ ensures trick(100, 10) == 100;
+ {
+ }
+}
diff --git a/Test/dafny0/Computations.dfy.expect b/Test/dafny0/Computations.dfy.expect index 85c793d4..71fc8a81 100644 --- a/Test/dafny0/Computations.dfy.expect +++ b/Test/dafny0/Computations.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 58 verified, 0 errors
+Dafny program verifier finished with 63 verified, 0 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 35c17112..74405fa5 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -943,3 +943,25 @@ method TupleResolution(x: int, y: int, r: real) var pp: (int) := x;
var qq: int := pp;
}
+
+// --- filling in type arguments and checking that there aren't too many ---
+
+module TypeArgumentCount {
+ class C<T> {
+ var f: T;
+ }
+
+ method R0(a: array3, c: C)
+
+ method R1()
+ {
+ var a: array3;
+ var c: C;
+ }
+
+ method R2<T>()
+ {
+ var a: array3<T,int>; // error: too many type arguments
+ var c: C<T,int>; // error: too many type arguments
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 22f3274e..74f4ab50 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -53,6 +53,8 @@ ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements ( 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(964,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
+ResolutionErrors.dfy(965,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
ResolutionErrors.dfy(429,2): Error: More than one default 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
@@ -139,4 +141,4 @@ ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, bu 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(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
-141 resolution/type errors detected in ResolutionErrors.dfy
+143 resolution/type errors detected in ResolutionErrors.dfy
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 963916f0..900b6110 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -321,3 +321,35 @@ method IdentityMap(s: set<Pair>) returns (m: map) m, s := m[p.0 := p.1], s - {p};
}
}
+
+// -------------- auto filled-in type arguments for array types ------
+
+module ArrayTypeMagic {
+ method M(a: array2)
+ {
+ }
+
+ method F(b: array) returns (s: seq)
+ requires b != null;
+ {
+ return b[..];
+ }
+
+ datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
+ datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)
+ datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)
+
+ function G(t: ArrayCubeTree): array3
+ {
+ match t
+ case Leaf(d) => d
+ case Node(l, _) => G(l)
+ }
+
+ datatype Nat = Zero | Succ(Nat)
+
+ datatype List<T> = Nil | Cons(T, List)
+
+ datatype Cell<T> = Mk(T)
+ datatype DList<T,U> = Nil(Cell) | Cons(T, U, DList)
+}
diff --git a/Test/dafny0/TypeParameters.dfy.expect b/Test/dafny0/TypeParameters.dfy.expect index 00efc26f..3d00e89a 100644 --- a/Test/dafny0/TypeParameters.dfy.expect +++ b/Test/dafny0/TypeParameters.dfy.expect @@ -49,4 +49,4 @@ Execution trace: TypeParameters.dfy(177,3): anon21_Else
TypeParameters.dfy(177,3): anon23_Else
-Dafny program verifier finished with 58 verified, 8 errors
+Dafny program verifier finished with 63 verified, 8 errors
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 7b2e7eda..a51a9fd0 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -176,6 +176,7 @@ abstract module M1 refines M0 { // discharge the "everything reachable is marked" postcondition, whose proof we postponed above
// by supplying an assume statement. Here, we refine that assume statement into an assert.
assert ...;
+ assume ...;
}
}
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index d7c142ee..6cb40284 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -8,6 +8,7 @@ function eval(digits: seq<int>, base: int): int
requires 2 <= base;
+ decreases digits; // see comment in test_eval()
{
if |digits| == 0 then 0 else digits[0] + base * eval(digits[1..], base)
}
@@ -16,36 +17,21 @@ lemma test_eval() {
assert forall base :: 2 <= base ==> eval([], base) == 0;
assert forall base :: 2 <= base ==> eval([0], base) == 0;
- forall base | 2 <= base {
- calc {
- eval([0, 0], base);
- 0;
- }
- }
+
+ // To prove this automatically, it is necessary that the Lit axiom is sensitive only to the
+ // 'digits' argument being a literal. Hence, the explicit 'decreases digits' clause on the
+ // 'eval' function.
+ assert forall base :: 2 <= base ==> eval([0, 0], base) == 0;
+
+ assert eval([3, 2], 10) == 23;
- calc {
- eval([3, 2], 10);
- 3 + 10 * eval([2], 10);
- 23;
- }
var oct, dec := 8, 10;
- calc {
- eval([1, 3], oct);
- 1 + oct * eval([3], oct);
- 5 + dec * eval([2], dec);
- eval([5, 2], dec);
- }
+ assert eval([1, 3], oct) == eval([5, 2], dec);
assert eval([29], 420) == 29;
assert eval([29], 8) == 29;
- calc {
- eval([-2, 1, -3], 5);
- -2 + 5 * eval([1, -3], 5);
- -2 + 5 * 1 + 25 * eval([-3], 5);
- -2 + 5 * 1 + 25 * (-3);
- -72;
- }
+ assert eval([-2, 1, -3], 5) == -72;
}
// To achieve a unique (except for leading zeros) representation of each number, we
|