summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg5
-rw-r--r--Source/Dafny/DafnyAst.ssc4
-rw-r--r--Source/Dafny/Parser.ssc3
-rw-r--r--Source/Dafny/Translator.ssc168
-rw-r--r--Test/dafny0/Answer34
-rw-r--r--Test/dafny0/SumOfCubes.dfy110
-rw-r--r--Test/dafny0/UnboundedStack.dfy98
-rw-r--r--Test/dafny0/Use.dfy183
-rw-r--r--Test/dafny0/runtest.bat3
9 files changed, 532 insertions, 76 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 9e30ab85..fe2e6a8c 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -263,8 +263,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
Statement! bb; Statement body = null;
.)
"method"
- (. if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); }
- if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
+ (. if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
.)
{ Attribute<ref attrs> }
Ident<out id>
@@ -280,7 +279,7 @@ MethodDecl<MemberModifiers mmod, out Method! m>
)
(. parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, typeArgs, ins, outs, req, mod, ens, body, attrs);
+ m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, body, attrs);
.)
.
diff --git a/Source/Dafny/DafnyAst.ssc b/Source/Dafny/DafnyAst.ssc
index 01e55cfd..549a32e0 100644
--- a/Source/Dafny/DafnyAst.ssc
+++ b/Source/Dafny/DafnyAst.ssc
@@ -487,6 +487,7 @@ namespace Microsoft.Dafny
public class Method : MemberDecl, TypeParameter.ParentType {
public readonly bool IsClass;
+ public readonly bool IsGhost;
public readonly List<TypeParameter!>! TypeArgs;
public readonly List<Formal!>! Ins;
public readonly List<Formal!>! Outs;
@@ -496,13 +497,14 @@ namespace Microsoft.Dafny
public readonly Statement Body;
public Method(Token! tok, string! name,
- bool isClass,
+ bool isClass, bool isGhost,
[Captured] List<TypeParameter!>! typeArgs,
[Captured] List<Formal!>! ins, [Captured] List<Formal!>! outs,
[Captured] List<MaybeFreeExpression!>! req, [Captured] List<Expression!>! mod, [Captured] List<MaybeFreeExpression!>! ens,
[Captured] Statement body,
Attributes attributes) {
this.IsClass = isClass;
+ this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.Ins = ins;
this.Outs = outs;
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc
index 76bb32bc..ec3e44f4 100644
--- a/Source/Dafny/Parser.ssc
+++ b/Source/Dafny/Parser.ssc
@@ -322,7 +322,6 @@ public static int Parse (List<TopLevelDecl!>! classes) {
Statement! bb; Statement body = null;
Expect(16);
- if (mmod.IsGhost) { SemErr(token, "methods cannot be declared 'ghost'"); }
if (mmod.IsUse) { SemErr(token, "methods cannot be declared 'use'"); }
while (t.kind == 5) {
@@ -351,7 +350,7 @@ public static int Parse (List<TopLevelDecl!>! classes) {
body = bb;
} else Error(96);
parseVarScope.PopMarker();
- m = new Method(id, id.val, mmod.IsClass, typeArgs, ins, outs, req, mod, ens, body, attrs);
+ m = new Method(id, id.val, mmod.IsClass, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, body, attrs);
}
diff --git a/Source/Dafny/Translator.ssc b/Source/Dafny/Translator.ssc
index 4a8d7ebf..aef2ad9b 100644
--- a/Source/Dafny/Translator.ssc
+++ b/Source/Dafny/Translator.ssc
@@ -377,24 +377,23 @@ namespace Microsoft.Dafny {
} else if (member is Function) {
Function f = (Function)member;
- Bpl.Function useFunc;
- Bpl.Function func = GetFunction(f, out useFunc);
- sink.TopLevelDeclarations.Add(func);
- if (useFunc != null) {
- sink.TopLevelDeclarations.Add(useFunc);
- }
- if (f.Body is MatchExpr) {
- MatchExpr me = (MatchExpr)f.Body;
- Formal formal = (Formal)((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
- foreach (MatchCase mc in me.Cases) {
- assert mc.Ctor != null; // the field is filled in by resolution
- Bpl.Axiom ax = FunctionAxiom(f, mc.Body, formal, mc.Ctor, mc.Arguments);
+ AddFunction(f);
+ if (f.Body != null) {
+ if (f.Body is MatchExpr) {
+ MatchExpr me = (MatchExpr)f.Body;
+ Formal formal = (Formal)((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
+ foreach (MatchCase mc in me.Cases) {
+ assert mc.Ctor != null; // the field is filled in by resolution
+ Bpl.Axiom ax = FunctionAxiom(f, mc.Body, formal, mc.Ctor, mc.Arguments);
+ sink.TopLevelDeclarations.Add(ax);
+ }
+ } else {
+ Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);
sink.TopLevelDeclarations.Add(ax);
}
-
- } else if (f.Body != null) {
- Bpl.Axiom ax = FunctionAxiom(f, f.Body, null, null, null);
- sink.TopLevelDeclarations.Add(ax);
+ if (f.IsUse) {
+ AddUseAxioms(f);
+ }
}
} else if (member is Method) {
@@ -416,7 +415,7 @@ namespace Microsoft.Dafny {
{
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
- // axiom (forall $Heap, formals :: f#use(args) && this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body)
+ // axiom (forall $Heap, formals :: this != null && $IsHeap($Heap) && Pre($Heap,args) ==> f(args) == body)
//
// The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
// "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by
@@ -426,7 +425,7 @@ namespace Microsoft.Dafny {
// If a specialization is provided, occurrences of "specializationFormal" in "body" are also replaced by
// that expression.
//
- // The antecedent f#use(fff) is included only if the function has been declared as 'use'.
+ // The translation of "body" uses the #alt form of all "use" functions.
//
// Note, an antecedent $Heap[this,alloc] is intentionally left out: including it would only weaken
// the axiom. Moreover, leaving it out does not introduce any soundness problem, because the Dafny
@@ -485,15 +484,7 @@ namespace Microsoft.Dafny {
}
Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
- Bpl.Trigger tr;
- if (f.IsUse) {
- Bpl.FunctionCall useID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", TrType(f.ResultType)));
- Bpl.Expr useAppl = new Bpl.NAryExpr(f.tok, useID, args);
- ante = Bpl.Expr.And(useAppl, ante);
- tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useAppl));
- } else {
- tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
- }
+ Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
if (specializationFormal != null) {
assert r != null;
@@ -501,10 +492,57 @@ namespace Microsoft.Dafny {
substMap.Add(specializationFormal, r);
body = Substitute(body, null, substMap);
}
- Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.TrExpr(body))));
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, Bpl.Expr.Eq(funcAppl, etran.AltFunctions.TrExpr(body))));
return new Bpl.Axiom(f.tok, ax);
}
+ void AddUseAxioms(Function! f)
+ requires f.IsUse;
+ requires sink != null && predef != null;
+ {
+ // axiom (forall formals :: { f(args) } f(args) == f#alt(args))
+ // axiom (forall formals :: { f#use(args) } f#use(args) ==> f(args) == f#alt(args))
+
+ Bpl.VariableSeq formals = new Bpl.VariableSeq();
+ Bpl.ExprSeq args = new Bpl.ExprSeq();
+ Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));
+ formals.Add(bv);
+ args.Add(new Bpl.IdentifierExpr(f.tok, bv));
+ Bpl.BoundVariable bvThis;
+ Bpl.Expr bvThisIdExpr;
+ if (f.IsClass) {
+ bvThis = null;
+ bvThisIdExpr = null;
+ } else {
+ bvThis = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "this", predef.RefType));
+ formals.Add(bvThis);
+ bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);
+ args.Add(bvThisIdExpr);
+ }
+ foreach (Formal p in f.Formals) {
+ bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));
+ formals.Add(bv);
+ args.Add(new Bpl.IdentifierExpr(p.tok, bv));
+ }
+
+ Bpl.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
+ Bpl.FunctionCall altFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#alt", TrType(f.ResultType)));
+ Bpl.Expr altFuncAppl = new Bpl.NAryExpr(f.tok, altFuncID, args);
+ Bpl.FunctionCall useFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#use", Bpl.Type.Bool));
+ Bpl.Expr useFuncAppl = new Bpl.NAryExpr(f.tok, useFuncID, args);
+
+ Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
+
+ Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(origFuncAppl));
+ Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, altFuncAppl));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
+
+ tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(useFuncAppl));
+ ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(useFuncAppl, Bpl.Expr.Eq(origFuncAppl, altFuncAppl)));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
+ }
+
void AddAllocationAxiom(Field! f)
requires sink != null && predef != null;
{
@@ -699,6 +737,8 @@ namespace Microsoft.Dafny {
/// Note, the second h?[o,alloc] in the antecedent of each inner forall above is sound
/// because user expressions are not allowed to quantify over all allocated objects, and
/// in particular, they have no way to depend on the .alloc field of an object.
+ ///
+ /// If the function is a "use" function, then "F "in the last line is replaced by "F#alt".
/// </summary>
void AddFrameAxiom(Function! f)
requires sink != null && predef != null;
@@ -764,7 +804,7 @@ namespace Microsoft.Dafny {
if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
}
- Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.IsUse ? f.FullName + "#alt" : f.FullName, TrType(f.ResultType)));
Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
Bpl.Expr eq = Bpl.Expr.Eq(F0, F1);
@@ -918,12 +958,24 @@ namespace Microsoft.Dafny {
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
assert e.Function != null; // follows from the fact that expr has been successfully resolved
+ // check well-formedness of receiver
Bpl.Expr r = IsTotal(e.Receiver, etran);
if (!e.Function.IsClass && !(e.Receiver is ThisExpr)) {
r = BplAnd(r, Bpl.Expr.Neq(etran.TrExpr(e.Receiver), predef.Null));
}
- // TODO: check reads permissions and check preconditions
- return BplAnd(r, IsTotal(e.Args, etran));
+ // check well-formedness of the other parameters
+ r = BplAnd(r, IsTotal(e.Args, etran));
+ // create a substitution map from each formal parameter to the corresponding actual parameter
+ Dictionary<IVariable,Expression!> substMap = new Dictionary<IVariable,Expression!>();
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ substMap.Add(e.Function.Formals[i], e.Args[i]);
+ }
+ // check that the preconditions for the call hold
+ foreach (Expression p in e.Function.Req) {
+ Expression precond = Substitute(p, e.Receiver, substMap);
+ r = BplAnd(r, etran.TrExpr(precond));
+ }
+ return r;
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
return IsTotal(dtv.Arguments, etran);
@@ -1332,10 +1384,9 @@ namespace Microsoft.Dafny {
return new Bpl.IdentifierExpr(fse.tok, GetField(fse.Field));
}
- Bpl.Function! GetFunction(Function! f, out Bpl.Function useF)
- requires predef != null;
+ void AddFunction(Function! f)
+ requires predef != null && sink != null;
{
- useF = null;
Bpl.Function func;
if (functions.TryGetValue(f, out func)) {
assert func != null;
@@ -1353,13 +1404,17 @@ namespace Microsoft.Dafny {
func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
functions.Add(f, func);
+ sink.TopLevelDeclarations.Add(func);
if (f.IsUse) {
+ Bpl.Function altF = new Bpl.Function(f.tok, f.FullName + "#alt", args, res);
+ sink.TopLevelDeclarations.Add(altF);
+
Bpl.Formal boolRes = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes);
+ Bpl.Function useF = new Bpl.Function(f.tok, f.FullName + "#use", args, boolRes);
+ sink.TopLevelDeclarations.Add(useF);
}
}
- return func;
}
Bpl.Procedure! GetMethod(Method! m)
@@ -2217,6 +2272,8 @@ namespace Microsoft.Dafny {
public readonly Bpl.Expr! HeapExpr;
public readonly PredefinedDecls! predef;
public readonly Translator! translator;
+ readonly bool applyAltFunctions;
+
public ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Token! heapToken) {
this.translator = translator;
this.predef = predef;
@@ -2229,16 +2286,29 @@ namespace Microsoft.Dafny {
this.HeapExpr = heap;
}
+ ExpressionTranslator(Translator! translator, PredefinedDecls! predef, Bpl.Expr! heap, bool applyAltFunctions) {
+ this.translator = translator;
+ this.predef = predef;
+ this.HeapExpr = heap;
+ this.applyAltFunctions = applyAltFunctions;
+ }
+
ExpressionTranslator oldEtran;
public ExpressionTranslator! Old {
get {
if (oldEtran == null) {
- oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr));
+ oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyAltFunctions);
}
return oldEtran;
}
}
+ public ExpressionTranslator! AltFunctions {
+ get {
+ return new ExpressionTranslator(translator, predef, HeapExpr, true);
+ }
+ }
+
public Bpl.Expr! TrExpr(Expression! expr)
requires predef != null;
{
@@ -2320,7 +2390,12 @@ namespace Microsoft.Dafny {
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- string nm = ((!)e.Function).FullName + (e is UseExpr ? "#use" : "");
+ string nm = ((!)e.Function).FullName;
+ if (e is UseExpr) {
+ nm += "#use";
+ } else if (this.applyAltFunctions && e.Function.IsUse) {
+ nm += "#alt";
+ }
Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(expr.tok, nm, translator.TrType((!)e.Type));
Bpl.ExprSeq args = new Bpl.ExprSeq();
args.Add(HeapExpr);
@@ -3033,24 +3108,9 @@ namespace Microsoft.Dafny {
Expression body = Substitute(fexp.Function.Body, fexp.Receiver, substMap);
foreach (Expression se in SplitExpr(body, false)) {
assert fexp != null && fexp.Function != null; // already checked above, but the compiler seems to have forgotten that
- if (fexp.Function.IsUse) {
- BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, new UseExpr(fexp), se);
- imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;
- imp.Type = Type.Bool;
- yield return imp;
- } else {
- yield return se;
- }
+ yield return se;
}
assert fexp != null && fexp.Function != null; // already checked above, but the compiler seems to have forgotten that
- if (fexp.Function.IsUse) {
- UnaryExpr ue = new UnaryExpr(expr.tok, UnaryExpr.Opcode.Not, new UseExpr(fexp));
- ue.Type = Type.Bool;
- BinaryExpr imp = new BinaryExpr(expr.tok, BinaryExpr.Opcode.Imp, ue, expr);
- imp.ResolvedOp = BinaryExpr.ResolvedOpcode.Imp;
- imp.Type = Type.Bool;
- yield return imp;
- }
yield break;
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d1584333..107cab0b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -134,17 +134,35 @@ Dafny program verifier finished with 6 verified, 0 errors
Dafny program verifier finished with 6 verified, 0 errors
-------------------- Use.dfy --------------------
-Use.dfy(12,5): Error: assertion violation
+Use.dfy(15,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(25,5): Error: assertion violation
+Use.dfy(26,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Use.dfy(50,5): Error: assertion violation
+Use.dfy(35,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(56,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(88,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(130,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(152,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(170,5): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Use.dfy(215,5): Error: assertion violation
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 6 verified, 3 errors
+Dafny program verifier finished with 20 verified, 9 errors
-------------------- DTypes.dfy --------------------
DTypes.dfy(15,5): Error: assertion violation
@@ -172,3 +190,11 @@ Dafny program verifier finished with 10 verified, 2 errors
-------------------- Datatypes.dfy --------------------
Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- UnboundedStack.dfy --------------------
+
+Dafny program verifier finished with 7 verified, 0 errors
+
+-------------------- SumOfCubes.dfy --------------------
+
+Dafny program verifier finished with 10 verified, 0 errors
diff --git a/Test/dafny0/SumOfCubes.dfy b/Test/dafny0/SumOfCubes.dfy
new file mode 100644
index 00000000..389c885c
--- /dev/null
+++ b/Test/dafny0/SumOfCubes.dfy
@@ -0,0 +1,110 @@
+class SumOfCubes {
+ class use function SumEmUp(n: int, m: int): int
+ requires 0 <= n && n <= m;
+ decreases m - n;
+ {
+ if m == n then 0 else n*n*n + SumEmUp(n+1, m)
+ }
+
+ class method Socu(n: int, m: int) returns (r: int)
+ requires 0 <= n && n <= m;
+ ensures r == SumEmUp(n, m);
+ {
+ call a := SocuFromZero(m);
+ call b := SocuFromZero(n);
+ r := a - b;
+ call Lemma0(n, m);
+ }
+
+ class method SocuFromZero(k: int) returns (r: int)
+ requires 0 <= k;
+ ensures r == SumEmUp(0, k);
+ {
+ call g := Gauss(k);
+ r := g * g;
+ call Lemma1(k);
+ }
+
+ ghost class method Lemma0(n: int, m: int)
+ requires 0 <= n && n <= m;
+ ensures SumEmUp(n, m) == SumEmUp(0, m) - SumEmUp(0, n);
+ {
+ var k := n;
+ while (k < m)
+ invariant n <= k && k <= m;
+ invariant SumEmDown(0, n) + SumEmDown(n, k) == SumEmDown(0, k);
+ decreases m - k;
+ {
+ k := k + 1;
+ }
+ call Lemma3(0, n);
+ call Lemma3(n, k);
+ call Lemma3(0, k);
+ }
+
+ class use function GSum(k: int): int
+ requires 0 <= k;
+ decreases k;
+ {
+ if k == 0 then 0 else GSum(k-1) + k-1
+ }
+
+ ghost class method Gauss(k: int) returns (r: int)
+ requires 0 <= k;
+ ensures r == GSum(k);
+ {
+ r := k * (k - 1) / 2;
+ call Lemma2(k);
+ }
+
+ ghost class method Lemma1(k: int)
+ requires 0 <= k;
+ ensures SumEmUp(0, k) == GSum(k) * GSum(k);
+ {
+ var i := 0;
+ while (i < k)
+ invariant i <= k;
+ invariant SumEmDown(0, i) == GSum(i) * GSum(i);
+ decreases k - i;
+ {
+ call Lemma2(i);
+ i := i + 1;
+ }
+ call Lemma3(0, k);
+ }
+
+ ghost class method Lemma2(k: int)
+ requires 0 <= k;
+ ensures 2 * GSum(k) == k * (k - 1);
+ {
+ var i := 0;
+ while (i < k)
+ invariant i <= k;
+ invariant 2 * GSum(i) == i * (i - 1);
+ decreases k - i;
+ {
+ i := i + 1;
+ }
+ }
+
+ class use function SumEmDown(n: int, m: int): int
+ requires 0 <= n && n <= m;
+ decreases m;
+ {
+ if m == n then 0 else SumEmDown(n, m-1) + (m-1)*(m-1)*(m-1)
+ }
+
+ ghost class method Lemma3(n: int, m: int)
+ requires 0 <= n && n <= m;
+ ensures SumEmUp(n, m) == SumEmDown(n, m);
+ {
+ var k := n;
+ while (k < m)
+ invariant n <= k && k <= m;
+ invariant SumEmUp(n, m) == SumEmDown(n, k) + SumEmUp(k, m);
+ decreases m - k;
+ {
+ k := k + 1;
+ }
+ }
+}
diff --git a/Test/dafny0/UnboundedStack.dfy b/Test/dafny0/UnboundedStack.dfy
new file mode 100644
index 00000000..4c3b095a
--- /dev/null
+++ b/Test/dafny0/UnboundedStack.dfy
@@ -0,0 +1,98 @@
+class UnboundedStack<T> {
+ ghost var representation: set<object>;
+ ghost var content: seq<T>;
+ var top: Node<T>;
+
+ function IsUnboundedStack(): bool
+ reads this, representation;
+ {
+ this in representation &&
+ (top == null ==>
+ content == []) &&
+ (top != null ==>
+ top in representation && this !in top.footprint && top.footprint <= representation &&
+ content == top.content &&
+ top.Valid())
+ }
+
+ method InitUnboundedStack()
+ modifies this;
+ ensures IsUnboundedStack();
+ ensures content == [];
+ {
+ this.top := null;
+ this.content := [];
+ this.representation := {this};
+ }
+
+ method Push(val: T)
+ requires IsUnboundedStack();
+ modifies this;
+ ensures IsUnboundedStack();
+ ensures content == [val] + old(content);
+ {
+ var tmp := new Node<T>;
+ call tmp.InitNode(val,top);
+ top := tmp;
+ representation := representation + top.footprint;
+ content := [val] + content;
+ }
+
+ method Pop() returns (result: T)
+ requires IsUnboundedStack();
+ requires content != [];
+ modifies this;
+ ensures IsUnboundedStack();
+ ensures content == old(content)[1..];
+ {
+ result := top.val;
+ top := top.next;
+ content := content[1..];
+ }
+
+ method isEmpty() returns (result: bool)
+ requires IsUnboundedStack();
+ ensures result <==> content == [];
+ {
+ result := top == null;
+ }
+}
+
+class Node<T> {
+ ghost var footprint: set<object>;
+ ghost var content: seq<T>;
+ var val: T;
+ var next: Node<T>;
+
+ function Valid(): bool
+ reads this, footprint;
+ {
+ this in footprint &&
+ (next == null ==>
+ content == [val]) &&
+ (next != null ==>
+ next in footprint && next.footprint <= footprint && this !in next.footprint &&
+ content == [val] + next.content &&
+ next.Valid())
+ }
+
+ method InitNode(val: T, next: Node<T>)
+ requires next != null ==> next.Valid() && !(this in next.footprint);
+ modifies this;
+ ensures Valid();
+ ensures next != null ==> content == [val] + next.content &&
+ footprint == {this} + next.footprint;
+ ensures next == null ==> content == [val] &&
+ footprint == {this};
+ {
+ this.val := val;
+ this.next := next;
+ if (next == null) {
+ this.footprint := {this};
+ this.content := [val];
+ } else {
+ this.footprint := {this} + next.footprint;
+ this.content := [val] + next.content;
+ }
+ }
+}
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 8b7eafc1..e006823e 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -1,7 +1,9 @@
class T {
var x: int;
- use function F(y: int): int {
+ use function F(y: int): int
+ decreases 0;
+ {
2*y
}
@@ -9,37 +11,73 @@ class T {
use F(4);
use F(5);
assert F(5) == 10;
- assert F(7) == 14; // error (definition not engaged)
+ assert F(7) == 14;
+ assert F(72) == 14; // error (just plain wrong)
+ }
+
+ use function FF(y: int): int
+ decreases 1;
+ {
+ F(y)
+ }
+
+ method MM() {
+ assert F(5) == 10;
+ assert FF(6) == 12; // error (definition of F not engaged)
+
+ assert F(7) == 14;
+ assert FF(7) == 14; // now the inner definition of F has already been engaged
+
+ use F(8);
+ assert FF(8) == 16; // same here
+
+ use FF(9);
+ assert FF(9) == 18; // error (definition of F not engaged; the use of FF does not help)
}
- use function G(y: int): bool {
+ use function G(y: int): bool
+ decreases 0;
+ {
0 <= y
}
+ use function GG(y: int): bool
+ decreases 1;
+ {
+ G(y)
+ }
method N(s: set<T>) {
use G(4);
use G(5);
use G(-5);
- assert G(5);
- assert !G(-5);
- assert G(7); // error (definition not engaged)
+ assert GG(5);
+ assert !GG(-5);
+ assert GG(7); // fine (the assert expands GG to G, then the definition of G kicks in)
+ assert !GG(-7); // error (the negation disables the expansion of GG in the assert)
}
use function H(): int
reads this;
+ decreases 0;
{
x
}
+ use function HH(): int
+ reads this;
+ decreases 1;
+ {
+ H()
+ }
method Q0()
modifies this;
{
var t := x;
use H();
- assert H() == t;
+ assert HH() == t;
x := x + 1;
- assert old(H()) == t;
+ assert old(HH()) == t;
}
method Q1()
@@ -47,7 +85,7 @@ class T {
{
x := x + 1;
use H();
- assert H() == old(H()) + 1; // error: does not know what old(H()) is
+ assert HH() == old(HH()) + 1; // error: does not know what old(H()) is
}
method Q2()
@@ -56,7 +94,7 @@ class T {
use H();
x := x + 1;
use H();
- assert H() == old(H()) + 1;
+ assert HH() == old(HH()) + 1;
}
method Q3()
@@ -65,6 +103,129 @@ class T {
x := x + 1;
use H();
use old(H());
- assert H() == old(H()) + 1;
+ assert HH() == old(HH()) + 1;
+ }
+
+ method Q4(other: T)
+ requires other != null && other != this;
+ modifies other;
+ {
+ other.x := other.x + 1;
+ assert HH() == old(HH()); // frame axiom for H still works
+ }
+
+ method Q5(other: T)
+ requires other != null && other != this;
+ modifies this;
+ {
+ x := x + 1;
+ assert other.HH() == old(other.HH()); // frame axiom for H still works
+ }
+
+ method Q6(other: T)
+ requires other != null;
+ modifies this;
+ {
+ x := x + 1;
+ assert other.HH() == old(other.HH()); // error: 'other' may equal 'this', in which
+ // case nothing is known about how H() changed
+ }
+
+ use function K(): bool
+ reads this;
+ decreases 0;
+ {
+ x <= 100
+ }
+ use function KK(): bool
+ reads this;
+ decreases 1;
+ {
+ K()
+ }
+
+ method R0()
+ requires KK();
+ modifies this;
+ {
+ x := x - 1;
+ assert KK(); // error (does not know exact definition of K from the initial state)
+ }
+
+ method R1()
+ requires KK();
+ modifies this;
+ {
+ use K(); // KK in the precondition and KK's definition give K#alt, which this use expands
+ x := x - 1;
+ assert KK(); // the assert expands KK to K, definition of K expands K
+ }
+
+ method R2()
+ requires KK();
+ modifies this;
+ {
+ x := x - 1;
+ use K();
+ assert KK(); // error (does not know exact definition of K in the pre-state)
+ }
+
+ method R3()
+ requires KK();
+ modifies this;
+ {
+ use K();
+ x := x - 1;
+ use K();
+ assert KK(); // thar it is
+ }
+}
+
+class Recursive {
+ use function Gauss(n: int): int
+ requires 0 <= n;
+ decreases n;
+ {
+ if n == 0 then 0 else Gauss(n-1) + n
+ }
+
+ ghost method G(n: int)
+ requires 0 <= n;
+ ensures Gauss(n) == (n+1)*n / 2;
+ {
+ var k := 0;
+ while (k < n)
+ invariant k <= n;
+ invariant Gauss(k) == (k+1)*k / 2;
+ decreases n - k;
+ {
+ k := k + 1;
+ }
+ }
+
+ use function Fib(n: int): int
+ requires 0 <= n;
+ decreases n;
+ {
+ if n < 2 then n else Fib(n-2) + Fib(n-1)
+ }
+
+ method F0()
+ {
+ assert Fib(2) == 1; // error (does not know about Fib for the recursive calls)
+ }
+
+ method F1()
+ {
+ assert Fib(0) == 0;
+ assert Fib(1) == 1;
+ assert Fib(2) == 1; // now it knows
+ }
+
+ method F2()
+ {
+ assert Fib(0) == 0;
+ use Fib(1);
+ assert Fib(2) == 1; // now it knows, too
}
}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index f1bcfde0..64efe27b 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -20,7 +20,8 @@ for %%f in (BQueue.bpl) do (
for %%f in (TypeTests.dfy SmallTests.dfy Queue.dfy ListCopy.dfy
BinaryTree.dfy ListReverse.dfy ListContents.dfy
SchorrWaite.dfy Termination.dfy Use.dfy DTypes.dfy
- TypeParameters.dfy Datatypes.dfy) do (
+ TypeParameters.dfy Datatypes.dfy UnboundedStack.dfy
+ SumOfCubes.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% %* %%f
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-28 14:31:22 +0000