summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2011-03-04 07:24:29 +0000
committerGravatar rustanleino <unknown>2011-03-04 07:24:29 +0000
commit8a2dd8d4c29df3db73dd13a5457efbee007dfeac (patch)
treecb62d829a0da76d3c68c40fbc815a700d2181044
parentccc1c910af50b211f66566c981bdb62827d814d6 (diff)
Dafny:
* Add support for an {:induction} attribute on universal quantifiers over one bound variable. It causes the universally quantified formulas to be proved by induction. * For a user-defined function F, introduce not just F and F#limited, but also F#2 (which sits "above" F, just as F sits "above" F#limited) * In base case of SplitExpr, make use of F#2 functions (unless already inside an inlined predicate)
-rw-r--r--Source/Dafny/Resolver.cs8
-rw-r--r--Source/Dafny/Translator.cs272
-rw-r--r--Test/dafny0/Answer15
-rw-r--r--Test/dafny0/DTypes.dfy53
-rw-r--r--Test/dafny0/Use.dfy10
-rw-r--r--Test/dafny1/Answer4
-rw-r--r--Test/dafny1/Induction.dfy132
-rw-r--r--Test/dafny1/runtest.bat1
8 files changed, 431 insertions, 64 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 57fe4f77..59a1331d 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1630,10 +1630,10 @@ namespace Microsoft.Dafny {
return null;
}
- Type SubstType(Type type, Dictionary<TypeParameter/*!*/,Type/*!*/>/*!*/ subst) {
- Contract.Requires(type != null);
- Contract.Requires(cce.NonNullElements(subst));
- Contract.Ensures(Contract.Result<Type>() != null);
+ public static Type SubstType(Type type, Dictionary<TypeParameter/*!*/,Type/*!*/>/*!*/ subst) {
+ Contract.Requires(type != null);
+ Contract.Requires(cce.NonNullElements(subst));
+ Contract.Ensures(Contract.Result<Type>() != null);
if (type is BasicType) {
return type;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c3eec272..1ba05262 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -416,7 +416,9 @@ namespace Microsoft.Dafny {
args = new List<Bpl.Expr>();
foreach (Formal arg in formals) {
Contract.Assert(arg != null);
- Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "a" + bvs.Length, TrType(arg.Type)));
+ var nm = string.Format("a{0}#{1}", bvs.Length, otherTmpVarCount);
+ otherTmpVarCount++;
+ Bpl.Variable bv = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)));
bvs.Add(bv);
args.Add(new Bpl.IdentifierExpr(arg.tok, bv));
}
@@ -444,16 +446,20 @@ namespace Microsoft.Dafny {
} else if (member is Function) {
Function f = (Function)member;
AddFunction(f);
- if (f.Body is MatchExpr) {
- AddFunctionAxiomCase(f, (MatchExpr)f.Body, null);
- Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null);
- sink.TopLevelDeclarations.Add(axPost);
- } else {
- Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null);
- sink.TopLevelDeclarations.Add(ax);
- }
if (f.IsRecursive && !f.IsUnlimited) {
- AddLimitedAxioms(f);
+ AddLimitedAxioms(f, 2);
+ AddLimitedAxioms(f, 1);
+ }
+ for (int layerOffset = 0; layerOffset < 2; layerOffset++) {
+ if (f.Body is MatchExpr) {
+ AddFunctionAxiomCase(f, (MatchExpr)f.Body, null, layerOffset);
+ Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, layerOffset);
+ sink.TopLevelDeclarations.Add(axPost);
+ } else {
+ Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, layerOffset);
+ sink.TopLevelDeclarations.Add(ax);
+ }
+ if (!f.IsRecursive || f.IsUnlimited) { break; }
}
AddFrameAxiom(f);
AddWellformednessCheck(f);
@@ -486,17 +492,19 @@ namespace Microsoft.Dafny {
}
}
- void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev) {
+ void AddFunctionAxiomCase(Function f, MatchExpr me, Specialization prev, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(me != null);
+ Contract.Requires(layerOffset == 0 || layerOffset == 1);
+
IVariable formal = ((IdentifierExpr)me.Source).Var; // correctness of casts follows from what resolution checks
foreach (MatchCaseExpr mc in me.Cases) {
Contract.Assert(mc.Ctor != null); // the field is filled in by resolution
Specialization s = new Specialization(formal, mc, prev);
if (mc.Body is MatchExpr) {
- AddFunctionAxiomCase(f, (MatchExpr)mc.Body, s);
+ AddFunctionAxiomCase(f, (MatchExpr)mc.Body, s, layerOffset);
} else {
- Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), s);
+ Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), s, layerOffset);
sink.TopLevelDeclarations.Add(ax);
}
}
@@ -557,9 +565,10 @@ namespace Microsoft.Dafny {
}
}
- Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization) {
+ Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {
Contract.Requires(f != null);
Contract.Requires(ens != null);
+ Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive && !f.IsUnlimited));
Contract.Requires(predef != null);
Contract.Requires(f.EnclosingClass != null);
@@ -576,10 +585,10 @@ namespace Microsoft.Dafny {
// $IsHeap($Heap) && this != null && formals-have-the-expected-types &&
// Pre($Heap,args))
// ==>
- // body-can-make-its-calls &&
+ // body-can-make-its-calls && // generated only for layerOffset==0
// f(args) == body &&
- // ens &&
- // f(args)-has-the-expected-type);
+ // ens && // generated only for layerOffset==0
+ // f(args)-has-the-expected-type); // generated only for layerOffset==0
//
// The variables "formals" are the formals of function "f"; except, if a specialization is provided, then
// "specialization.Formals" (which are expected to be among the formals of "f") are excluded and replaced by
@@ -591,6 +600,8 @@ namespace Microsoft.Dafny {
//
// The translation of "body" uses the #limited form whenever the callee is in the same SCC of the call graph.
//
+ // if layerOffset==1, then the names f#2 and f are used instead of f and f#limited.
+ //
// 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
// allocation statement changes only an allocation bit and then re-assumes $IsGoodHeap; so if it is
@@ -663,7 +674,7 @@ namespace Microsoft.Dafny {
substMap.Add(specialization.Formals[i], specialization.ReplacementExprs[i]);
}
}
- Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType));
+ Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1+layerOffset), TrType(f.ResultType));
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);
Bpl.Expr pre = Bpl.Expr.True;
@@ -686,22 +697,28 @@ namespace Microsoft.Dafny {
Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
Bpl.Expr meat;
- if (body != null) {
- Expression bodyWithSubst = Substitute(body, null, substMap);
- meat = Bpl.Expr.And(
- CanCallAssumption(bodyWithSubst, etran),
- Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
- } else {
+ if (body == null) {
meat = Bpl.Expr.True;
+ } else {
+ Expression bodyWithSubst = Substitute(body, null, substMap);
+ if (layerOffset == 0) {
+ meat = Bpl.Expr.And(
+ CanCallAssumption(bodyWithSubst, etran),
+ Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));
+ } else {
+ meat = Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));
+ }
}
- foreach (Expression p in ens) {
- Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));
- meat = BplAnd(meat, q);
+ if (layerOffset == 0) {
+ foreach (Expression p in ens) {
+ Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));
+ meat = BplAnd(meat, q);
+ }
+ Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);
+ if (whr != null) { meat = Bpl.Expr.And(meat, whr); }
}
- Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);
- if (whr != null) { meat = Bpl.Expr.And(meat, whr); }
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));
- string comment = "definition axiom for " + f.FullName;
+ string comment = "definition axiom for " + FunctionName(f, 1+layerOffset);
if (specialization != null) {
string sep = "{0}, specialized for '{1}'";
foreach (var formal in specialization.Formals) {
@@ -712,11 +729,15 @@ namespace Microsoft.Dafny {
return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);
}
- void AddLimitedAxioms(Function f){
+ void AddLimitedAxioms(Function f, int fromLayer) {
Contract.Requires(f != null);
Contract.Requires(f.IsRecursive && !f.IsUnlimited);
+ Contract.Requires(fromLayer == 1 || fromLayer == 2);
Contract.Requires(sink != null && predef != null);
- // axiom (forall formals :: { f(args) } f(args) == f#limited(args))
+ // With fromLayer==1, generate:
+ // axiom (forall formals :: { f(args) } f(args) == f#limited(args))
+ // With fromLayer==2, generate:
+ // axiom (forall formals :: { f#2(args) } f#2(args) == f(args))
Bpl.VariableSeq formals = new Bpl.VariableSeq();
Bpl.ExprSeq args = new Bpl.ExprSeq();
@@ -739,10 +760,10 @@ namespace Microsoft.Dafny {
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.FunctionCall origFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer), TrType(f.ResultType)));
Bpl.Expr origFuncAppl = new Bpl.NAryExpr(f.tok, origFuncID, args);
- Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
+ Bpl.FunctionCall limitedFuncID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, fromLayer-1), TrType(f.ResultType)));
Bpl.Expr limitedFuncAppl = new Bpl.NAryExpr(f.tok, limitedFuncID, args);
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);
@@ -751,6 +772,25 @@ namespace Microsoft.Dafny {
Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Eq(origFuncAppl, limitedFuncAppl));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));
}
+
+ /// <summary>
+ /// Returns the appropriate Boogie function for the given function. In particular:
+ /// Layer 2: f#2 --currently used only for induction axioms
+ /// Layer 1: f --this is the default name
+ /// Layer 0: f#limited --does not trigger the function definition axiom
+ /// </summary>
+ public static string FunctionName(Function f, int layer) {
+ Contract.Requires(f != null);
+ Contract.Requires(0 <= layer && layer < 3);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ string name = f.FullName;
+ switch (layer) {
+ case 2: name += "#2"; break;
+ case 0: name += "#limited"; break;
+ }
+ return name;
+ }
/// <summary>
/// Generate:
@@ -1101,7 +1141,7 @@ namespace Microsoft.Dafny {
Bpl.Expr.Imp(q0, eq)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax, axiomComment));
if (axiomComment != null && f.IsRecursive && !f.IsUnlimited) {
- fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName + "#limited", TrType(f.ResultType)));
+ fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, FunctionName(f, 0), TrType(f.ResultType)));
axiomComment = null; // the comment goes only with the first frame axiom
} else {
break; // no more frame axioms to produce
@@ -1407,7 +1447,7 @@ namespace Microsoft.Dafny {
Bpl.Expr total = IsTotal(e.Body, etran);
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- Bpl.Expr typeAntecedent = etran.TrBoundVariables(e, bvars);
+ Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
@@ -1534,7 +1574,7 @@ namespace Microsoft.Dafny {
Bpl.Expr total = CanCallAssumption(e.Body, etran);
if (total != Bpl.Expr.True) {
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- Bpl.Expr typeAntecedent = etran.TrBoundVariables(e, bvars);
+ Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));
}
return total;
@@ -2201,8 +2241,8 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(func);
if (f.IsRecursive && !f.IsUnlimited) {
- Bpl.Function limitedF = new Bpl.Function(f.tok, f.FullName + "#limited", args, res);
- sink.TopLevelDeclarations.Add(limitedF);
+ sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 0), args, res));
+ sink.TopLevelDeclarations.Add(new Bpl.Function(f.tok, FunctionName(f, 2), args, res));
}
res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
@@ -3710,6 +3750,8 @@ namespace Microsoft.Dafny {
public readonly Translator translator;
public readonly string This;
readonly Function applyLimited_CurrentFunction;
+ readonly int layerOffset = 0;
+ public int Statistics_FunctionCount = 0;
[ContractInvariantMethod]
void ObjectInvariant()
{
@@ -3717,6 +3759,8 @@ namespace Microsoft.Dafny {
Contract.Invariant(predef != null);
Contract.Invariant(translator != null);
Contract.Invariant(This != null);
+ Contract.Invariant(layerOffset == 0 || layerOffset == 1);
+ Contract.Invariant(0 <= Statistics_FunctionCount);
}
public ExpressionTranslator(Translator translator, PredefinedDecls predef, IToken heapToken) {
@@ -3750,7 +3794,7 @@ namespace Microsoft.Dafny {
this.This = thisVar;
}
- ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction) {
+ ExpressionTranslator(Translator translator, PredefinedDecls predef, Bpl.Expr heap, Function applyLimited_CurrentFunction, int layerOffset) {
Contract.Requires(translator != null);
Contract.Requires(predef != null);
Contract.Requires(heap != null);
@@ -3760,7 +3804,8 @@ namespace Microsoft.Dafny {
this.HeapExpr = heap;
this.applyLimited_CurrentFunction = applyLimited_CurrentFunction;
this.This = "this";
- }
+ this.layerOffset = layerOffset;
+ }
ExpressionTranslator oldEtran;
public ExpressionTranslator Old {
@@ -3768,7 +3813,7 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
if (oldEtran == null) {
- oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction);
+ oldEtran = new ExpressionTranslator(translator, predef, new Bpl.OldExpr(HeapExpr.tok, HeapExpr), applyLimited_CurrentFunction, layerOffset);
}
return oldEtran;
}
@@ -3784,7 +3829,15 @@ namespace Microsoft.Dafny {
Contract.Requires(applyLimited_CurrentFunction != null);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction);
+ return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset);
+ }
+
+ public ExpressionTranslator LayerOffset(int offset) {
+ Contract.Requires(0 <= offset);
+ Contract.Requires(layerOffset + offset <= 1);
+ Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
+
+ return new ExpressionTranslator(translator, predef, HeapExpr, applyLimited_CurrentFunction, layerOffset + offset);
}
public Bpl.IdentifierExpr TheFrame(IToken tok)
@@ -3938,12 +3991,14 @@ namespace Microsoft.Dafny {
} else if (expr is FunctionCallExpr) {
FunctionCallExpr e = (FunctionCallExpr)expr;
- string nm = cce.NonNull(e.Function).FullName;
+ Statistics_FunctionCount++;
+ int offsetToUse = e.Function.IsRecursive && !e.Function.IsUnlimited ? this.layerOffset : 0;
+ string nm = FunctionName(e.Function, 1 + offsetToUse);
if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive && !e.Function.IsUnlimited) {
ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module;
if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) {
if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) {
- nm += "#limited";
+ nm = FunctionName(e.Function, 0 + offsetToUse);
}
}
}
@@ -4131,7 +4186,7 @@ namespace Microsoft.Dafny {
} else if (expr is QuantifierExpr) {
QuantifierExpr e = (QuantifierExpr)expr;
Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- Bpl.Expr typeAntecedent = TrBoundVariables(e, bvars);
+ Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);
Bpl.QKeyValue kv = TrAttributes(e.Attributes);
Bpl.Trigger tr = null;
for (Triggers trigs = e.Trigs; trigs != null; trigs = trigs.Prev) {
@@ -4170,12 +4225,12 @@ namespace Microsoft.Dafny {
}
}
- public Bpl.Expr TrBoundVariables(QuantifierExpr e, Bpl.VariableSeq bvars) {
- Contract.Requires(e != null);
+ public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, Bpl.VariableSeq bvars) {
+ Contract.Requires(boundVars != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
Bpl.Expr typeAntecedent = Bpl.Expr.True;
- foreach (BoundVar bv in e.BoundVars) {
+ foreach (BoundVar bv in boundVars) {
Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));
bvars.Add(bvar);
Bpl.Expr wh = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, bvar), bv.Type, this);
@@ -4257,7 +4312,7 @@ namespace Microsoft.Dafny {
Bpl.Expr f0 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName, translator.TrType(e.Type))), args);
Bpl.Expr f1;
if (fn.IsRecursive && !fn.IsUnlimited) {
- f1 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, fn.FullName + "#limited", translator.TrType(e.Type))), args);
+ f1 = new Bpl.NAryExpr(e.tok, new Bpl.FunctionCall(new Bpl.IdentifierExpr(e.tok, FunctionName(fn, 0), translator.TrType(e.Type))), args);
} else {
f1 = f0;
}
@@ -4916,10 +4971,121 @@ namespace Microsoft.Dafny {
return true;
}
+
+ } else if (expr is ForallExpr) {
+ ForallExpr e = (ForallExpr)expr;
+ for (var a = e.Attributes; a != null; a = a.Prev) {
+ if (a.Name == "induction") {
+ if (e.BoundVars.Count == 1) {
+ var n = e.BoundVars[0];
+ // From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation
+ // (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))
+ BoundVar k = new BoundVar(n.tok, n.Name + "$ih#" + otherTmpVarCount, n.Type);
+ otherTmpVarCount++;
+
+ IdentifierExpr ieK = new IdentifierExpr(k.tok, k.UniqueName);
+ ieK.Var = k; ieK.Type = ieK.Var.Type; // resolve it here
+ Bpl.Expr boogieK = etran.TrExpr(ieK);
+
+ IdentifierExpr ieN = new IdentifierExpr(n.tok, n.UniqueName);
+ ieN.Var = n; ieN.Type = ieN.Var.Type; // resolve it here
+ Bpl.Expr boogieN = etran.TrExpr(ieN);
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ substMap.Add(n, ieK);
+ Expression bodyK = Substitute(e.Body, null, substMap);
+
+ Bpl.Expr less; // says that k is bounded from below and less than n, for each respective type
+ if (n.Type is BoolType) {
+ less = Bpl.Expr.And(Bpl.Expr.Not(boogieK), boogieN);
+ } else if (n.Type is IntType) {
+ less = Bpl.Expr.And(Bpl.Expr.Le(Bpl.Expr.Literal(0), boogieK), Bpl.Expr.Lt(boogieK, boogieN));
+ } else if (n.Type is SetType) {
+ less = etran.ProperSubset(e.tok, boogieK, boogieN);
+ } else if (n.Type is SeqType) {
+ Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieK);
+ Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.SeqLength, null, boogieN);
+ less = Bpl.Expr.Lt(b0, b1);
+ } else if (n.Type.IsDatatype) {
+ Bpl.Expr b0 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieK);
+ Bpl.Expr b1 = FunctionCall(e.tok, BuiltinFunction.DtRank, null, boogieN);
+ less = Bpl.Expr.Lt(b0, b1);
+ } else {
+ // reference type
+ Bpl.Expr b0 = Bpl.Expr.Neq(boogieK, predef.Null);
+ Bpl.Expr b1 = Bpl.Expr.Neq(boogieN, predef.Null);
+ less = Bpl.Expr.And(Bpl.Expr.Not(b0), b1);
+ }
+
+ Bpl.Expr ihBody = Bpl.Expr.Imp(less, etran.TrExpr(bodyK));
+ Bpl.VariableSeq bvars = new Bpl.VariableSeq();
+ Bpl.Expr typeAntecedent = etran.TrBoundVariables(new List<BoundVar>() { k }, bvars);
+ Bpl.Expr ih = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, ihBody));
+
+ // More precisely now:
+ // (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case0(n) ==> P(n))
+ // (forall n :: n-has-expected-type && (forall k :: k < n ==> P(k)) && case...(n) ==> P(n))
+ bvars = new Bpl.VariableSeq();
+ typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);
+ foreach (var kase in InductionCases(expr.tok, n.Type, boogieN, etran)) {
+ var ante = BplAnd(BplAnd(typeAntecedent, ih), kase);
+ var bdy = etran.LayerOffset(1).TrExpr(e.Body);
+ Bpl.Expr q = new Bpl.ForallExpr(kase.tok, bvars, Bpl.Expr.Imp(ante, bdy));
+ splits.Add(new SplitExprInfo(false, q));
+ }
+
+ // Finally, assume the original quantifier (forall n :: P(n))
+ splits.Add(new SplitExprInfo(true, etran.TrExpr(expr)));
+ return true;
+ }
+ }
+ }
}
- splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));
- return false;
+ if (expandFunctions) {
+ etran = etran.LayerOffset(1);
+ splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));
+ return etran.Statistics_FunctionCount != 0;
+ } else {
+ splits.Add(new SplitExprInfo(false, etran.TrExpr(expr)));
+ return false;
+ }
+ }
+
+ IEnumerable<Bpl.Expr> InductionCases(IToken tok, Type ty, Bpl.Expr expr, ExpressionTranslator etran) {
+ DatatypeDecl dt = ty.AsDatatype;
+ if (dt == null) {
+ yield return new Bpl.LiteralExpr(tok, true); // note, we don't use Bpl.Expr.True here, because we want to set the source location
+ } else {
+ UserDefinedType instantiatedType = (UserDefinedType)ty; // correctness of cast follows from the non-null return of ty.AsDatatype
+ var subst = new Dictionary<TypeParameter, Type>();
+ for (int i = 0; i < dt.TypeArgs.Count; i++) {
+ subst.Add(dt.TypeArgs[i], instantiatedType.TypeArgs[i]);
+ }
+
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ IToken kaseTok = new NestedToken(tok, ctor.tok);
+ Bpl.VariableSeq bvs;
+ List<Bpl.Expr> args;
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ // (exists args :: args-have-the-expected-types ==> ct(args) == expr)
+ Bpl.Expr q = Bpl.Expr.Binary(kaseTok, BinaryOperator.Opcode.Eq, ct, expr);
+ if (bvs.Length != 0) {
+ int i = 0;
+ Bpl.Expr typeAntecedent = Bpl.Expr.True;
+ foreach (Formal arg in ctor.Formals) {
+ Bpl.Expr wh = GetWhereClause(arg.tok, args[i], Resolver.SubstType(arg.Type, subst), etran);
+ if (wh != null) {
+ typeAntecedent = BplAnd(typeAntecedent, wh);
+ }
+ i++;
+ }
+ q = new Bpl.ExistsExpr(kaseTok, bvs, BplAnd(typeAntecedent, q));
+ }
+ yield return q;
+ }
+ }
}
static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 9501d26d..4bf7e527 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -530,8 +530,21 @@ Execution trace:
DTypes.dfy(53,18): Error: assertion violation
Execution trace:
(0,0): anon0
+DTypes.dfy(123,13): Error: assertion violation
+DTypes.dfy(94,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+DTypes.dfy(129,13): Error: assertion violation
+DTypes.dfy(93,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
+DTypes.dfy(139,12): Error: assertion violation
+DTypes.dfy(134,6): Related location: Related location
+DTypes.dfy(93,3): Related location: Related location
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 15 verified, 2 errors
+Dafny program verifier finished with 24 verified, 5 errors
-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(41,22): Error: assertion violation
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index f92e93e6..efd2f6f0 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -86,3 +86,56 @@ function G(d: Data): int
case Lemon => G(d)
case Kiwi(x) => 7
}
+
+// -------- some things about induction ---------------------------------
+
+datatype Tree<T> {
+ Leaf(T);
+ Branch(Tree<T>, Tree<T>);
+}
+
+class DatatypeInduction<T> {
+ function LeafCount<G>(tree: Tree<G>): int
+ {
+ match tree
+ case Leaf(t) => 1
+ case Branch(left, right) => LeafCount(left) + LeafCount(right)
+ }
+
+ method Theorem0(tree: Tree<T>)
+ ensures 1 <= LeafCount(tree);
+ {
+ assert (forall t: Tree<T> {:induction} :: 1 <= LeafCount(t));
+ }
+
+ // also make sure it works for an instantiated generic datatype
+ method Theorem1(bt: Tree<bool>, it: Tree<int>)
+ ensures 1 <= LeafCount(bt);
+ ensures 1 <= LeafCount(it);
+ {
+ assert (forall t: Tree<bool> {:induction} :: 1 <= LeafCount(t));
+ assert (forall t: Tree<int> {:induction} :: 1 <= LeafCount(t));
+ }
+
+ method NotATheorem0(tree: Tree<T>)
+ ensures LeafCount(tree) % 2 == 1;
+ {
+ assert (forall t: Tree<T> {:induction} :: LeafCount(t) % 2 == 1); // error: fails for Branch case
+ }
+
+ method NotATheorem1(tree: Tree<T>)
+ ensures 2 <= LeafCount(tree);
+ {
+ assert (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t)); // error: fails for Leaf case
+ }
+
+ function Predicate(): bool
+ {
+ (forall t: Tree<T> {:induction} :: 2 <= LeafCount(t))
+ }
+
+ method NotATheorem2()
+ {
+ assert Predicate(); // error (this tests Related Location for induction via a predicate)
+ }
+}
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index 7a963382..502c4222 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -210,20 +210,18 @@ class Recursive {
method F0()
{
- assert Fib(2) == 1; // error (does not know about Fib for the recursive calls)
+ assert Fib(3) == 2; // 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
+ assert Fib(3) == 2; // now it knows
}
method F2()
{
- assert Fib(0) == 0;
- use Fib(1);
- assert Fib(2) == 1; // now it knows, too
+ use Fib(0);
+ assert Fib(3) == 2; // now it knows, too
}
}
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index a6fb57a7..07797d04 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -71,6 +71,10 @@ Dafny program verifier finished with 6 verified, 0 errors
Dafny program verifier finished with 6 verified, 0 errors
+-------------------- Induction.dfy --------------------
+
+Dafny program verifier finished with 22 verified, 0 errors
+
-------------------- Celebrity.dfy --------------------
Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
new file mode 100644
index 00000000..ea447be7
--- /dev/null
+++ b/Test/dafny1/Induction.dfy
@@ -0,0 +1,132 @@
+class IntegerInduction {
+ // This class considers different ways of proving, for any natural n:
+ // (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2
+
+ // In terms of Dafny functions, the theorem to be proved is:
+ // SumOfCubes(n) == Gauss(n) * Gauss(n)
+
+ function SumOfCubes(n: int): int
+ requires 0 <= n;
+ {
+ if n == 0 then 0 else SumOfCubes(n-1) + n*n*n
+ }
+
+ function Gauss(n: int): int
+ requires 0 <= n;
+ {
+ if n == 0 then 0 else Gauss(n-1) + n
+ }
+
+ // Here is one proof. It uses a lemma, which is proved separately.
+
+ ghost method Theorem0(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
+ {
+ if (n != 0) {
+ call Theorem0(n-1);
+ call Lemma(n-1);
+ }
+ }
+
+ ghost method Lemma(n: int)
+ requires 0 <= n;
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ if (n != 0) { call Lemma(n-1); }
+ }
+
+ // Here is another proof. It states the lemma as part of the theorem, and
+ // thus proves the two together.
+
+ ghost method Theorem1(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ if (n != 0) {
+ call Theorem1(n-1);
+ }
+ }
+
+ // Here is another proof. It makes use of Dafny's {:induction} attribute to
+ // prove the lemma.
+
+ ghost method Theorem2(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
+ {
+ if (n != 0) {
+ call Theorem0(n-1);
+
+ assert (forall m {:induction} :: 0 <= m ==> 2 * Gauss(m) == m*(m+1));
+ }
+ }
+
+ ghost method M(n: int)
+ requires 0 <= n;
+ {
+ assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis
+ assert 2 * Gauss(n) == n*(n+1);
+ }
+
+ // Another way to prove the lemma is to supply a postcondition on the Gauss function
+
+ ghost method Theorem3(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
+ {
+ if (n != 0) {
+ call Theorem3(n-1);
+ }
+ }
+
+ function GaussWithPost(n: int): int
+ requires 0 <= n;
+ ensures 2 * GaussWithPost(n) == n*(n+1);
+ {
+ if n == 0 then 0 else GaussWithPost(n-1) + n
+ }
+
+ // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction
+
+ ghost method Theorem4()
+ ensures (forall n {:induction} :: 0 <= n ==> SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n));
+ {
+ // look ma, no hints!
+ }
+
+ ghost method Theorem5(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n);
+ {
+ // the postcondition is a simple consequence of these quantified versions of the theorem:
+ if (*) {
+ assert (forall m {:induction} :: 0 <= m ==> SumOfCubes(m) == GaussWithPost(m) * GaussWithPost(m));
+ } else {
+ call Theorem4();
+ }
+ }
+}
+
+datatype Tree<T> {
+ Leaf(T);
+ Branch(Tree<T>, Tree<T>);
+}
+
+class DatatypeInduction<T> {
+ function LeafCount<T>(tree: Tree<T>): int
+ {
+ match tree
+ case Leaf(t) => 1
+ case Branch(left, right) => LeafCount(left) + LeafCount(right)
+ }
+
+ method Theorem0(tree: Tree<T>)
+ ensures 1 <= LeafCount(tree);
+ {
+ assert (forall t: Tree<T> {:induction} :: 1 <= LeafCount(t));
+ }
+
+ // see also Test/dafny0/DTypes.dfy for more variations of this example
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 772d4fdb..441062d3 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -20,6 +20,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
SchorrWaite.dfy
Cubes.dfy SumOfCubes.dfy
TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy
+ Induction.dfy
Celebrity.dfy
UltraFilter.dfy) do (
echo.