From 13a88d7263c02590f5be9bb9944c0ab43b76bccc Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 26 Feb 2016 09:56:59 -0800 Subject: Fix issue 136. Less aggressive Lit wrap for assert/assume. --- Source/Dafny/Translator.cs | 235 +-- Test/dafny0/DTypes.dfy | 2 +- Test/dafny0/snapshots/Snapshots0.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots1.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots2.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots3.run.dfy.expect | 6 +- Test/dafny0/snapshots/Snapshots4.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots6.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots7.run.dfy.expect | 4 +- Test/dafny0/snapshots/Snapshots8.run.dfy.expect | 4 +- Test/dafny4/Bug136.dfy | 12 + Test/dafny4/Bug136.dfy.expect | 1772 +++++++++++++++++++++++ 12 files changed, 1924 insertions(+), 131 deletions(-) create mode 100644 Test/dafny4/Bug136.dfy create mode 100644 Test/dafny4/Bug136.dfy.expect diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 52f52abf..c7552a79 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1650,7 +1650,7 @@ namespace Microsoft.Dafny { // Next, we assume about this.* whatever we said that the iterator constructor promises foreach (var p in iter.Member_Init.Ens) { - builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); } // play havoc with the heap, except at the locations prescribed by (this._reads - this._modifies - {this}) @@ -1676,7 +1676,7 @@ namespace Microsoft.Dafny { validCall.TypeArgumentSubstitutions[p] = new UserDefinedType(p); } // resolved here. - builder.Add(new Bpl.AssumeCmd(iter.tok, etran.TrExpr(validCall))); + builder.Add(TrAssumeCmd(iter.tok, etran.TrExpr(validCall))); // check well-formedness of the user-defined part of the yield-requires foreach (var p in iter.YieldRequires) { @@ -1703,13 +1703,13 @@ namespace Microsoft.Dafny { setDiff.ResolvedOp = BinaryExpr.ResolvedOpcode.SetDifference; setDiff.Type = nw.Type; // resolve here Expression cond = new UnaryOpExpr(iter.tok, UnaryOpExpr.Opcode.Fresh, setDiff); cond.Type = Type.Bool; // resolve here - builder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(cond))); + builder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(cond))); // check wellformedness of postconditions var yeBuilder = new Bpl.StmtListBuilder(); var endBuilder = new Bpl.StmtListBuilder(); // In the yield-ensures case: assume this.Valid(); - yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, yeEtran.TrExpr(validCall))); + yeBuilder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(validCall))); Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); for (int i = 0; i < iter.OutsFields.Count; i++) { var y = iter.OutsFields[i]; @@ -1726,9 +1726,9 @@ namespace Microsoft.Dafny { concat.ResolvedOp = BinaryExpr.ResolvedOpcode.Concat; concat.Type = oldThisYs.Type; // resolve here // In the yield-ensures case: assume this.ys == old(this.ys) + [this.y]; - yeBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); + yeBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(concat)))); // In the ensures case: assume this.ys == old(this.ys); - endBuilder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); + endBuilder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(yeEtran.TrExpr(thisYs), yeEtran.TrExpr(oldThisYs)))); } foreach (var p in iter.YieldEnsures) { @@ -1775,18 +1775,18 @@ namespace Microsoft.Dafny { // add locals for the yield-history variables and the extra variables // Assume the precondition and postconditions of the iterator constructor method foreach (var p in iter.Member_Init.Req) { - builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); } foreach (var p in iter.Member_Init.Ens) { // these postconditions are two-state predicates, but that's okay, because we haven't changed anything yet - builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmd(p.E.tok, etran.TrExpr(p.E))); } // add the _yieldCount variable, and assume its initial value to be 0 yieldCountVariable = new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(currentDeclaration.IdGenerator), TrType(iter.YieldCountVariable.Type))); yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran); // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption localVariables.Add(yieldCountVariable); - builder.Add(new Bpl.AssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0)))); + builder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0)))); // add a variable $_OldIterHeap var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType); Bpl.Expr wh = BplAnd( @@ -2789,7 +2789,7 @@ namespace Microsoft.Dafny { if (dt != null) { var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool)); var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type)); - builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List { f }))); + builder.Add(TrAssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List { f }))); } } @@ -2891,7 +2891,7 @@ namespace Microsoft.Dafny { foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) { if (tri.IsFree) { - builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr)); + builder.Add(TrAssumeCmd(m.tok, tri.Expr)); } } @@ -3092,7 +3092,7 @@ namespace Microsoft.Dafny { //generating class post-conditions foreach (var en in f.Ens) { - builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(en))); + builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(en))); } //generating assume J.F(ins) == C.F(ins) @@ -3117,7 +3117,7 @@ namespace Microsoft.Dafny { } Bpl.Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC); Bpl.Expr funcExpT = new Bpl.NAryExpr(f.OverriddenFunction.tok, funcIdT, argsT); - builder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, funcExpT))); + builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, funcExpT))); //generating trait post-conditions with class variables foreach (var en in f.OverriddenFunction.Ens) @@ -3127,7 +3127,7 @@ namespace Microsoft.Dafny { var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened); foreach (var s in reqSplitedE) { - var assert = new Bpl.AssertCmd(f.tok, s.E); + var assert = TrAssertCmd(f.tok, s.E); assert.ErrorData = "Error: the function must provide an equal or more detailed postcondition than in its parent trait"; builder.Add(assert); } @@ -3143,7 +3143,7 @@ namespace Microsoft.Dafny { { if (tri.IsFree) { - builder.Add(new Bpl.AssumeCmd(f.tok, tri.Expr)); + builder.Add(TrAssumeCmd(f.tok, tri.Expr)); } } } @@ -3196,7 +3196,7 @@ namespace Microsoft.Dafny { foreach (var req in f.OverriddenFunction.Req) { Expression precond = Substitute(req, null, substMap); - builder.Add(new Bpl.AssumeCmd(f.tok, etran.TrExpr(precond))); + builder.Add(TrAssumeCmd(f.tok, etran.TrExpr(precond))); } //generating class pre-conditions foreach (var req in f.Req) @@ -3205,7 +3205,7 @@ namespace Microsoft.Dafny { var reqSplitedE = TrSplitExpr(req, etran,false, out splitHappened); foreach (var s in reqSplitedE) { - var assert = new Bpl.AssertCmd(f.tok, s.E); + var assert = TrAssertCmd(f.tok, s.E); assert.ErrorData = "Error: the function must provide an equal or more permissive precondition than in its parent trait"; builder.Add(assert); } @@ -3295,7 +3295,7 @@ namespace Microsoft.Dafny { { if (tri.IsFree) { - builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr)); + builder.Add(TrAssumeCmd(m.tok, tri.Expr)); } } } @@ -3305,7 +3305,7 @@ namespace Microsoft.Dafny { //generating class post-conditions foreach (var en in m.Ens) { - builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(en.E))); + builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(en.E))); } //generating trait post-conditions with class variables foreach (var en in m.OverriddenMethod.Ens) @@ -3315,7 +3315,7 @@ namespace Microsoft.Dafny { var reqSplitedE = TrSplitExpr(postcond, etran,false, out splitHappened); foreach (var s in reqSplitedE) { - var assert = new Bpl.AssertCmd(m.tok, s.E); + var assert = TrAssertCmd(m.tok, s.E); assert.ErrorData = "Error: the method must provide an equal or more detailed postcondition than in its parent trait"; builder.Add(assert); } @@ -3328,7 +3328,7 @@ namespace Microsoft.Dafny { foreach (var req in m.OverriddenMethod.Req) { Expression precond = Substitute(req.E, null, substMap); - builder.Add(new Bpl.AssumeCmd(m.tok, etran.TrExpr(precond))); + builder.Add(TrAssumeCmd(m.tok, etran.TrExpr(precond))); } //generating class pre-conditions foreach (var req in m.Req) @@ -3337,7 +3337,7 @@ namespace Microsoft.Dafny { var reqSplitedE = TrSplitExpr(req.E, etran,false, out splitHappened); foreach (var s in reqSplitedE) { - var assert = new Bpl.AssertCmd(m.tok, s.E); + var assert = TrAssertCmd(m.tok, s.E); assert.ErrorData = "Error: the method must provide an equal or more permissive precondition than in its parent trait"; builder.Add(assert); } @@ -3617,7 +3617,7 @@ namespace Microsoft.Dafny { var col = tok.col + (isEndToken ? tok.val.Length : 0); string description = ErrorReporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, col, additionalInfo ?? ""); QKeyValue kv = new QKeyValue(tok, "captureState", new List() { description }, null); - return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv); + return TrAssumeCmd(tok, Bpl.Expr.True, kv); } Bpl.Cmd CaptureState(Statement stmt) { Contract.Requires(stmt != null); @@ -4086,7 +4086,7 @@ namespace Microsoft.Dafny { var wh = GetWhereClause(f.tok, funcAppl, f.ResultType, etran); if (wh != null) { - postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, wh)); + postCheckBuilder.Add(TrAssumeCmd(f.tok, wh)); } } // Now for the ensures clauses @@ -4098,7 +4098,7 @@ namespace Microsoft.Dafny { StmtListBuilder bodyCheckBuilder = new StmtListBuilder(); if (f.Body == null) { // don't fall through to postcondition checks - bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False)); + bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False)); } else { Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType))); List args = new List(); @@ -4126,7 +4126,7 @@ namespace Microsoft.Dafny { wfo.ProcessSavedReadsChecks(locals, builderInitializationArea, bodyCheckBuilder); } // Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch - postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False)); + postCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False)); builder.Add(new Bpl.IfCmd(f.tok, null, postCheckBuilder.Collect(f.tok), null, bodyCheckBuilder.Collect(f.tok))); var s0 = builderInitializationArea.Collect(f.tok); @@ -4241,7 +4241,7 @@ namespace Microsoft.Dafny { Type t = mc.Ctor.Formals[i].Type; Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, local), p.Type, etran); if (wh != null) { - localTypeAssumptions.Add(new Bpl.AssumeCmd(p.tok, wh)); + localTypeAssumptions.Add(TrAssumeCmd(p.tok, wh)); } args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t)); } @@ -4555,7 +4555,7 @@ namespace Microsoft.Dafny { var correctConstructor = FunctionCall(pat.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, rhs); if (ctor.EnclosingDatatype.Ctors.Count == 1) { // There is only one constructor, so the value must have been constructed by it; might as well assume that here. - builder.Add(new Bpl.AssumeCmd(pat.tok, correctConstructor)); + builder.Add(TrAssumeCmd(pat.tok, correctConstructor)); } else { builder.Add(Assert(pat.tok, correctConstructor, string.Format("RHS is not certain to look like the pattern '{0}'", ctor.Name))); } @@ -4691,7 +4691,7 @@ namespace Microsoft.Dafny { kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null); } CheckWellformed(expr, new WFOptions(kv), locals, builder, etran); - builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran))); + builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); } void CheckWellformedAndAssume(Expression expr, WFOptions options, List locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) { @@ -4720,7 +4720,7 @@ namespace Microsoft.Dafny { CheckWellformedAndAssume(e.E0, options, locals, bAnd, etran); CheckWellformedAndAssume(e.E1, options, locals, bAnd, etran); var bImp = new Bpl.StmtListBuilder(); - bImp.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr))); + bImp.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr))); builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok))); } return; @@ -4734,7 +4734,7 @@ namespace Microsoft.Dafny { var b0 = new Bpl.StmtListBuilder(); CheckWellformedAndAssume(e.E0, options, locals, b0, etran); var b1 = new Bpl.StmtListBuilder(); - b1.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)))); + b1.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)))); CheckWellformedAndAssume(e.E1, options, locals, b1, etran); builder.Add(new Bpl.IfCmd(expr.tok, null, b0.Collect(expr.tok), null, b1.Collect(expr.tok))); } @@ -4755,7 +4755,7 @@ namespace Microsoft.Dafny { CheckWellformedAndAssume(e.Test, options, locals, bThn, etran); CheckWellformedAndAssume(e.Thn, options, locals, bThn, etran); var bEls = new Bpl.StmtListBuilder(); - bEls.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.Test)))); + bEls.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.Test)))); CheckWellformedAndAssume(e.Els, options, locals, bEls, etran); builder.Add(new Bpl.IfCmd(expr.tok, null, bThn.Collect(expr.tok), null, bEls.Collect(expr.tok))); return; @@ -4781,7 +4781,7 @@ namespace Microsoft.Dafny { if (e is ForallExpr) { // Although we do the WF check on the original quantifier, we assume the split one. // This ensures that cases like forall x :: x != null && f(x.a) do not fail to verify. - builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(e.SplitQuantifierExpression ?? e))); + builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(e.SplitQuantifierExpression ?? e))); } return; } @@ -4793,7 +4793,7 @@ namespace Microsoft.Dafny { // the splitting and proceeded to decompose the full quantifier as // normal. This call to TrExpr, on the other hand, will indeed use the // split quantifier. - builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr))); + builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(expr))); } /// @@ -4852,7 +4852,7 @@ namespace Microsoft.Dafny { var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullSanitizedName, Bpl.Type.Bool, etran.TrExpr(e.Obj)); if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) { // There is only one constructor, so the value must be been constructed by it; might as well assume that here. - builder.Add(new Bpl.AssumeCmd(expr.tok, correctConstructor)); + builder.Add(TrAssumeCmd(expr.tok, correctConstructor)); } else { builder.Add(Assert(expr.tok, correctConstructor, string.Format("destructor '{0}' can only be applied to datatype values constructed by '{1}'", dtor.Name, dtor.EnclosingCtor.Name))); @@ -5048,7 +5048,7 @@ namespace Microsoft.Dafny { if (!etran.UsesOldHeap) { // the argument can't be assumed to be allocated for the old heap builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function")); - builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr))); + builder.Add(TrAssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr))); } } // Check that every parameter is available in the state in which the function is invoked; this means checking that it has @@ -5087,7 +5087,7 @@ namespace Microsoft.Dafny { } if (options.AssertKv == null) { // assume only if no given assert attribute is given - builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(precond))); + builder.Add(TrAssumeCmd(expr.tok, etran.TrExpr(precond))); } } if (options.DoReadsChecks) { @@ -5148,7 +5148,7 @@ namespace Microsoft.Dafny { Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullSanitizedName + "#canCall", Bpl.Type.Bool); List args = etran.FunctionInvocationArguments(e, null); Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args); - builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl))); + builder.Add(TrAssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl))); } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; @@ -5245,7 +5245,7 @@ namespace Microsoft.Dafny { var rIe = new Bpl.IdentifierExpr(pat.tok, r); CheckWellformedWithResult(e.RHSs[i], options, rIe, pat.Expr.Type, locals, builder, etran); CheckCasePatternShape(pat, rIe, builder); - builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe))); + builder.Add(TrAssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(Substitute(pat.Expr, null, substMap)), rIe))); } CheckWellformedWithResult(Substitute(e.Body, null, substMap), options, result, resultType, locals, builder, etran); result = null; @@ -5276,7 +5276,7 @@ namespace Microsoft.Dafny { w = BplOr(body, w); } builder.Add(Assert(e.tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate")); - builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(rhs))); + builder.Add(TrAssumeCmd(e.tok, etran.TrExpr(rhs))); var letBody = Substitute(e.Body, null, substMap); CheckWellformed(letBody, options, locals, builder, etran); if (e.Constraint_Bounds != null) { @@ -5284,9 +5284,9 @@ namespace Microsoft.Dafny { var substMap_prime = SetupBoundVarsAsLocals(lhsVars, builder, locals, etran); var rhs_prime = Substitute(e.RHSs[0], null, substMap_prime); var letBody_prime = Substitute(e.Body, null, substMap_prime); - builder.Add(new Bpl.AssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran))); - builder.Add(new Bpl.AssumeCmd(e.tok, etran.TrExpr(rhs_prime))); - builder.Add(new Bpl.AssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran))); + builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(rhs_prime, etran))); + builder.Add(TrAssumeCmd(e.tok, etran.TrExpr(rhs_prime))); + builder.Add(TrAssumeCmd(e.tok, CanCallAssumption(letBody_prime, etran))); var eq = Expression.CreateEq(letBody, letBody_prime, e.Body.Type); builder.Add(Assert(e.tok, etran.TrExpr(eq), "to be compilable, the value of a let-such-that expression must be uniquely determined")); } @@ -5295,11 +5295,11 @@ namespace Microsoft.Dafny { Contract.Assert(resultType != null); var bResult = etran.TrExpr(letBody); CheckSubrange(letBody.tok, bResult, resultType, builder); - builder.Add(new Bpl.AssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult))); - builder.Add(new Bpl.AssumeCmd(letBody.tok, CanCallAssumption(letBody, etran))); + builder.Add(TrAssumeCmd(letBody.tok, Bpl.Expr.Eq(result, bResult))); + builder.Add(TrAssumeCmd(letBody.tok, CanCallAssumption(letBody, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: Let expression")); - builder.Add(new Bpl.AssumeCmd(letBody.tok, MkIsAlloc(result, resultType, etran.HeapExpr))); - builder.Add(new Bpl.AssumeCmd(letBody.tok, MkIs(result, resultType))); + builder.Add(TrAssumeCmd(letBody.tok, MkIsAlloc(result, resultType, etran.HeapExpr))); + builder.Add(TrAssumeCmd(letBody.tok, MkIs(result, resultType))); result = null; } } @@ -5406,7 +5406,7 @@ namespace Microsoft.Dafny { Bpl.Expr src = etran.TrExpr(me.Source); Bpl.IfCmd ifCmd = null; StmtListBuilder elsBldr = new StmtListBuilder(); - elsBldr.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.False)); + elsBldr.Add(TrAssumeCmd(expr.tok, Bpl.Expr.False)); StmtList els = elsBldr.Collect(expr.tok); foreach (var missingCtor in me.MissingCases) { // havoc all bound variables @@ -5460,11 +5460,11 @@ namespace Microsoft.Dafny { Contract.Assert(resultType != null); var bResult = etran.TrExpr(expr); CheckSubrange(expr.tok, bResult, resultType, builder); - builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult))); - builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran))); + builder.Add(TrAssumeCmd(expr.tok, Bpl.Expr.Eq(result, bResult))); + builder.Add(TrAssumeCmd(expr.tok, CanCallAssumption(expr, etran))); builder.Add(new CommentCmd("CheckWellformedWithResult: any expression")); - builder.Add(new Bpl.AssumeCmd(expr.tok, MkIsAlloc(result, resultType, etran.HeapExpr))); - builder.Add(new Bpl.AssumeCmd(expr.tok, MkIs(result, resultType))); + builder.Add(TrAssumeCmd(expr.tok, MkIsAlloc(result, resultType, etran.HeapExpr))); + builder.Add(TrAssumeCmd(expr.tok, MkIs(result, resultType))); } } @@ -6499,7 +6499,7 @@ namespace Microsoft.Dafny { foreach (var p in m.Ens) { bool splitHappened; // we actually don't care foreach (var s in TrSplitExpr(p.E, etran, true, out splitHappened)) { - var assert = new Bpl.AssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold.")); + var assert = TrAssertCmd(method.tok, s.E, ErrorMessageAttribute(s.E.tok, "This is the postcondition that may not hold.")); assert.ErrorData = "Error: A postcondition of the refined method may not hold."; builder.Add(assert); } @@ -6984,9 +6984,9 @@ namespace Microsoft.Dafny { if (assertAsAssume || (RefinementToken.IsInherited(refinesToken, currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce an assume instead - return new Bpl.AssumeCmd(tok, condition, kv); + return TrAssumeCmd(tok, condition, kv); } else { - var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv); + var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv); cmd.ErrorData = "Error: " + errorMessage; return cmd; } @@ -7003,12 +7003,12 @@ namespace Microsoft.Dafny { if (RefinementToken.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify)) { // produce a "skip" instead - return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv); + return TrAssumeCmd(tok, Bpl.Expr.True, kv); } else { tok = ForceCheckToken.Unwrap(tok); var args = new List(); args.Add(Bpl.Expr.Literal(0)); - Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, new Bpl.QKeyValue(tok, "subsumption", args, kv)); + Bpl.AssertCmd cmd = TrAssertCmd(tok, condition, new Bpl.QKeyValue(tok, "subsumption", args, kv)); cmd.ErrorData = "Error: " + errorMessage; return cmd; } @@ -7022,9 +7022,9 @@ namespace Microsoft.Dafny { if (assertAsAssume || (RefinementToken.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce an assume instead - return new Bpl.AssumeCmd(tok, condition, kv); + return TrAssumeCmd(tok, condition, kv); } else { - var cmd = new Bpl.AssertCmd(ForceCheckToken.Unwrap(tok), condition, kv); + var cmd = TrAssertCmd(ForceCheckToken.Unwrap(tok), condition, kv); cmd.ErrorData = "Error: " + errorMessage; return cmd; } @@ -7097,13 +7097,13 @@ namespace Microsoft.Dafny { builder.Add(AssertNS(tok, split.E, "assertion violation", stmt.Tok, etran.TrAttributes(stmt.Attributes, null))); // attributes go on every split } } - builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr))); + builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr))); } } else if (stmt is AssumeStmt) { AddComment(builder, stmt, "assume statement"); AssumeStmt s = (AssumeStmt)stmt; TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false); - builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null))); + builder.Add(TrAssumeCmd(stmt.Tok, etran.TrExpr(s.Expr), etran.TrAttributes(stmt.Attributes, null))); } this.fuelContext = FuelSetting.PopFuelContext(); } else if (stmt is PrintStmt) { @@ -7161,7 +7161,7 @@ namespace Microsoft.Dafny { var yc = new Bpl.IdentifierExpr(s.Tok, yieldCountVariable); var incYieldCount = Bpl.Cmd.SimpleAssign(s.Tok, yc, Bpl.Expr.Binary(s.Tok, Bpl.BinaryOperator.Opcode.Add, yc, Bpl.Expr.Literal(1))); builder.Add(incYieldCount); - builder.Add(new Bpl.AssumeCmd(s.Tok, YieldCountAssumption(iter, etran))); + builder.Add(TrAssumeCmd(s.Tok, YieldCountAssumption(iter, etran))); // assume $IsGoodHeap($Heap); builder.Add(AssumeGoodHeap(s.Tok, etran)); // assert YieldEnsures[subst]; // where 'subst' replaces "old(E)" with "E" being evaluated in $_OldIterHeap @@ -7180,7 +7180,7 @@ namespace Microsoft.Dafny { builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok, null)); } } - builder.Add(new Bpl.AssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E))); + builder.Add(TrAssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E))); } } YieldHavoc(iter.tok, iter, builder, etran); @@ -7245,7 +7245,7 @@ namespace Microsoft.Dafny { builder.Add(Assert(s.Tok, w, "cannot establish the existence of LHS values that satisfy the such-that predicate")); } // End by doing the assume - builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Expr))); + builder.Add(TrAssumeCmd(s.Tok, etran.TrExpr(s.Expr))); builder.Add(CaptureState(s)); // just do one capture state--here, at the very end (that is, don't do one before the assume) } else if (stmt is UpdateStmt) { @@ -7320,7 +7320,7 @@ namespace Microsoft.Dafny { Bpl.IfCmd elsIf = null; b = new Bpl.StmtListBuilder(); if (s.IsExistentialGuard) { - b.Add(new Bpl.AssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard)))); + b.Add(TrAssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard)))); } if (s.Els == null) { els = b.Collect(s.Tok); @@ -7383,11 +7383,11 @@ namespace Microsoft.Dafny { // havoc $Heap; builder.Add(new Bpl.HavocCmd(s.Tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); // assume $HeapSucc(preModifyHeap, $Heap); OR $HeapSuccGhost - builder.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost))); + builder.Add(TrAssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost))); // assume nothing outside the frame was changed var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap); var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName); - builder.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran))); + builder.Add(TrAssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran))); } else { // do the body, but with preModifyHeapVar as the governing frame var updatedFrameEtran = new ExpressionTranslator(etran, modifyFrameName); @@ -7486,7 +7486,7 @@ namespace Microsoft.Dafny { if (s.Steps[i] is BinaryExpr && (((BinaryExpr)s.Steps[i]).ResolvedOp == BinaryExpr.ResolvedOpcode.Imp)) { // assume line: AddComment(b, stmt, "assume lhs"); - b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i])))); + b.Add(TrAssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i])))); } // hint: AddComment(b, stmt, "Hint" + i.ToString()); @@ -7514,7 +7514,7 @@ namespace Microsoft.Dafny { } } } - b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + b.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null); CurrentIdGenerator.Pop(); } @@ -7523,12 +7523,12 @@ namespace Microsoft.Dafny { AddComment(b, stmt, "assert wf[initial]"); Contract.Assert(s.Result != null); // established by the resolver TrStmt_CheckWellformed(CalcStmt.Lhs(s.Result), b, locals, etran, false); - b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + b.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null); builder.Add(ifCmd); // assume result: if (s.Steps.Count > 1) { - builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result))); + builder.Add(TrAssumeCmd(s.Tok, etran.TrExpr(s.Result))); } } CurrentIdGenerator.Pop(); @@ -7539,7 +7539,7 @@ namespace Microsoft.Dafny { Bpl.Expr source = etran.TrExpr(s.Source); var b = new Bpl.StmtListBuilder(); - b.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False)); + b.Add(TrAssumeCmd(stmt.Tok, Bpl.Expr.False)); Bpl.StmtList els = b.Collect(stmt.Tok); Bpl.IfCmd ifCmd = null; foreach (var missingCtor in s.MissingCases) { @@ -7617,7 +7617,7 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.HavocCmd(bv.Tok, new List { bIe })); Bpl.Expr wh = GetWhereClause(bv.Tok, bIe, bv.Type, etran); if (wh != null) { - builder.Add(new Bpl.AssumeCmd(bv.Tok, wh)); + builder.Add(TrAssumeCmd(bv.Tok, wh)); } } Contract.Assert(s.LHSs.Count == s.RHSs.Count); // checked by resolution @@ -7632,7 +7632,7 @@ namespace Microsoft.Dafny { TrStmt_CheckWellformed(s.RHSs[i], builder, locals, etran, false); CheckWellformedWithResult(s.RHSs[i], new WFOptions(null, false, false), rIe, pat.Expr.Type, locals, builder, etran); CheckCasePatternShape(pat, rIe, builder); - builder.Add(new Bpl.AssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(pat.Expr), rIe))); + builder.Add(TrAssumeCmd(pat.tok, Bpl.Expr.Eq(etran.TrExpr(pat.Expr), rIe))); } } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement @@ -7656,7 +7656,7 @@ namespace Microsoft.Dafny { iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local)); } builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc)); - builder.Add(new Bpl.AssumeCmd(exists.tok, etran.TrExpr(exists.Term))); + builder.Add(TrAssumeCmd(exists.tok, etran.TrExpr(exists.Term))); } void TrStmtList(List stmts, Bpl.StmtListBuilder builder, List locals, ExpressionTranslator etran) { @@ -7738,7 +7738,7 @@ namespace Microsoft.Dafny { new List())); // assume YieldRequires; foreach (var p in iter.YieldRequires) { - builder.Add(new Bpl.AssumeCmd(tok, etran.TrExpr(p.E))); + builder.Add(TrAssumeCmd(tok, etran.TrExpr(p.E))); } // $_OldIterHeap := Heap; builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr)); @@ -7953,7 +7953,7 @@ namespace Microsoft.Dafny { var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); Expression range = Substitute(s.Range, null, substMap); TrStmt_CheckWellformed(range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range))); + definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(range))); var lhs = Substitute(s0.Lhs.Resolved, null, substMap); TrStmt_CheckWellformed(lhs, definedness, locals, etran, false); @@ -7989,7 +7989,7 @@ namespace Microsoft.Dafny { var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime); range = Substitute(s.Range, null, substMapPrime); - definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); + definedness.Add(TrAssumeCmd(range.tok, etran.TrExpr(range))); // assume !(x == x' && y == y'); Bpl.Expr eqs = Bpl.Expr.True; foreach (var bv in s.BoundVars) { @@ -7998,7 +7998,7 @@ namespace Microsoft.Dafny { // TODO: in the following line, is the term equality okay, or does it have to include things like Set#Equal sometimes too? eqs = BplAnd(eqs, Bpl.Expr.Eq(etran.TrExpr(x), etran.TrExpr(xPrime))); } - definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.Not(eqs))); + definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.Not(eqs))); Bpl.Expr objPrime, FPrime; GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime); var Rhs = ((ExprRhs)s0.Rhs).Expr; @@ -8011,7 +8011,7 @@ namespace Microsoft.Dafny { "left-hand sides for different forall-statement bound variables may refer to the same location")); } - definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); // Now for the translation of the update itself @@ -8019,7 +8019,7 @@ namespace Microsoft.Dafny { var prevEtran = new ExpressionTranslator(this, predef, prevHeap); updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr)); updater.Add(new Bpl.HavocCmd(s.Tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); - updater.Add(new Bpl.AssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr))); + updater.Add(TrAssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr))); // Here comes: // assume (forall o: ref, f: Field alpha :: @@ -8046,7 +8046,7 @@ namespace Microsoft.Dafny { Bpl.Expr body = Bpl.Expr.Or(Bpl.Expr.Eq(heapOF, oldHeapOF), xObjField); var tr = new Trigger(s.Tok, true, new List() { heapOF }); Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List { alpha }, new List { oVar, fVar }, null, tr, body); - updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); + updater.Add(TrAssumeCmd(s.Tok, qq)); if (s.ForallExpressions != null) { foreach (ForallExpr expr in s.ForallExpressions) { @@ -8055,7 +8055,7 @@ namespace Microsoft.Dafny { var e0 = Substitute(((BinaryExpr)term).E0.Resolved, null, substMap); var e1 = Substitute(((BinaryExpr)term).E1, null, substMap); qq = TrForall_NewValueAssumption(expr.tok, expr.BoundVars, expr.Range, e0, e1, expr.Attributes, etran, prevEtran); - updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); + updater.Add(TrAssumeCmd(s.Tok, qq)); } } } @@ -8158,18 +8158,18 @@ namespace Microsoft.Dafny { havocIds.Add(new Bpl.IdentifierExpr(tok, bv)); } definedness.Add(new Bpl.HavocCmd(tok, havocIds)); - definedness.Add(new Bpl.AssumeCmd(tok, ante)); + definedness.Add(TrAssumeCmd(tok, ante)); } TrStmt_CheckWellformed(range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); + definedness.Add(TrAssumeCmd(range.tok, etran.TrExpr(range))); if (additionalRange != null) { var es = additionalRange(new Dictionary(), etran); - definedness.Add(new Bpl.AssumeCmd(es.tok, es)); + definedness.Add(TrAssumeCmd(es.tok, es)); } TrStmt(s0, definedness, locals, etran); - definedness.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.False)); + definedness.Add(TrAssumeCmd(tok, Bpl.Expr.False)); } // Now for the other branch, where the postcondition of the call is exported. @@ -8186,7 +8186,7 @@ namespace Microsoft.Dafny { Contract.Assert(s0.Method.Mod.Expressions.Count == 0); // checked by the resolver foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List(), s0.IsGhost, initEtran, etran, initEtran)) { if (tri.IsFree) { - exporter.Add(new Bpl.AssumeCmd(tok, tri.Expr)); + exporter.Add(TrAssumeCmd(tok, tri.Expr)); } } if (codeContext is IteratorDecl) { @@ -8214,7 +8214,7 @@ namespace Microsoft.Dafny { var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals qq = callEtran.TrExpr(p, initEtran); - exporter.Add(new Bpl.AssumeCmd(tok, qq)); + exporter.Add(TrAssumeCmd(tok, qq)); } } else { var bvars = new List(); @@ -8242,7 +8242,7 @@ namespace Microsoft.Dafny { // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER - exporter.Add(new Bpl.AssumeCmd(tok, qq)); + exporter.Add(TrAssumeCmd(tok, qq)); } } } @@ -8309,10 +8309,10 @@ namespace Microsoft.Dafny { havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv)); } definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds)); - definedness.Add(new Bpl.AssumeCmd(s.Tok, typeAntecedent)); + definedness.Add(TrAssumeCmd(s.Tok, typeAntecedent)); } TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); + definedness.Add(TrAssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); if (s.Body != null) { TrStmt(s.Body, definedness, locals, etran); @@ -8330,7 +8330,7 @@ namespace Microsoft.Dafny { } } - definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + definedness.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); // Now for the other branch, where the ensures clauses are exported. @@ -8344,7 +8344,7 @@ namespace Microsoft.Dafny { exporter.Add(new Bpl.HavocCmd(s.Tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick() })); foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, new List(), s.IsGhost, initEtran, etran, initEtran)) { if (tri.IsFree) { - exporter.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr)); + exporter.Add(TrAssumeCmd(s.Tok, tri.Expr)); } } @@ -8352,9 +8352,9 @@ namespace Microsoft.Dafny { var p = Substitute(s.ForallExpressions[0], null, substMap); Bpl.Expr qq = etran.TrExpr(p, initEtran); if (s.BoundVars.Count != 0) { - exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); + exporter.Add(TrAssumeCmd(s.Tok, qq)); } else { - exporter.Add(new Bpl.AssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body)); + exporter.Add(TrAssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body)); } } @@ -8379,6 +8379,15 @@ namespace Microsoft.Dafny { return description; } + Bpl.AssumeCmd TrAssumeCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) { + var lit = RemoveLit(expr); + return attributes == null ? new Bpl.AssumeCmd(tok, lit) : new Bpl.AssumeCmd(tok, lit, attributes); + } + + Bpl.AssertCmd TrAssertCmd(IToken tok, Bpl.Expr expr, Bpl.QKeyValue attributes = null) { + var lit = RemoveLit(expr); + return attributes == null ? new Bpl.AssertCmd(tok, lit) : new Bpl.AssertCmd(tok, lit, attributes); + } delegate void BodyTranslator(Bpl.StmtListBuilder builder, ExpressionTranslator etran); @@ -8427,11 +8436,11 @@ namespace Microsoft.Dafny { Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder(); foreach (MaybeFreeExpression loopInv in s.Invariants) { TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false); - invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E))); + invDefinednessBuilder.Add(TrAssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E))); - invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran)))); + invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran)))); if (loopInv.IsFree && !DafnyOptions.O.DisallowSoundnessCheating) { - invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E)))); + invariants.Add(TrAssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E)))); } else { bool splitHappened; var ss = TrSplitExpr(loopInv.E, etran, false, out splitHappened); @@ -8444,7 +8453,7 @@ namespace Microsoft.Dafny { if (split.IsChecked) { invariants.Add(Assert(split.E.tok, wInv, "loop invariant violation")); // TODO: it would be fine to have this use {:subsumption 0} } else { - invariants.Add(new Bpl.AssumeCmd(split.E.tok, wInv)); + invariants.Add(TrAssumeCmd(split.E.tok, wInv)); } } } @@ -8460,14 +8469,14 @@ namespace Microsoft.Dafny { // include boilerplate invariants foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, modifiesClause, s.IsGhost, etranPreLoop, etran, etran.Old)) { if (tri.IsFree) { - invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr)); + invariants.Add(TrAssumeCmd(s.Tok, tri.Expr)); } else { Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage)); } } // add a free invariant which says that the heap hasn't changed outside of the modifies clause. - invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran))); + invariants.Add(TrAssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran))); } // include a free invariant that says that all completed iterations so far have only decreased the termination metric @@ -8481,13 +8490,13 @@ namespace Microsoft.Dafny { decrs.Add(etran.TrExpr(e)); } Bpl.Expr decrCheck = DecreasesCheck(toks, types, types, decrs, initDecr, null, null, true, false); - invariants.Add(new Bpl.AssumeCmd(s.Tok, decrCheck)); + invariants.Add(TrAssumeCmd(s.Tok, decrCheck)); } Bpl.StmtListBuilder loopBodyBuilder = new Bpl.StmtListBuilder(); loopBodyBuilder.Add(CaptureState(s.Tok, true, "after some loop iterations")); // as the first thing inside the loop, generate: if (!w) { CheckWellformed(inv); assume false; } - invDefinednessBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + invDefinednessBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(s.Tok), null, null)); // generate: CheckWellformed(guard); if (!guard) { break; } Bpl.Expr guard = null; @@ -8528,13 +8537,13 @@ namespace Microsoft.Dafny { loopBodyBuilder.Add(Assert(s.Tok, decrCheck, msg)); } } else { - loopBodyBuilder.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + loopBodyBuilder.Add(TrAssumeCmd(s.Tok, Bpl.Expr.False)); // todo(maria): havoc stuff } // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check // of invariant-maintenance can use the appropriate canCall predicates. foreach (MaybeFreeExpression loopInv in s.Invariants) { - loopBodyBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran))); + loopBodyBuilder.Add(TrAssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran))); } Bpl.StmtList body = loopBodyBuilder.Collect(s.Tok); @@ -8569,7 +8578,7 @@ namespace Microsoft.Dafny { var b = new Bpl.StmtListBuilder(); var elseTok = elseCase0 != null ? elseCase0.tok : elseCase1.tok; - b.Add(new Bpl.AssumeCmd(elseTok, noGuard)); + b.Add(TrAssumeCmd(elseTok, noGuard)); if (elseCase0 != null) { b.Add(elseCase0); } else { @@ -8838,7 +8847,7 @@ namespace Microsoft.Dafny { // the out-parameter. Bpl.Cmd cmd = new Bpl.HavocCmd(bLhs.tok, new List { bLhs }); builder.Add(cmd); - cmd = new Bpl.AssumeCmd(bLhs.tok, Bpl.Expr.Eq(bLhs, FunctionCall(bLhs.tok, BuiltinFunction.Unbox, TrType(LhsTypes[i]), tmpVarIdE))); + cmd = TrAssumeCmd(bLhs.tok, Bpl.Expr.Eq(bLhs, FunctionCall(bLhs.tok, BuiltinFunction.Unbox, TrType(LhsTypes[i]), tmpVarIdE))); builder.Add(cmd); } } @@ -8866,7 +8875,7 @@ namespace Microsoft.Dafny { builder.Add(new Bpl.HavocCmd(bv.tok, new List { bIe })); Bpl.Expr wh = GetWhereClause(bv.tok, bIe, local.Type, etran); if (wh != null) { - builder.Add(new Bpl.AssumeCmd(bv.tok, wh)); + builder.Add(TrAssumeCmd(bv.tok, wh)); } } return substMap; @@ -9792,7 +9801,7 @@ namespace Microsoft.Dafny { } else if (rhs is HavocRhs) { builder.Add(new Bpl.HavocCmd(tok, new List { bLhs })); var isNat = CheckSubrange_Expr(tok, bLhs, rhsTypeConstraint); - builder.Add(new Bpl.AssumeCmd(tok, isNat)); + builder.Add(TrAssumeCmd(tok, isNat)); return CondApplyBox(tok, bLhs, rhsTypeConstraint, lhsType); } else { // x := new Something @@ -9817,13 +9826,13 @@ namespace Microsoft.Dafny { Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null); Bpl.Expr rightType; rightType = etran.GoodRef_(tok, nw, tRhs.Type, true); - builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType))); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType))); if (tRhs.ArrayDimensions != null) { int i = 0; foreach (Expression dim in tRhs.ArrayDimensions) { // assume Array#Length($nw, i) == arraySize; Bpl.Expr arrayLength = ArrayLength(tok, nw, tRhs.ArrayDimensions.Count, i); - builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim)))); + builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(arrayLength, etran.TrExpr(dim)))); i++; } } @@ -9929,7 +9938,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null); Contract.Ensures(Contract.Result() != null); - return new Bpl.AssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr)); + return TrAssumeCmd(tok, FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr)); } /// diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index 9e36e64c..9891c040 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect index d32cd9bb..bf7388cf 100644 --- a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 3 verified, 0 errors @@ -16,7 +16,7 @@ Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall $o: ref, $f >>> MarkAsFullyVerified Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap); >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots0.v1.dfy(4,10)) assert false; >>> MarkAsPartiallyVerified Snapshots0.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect index 6d5e43f8..1b5c8d24 100644 --- a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots1.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Processing command (at Snapshots1.v0.dfy(12,3)) assert true; >>> DoNothingToAssert @@ -12,7 +12,7 @@ Processing command (at Snapshots1.v1.dfy(12,3)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> MarkAsFullyVerified -Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots1.v1.dfy(4,10)) assert false; >>> DoNothingToAssert Snapshots1.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect index ee2ceecd..949ecec9 100644 --- a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect @@ -1,6 +1,6 @@ Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> DoNothingToAssert -Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots2.v0.dfy(4,10)) assert false; >>> DoNothingToAssert Processing command (at Snapshots2.v0.dfy(11,11)) assert true; >>> DoNothingToAssert @@ -24,7 +24,7 @@ Processing command (at Snapshots2.v1.dfy(18,3)) assert true; >>> MarkAsFullyVerified Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]); >>> MarkAsFullyVerified -Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false); +Processing command (at Snapshots2.v1.dfy(4,10)) assert false; >>> DoNothingToAssert Snapshots2.v1.dfy(4,9): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect index accacd90..a7f05a68 100644 --- a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect @@ -1,4 +1,4 @@ -Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v0.dfy(9,14)) assert 0 != 0; >>> DoNothingToAssert Snapshots3.v0.dfy(9,13): Error: assertion violation Execution trace: @@ -6,9 +6,9 @@ Execution trace: (0,0): anon3_Else Dafny program verifier finished with 1 verified, 1 error -Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true); +Processing command (at Snapshots3.v1.dfy(5,12)) assert true; >>> DoNothingToAssert -Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0); +Processing command (at Snapshots3.v1.dfy(9,14)) assert 0 != 0; >>> RecycleError Snapshots3.v0.dfy(9,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect index d56eb9d0..e0f07849 100644 --- a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect @@ -2,11 +2,11 @@ Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0); >>> DoNothingToAssert Dafny program verifier finished with 2 verified, 0 errors -Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1); +Processing command (at Snapshots4.v1.dfy(5,14)) assert 1 != 1; >>> DoNothingToAssert Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0); >>> MarkAsFullyVerified -Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2); +Processing command (at Snapshots4.v1.dfy(10,14)) assert 2 != 2; >>> DoNothingToAssert Snapshots4.v1.dfy(5,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect index bef5a87d..cdb942bb 100644 --- a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect @@ -1,8 +1,8 @@ -Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false); +Processing command (at Snapshots6.v0.dfy(20,14)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 4 verified, 0 errors -Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false); +Processing command (at Snapshots6.v1.dfy(20,14)) assert false; >>> DoNothingToAssert Snapshots6.v1.dfy(20,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect index b90a6034..a08b32c6 100644 --- a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect @@ -1,4 +1,4 @@ -Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false); +Processing command (at Snapshots7.v0.dfy(19,14)) assert false; >>> DoNothingToAssert Dafny program verifier finished with 4 verified, 0 errors @@ -22,7 +22,7 @@ Processing command (at ) a##cached##0 := a##cached##0 && ##ext >>> AssumeNegationOfAssumptionVariable Processing command (at ) a##cached##0 := a##cached##0 && ##extracted_function##4(); >>> AssumeNegationOfAssumptionVariable -Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false); +Processing command (at Snapshots7.v1.dfy(19,14)) assert false; >>> MarkAsPartiallyVerified Snapshots7.v1.dfy(19,13): Error: assertion violation Execution trace: diff --git a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect index 625b71b4..e1cbdbe0 100644 --- a/Test/dafny0/snapshots/Snapshots8.run.dfy.expect +++ b/Test/dafny0/snapshots/Snapshots8.run.dfy.expect @@ -20,7 +20,7 @@ Snapshots8.v0.dfy(13,12): Related location: This is the postcondition that might Processing command (at Snapshots8.v0.dfy(23,12)) assert u#0 != 53; >>> DoNothingToAssert Snapshots8.v0.dfy(23,11): Error: assertion violation -Processing command (at Snapshots8.v0.dfy(28,10)) assert Lit(true); +Processing command (at Snapshots8.v0.dfy(28,10)) assert true; >>> DoNothingToAssert Dafny program verifier finished with 7 verified, 4 errors @@ -45,7 +45,7 @@ Snapshots8.v1.dfy(12,20): Related location: This is the precondition that might Snapshots8.v1.dfy(7,11): Error: assertion violation Processing command (at Snapshots8.v1.dfy(21,12)) assert true; >>> MarkAsFullyVerified -Processing command (at Snapshots8.v1.dfy(23,12)) assert Lit(true); +Processing command (at Snapshots8.v1.dfy(23,12)) assert true; >>> DoNothingToAssert Processing command (at Snapshots8.v1.dfy(19,13)) assert LitInt(2) <= z#0; >>> DoNothingToAssert diff --git a/Test/dafny4/Bug136.dfy b/Test/dafny4/Bug136.dfy new file mode 100644 index 00000000..5f3cde69 --- /dev/null +++ b/Test/dafny4/Bug136.dfy @@ -0,0 +1,12 @@ +// RUN: %dafny /compile:0 /print:- "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method test() +{ + assume false; + assert true; +} + + + + diff --git a/Test/dafny4/Bug136.dfy.expect b/Test/dafny4/Bug136.dfy.expect new file mode 100644 index 00000000..8b9d32a8 --- /dev/null +++ b/Test/dafny4/Bug136.dfy.expect @@ -0,0 +1,1772 @@ +// Dafny program verifier version 1.9.6.21116, Copyright (c) 2003-2015, Microsoft. +// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /compile:0 /print:- c:\dafny\Test\dafny4\Bug136.dfy + +const $$Language$Dafny: bool; + +axiom $$Language$Dafny; + +type Ty; + +const unique TBool: Ty; + +const unique TChar: Ty; + +const unique TInt: Ty; + +const unique TNat: Ty; + +const unique TReal: Ty; + +function TSet(Ty) : Ty; + +function TISet(Ty) : Ty; + +function TMultiSet(Ty) : Ty; + +function TSeq(Ty) : Ty; + +function TMap(Ty, Ty) : Ty; + +function TIMap(Ty, Ty) : Ty; + +function Inv0_TSet(Ty) : Ty; + +axiom (forall t: Ty :: { TSet(t) } Inv0_TSet(TSet(t)) == t); + +function Inv0_TISet(Ty) : Ty; + +axiom (forall t: Ty :: { TISet(t) } Inv0_TISet(TISet(t)) == t); + +function Inv0_TSeq(Ty) : Ty; + +axiom (forall t: Ty :: { TSeq(t) } Inv0_TSeq(TSeq(t)) == t); + +function Inv0_TMultiSet(Ty) : Ty; + +axiom (forall t: Ty :: { TMultiSet(t) } Inv0_TMultiSet(TMultiSet(t)) == t); + +function Inv0_TMap(Ty) : Ty; + +function Inv1_TMap(Ty) : Ty; + +axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv0_TMap(TMap(t, u)) == t); + +axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Inv1_TMap(TMap(t, u)) == u); + +function Inv0_TIMap(Ty) : Ty; + +function Inv1_TIMap(Ty) : Ty; + +axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv0_TIMap(TIMap(t, u)) == t); + +axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Inv1_TIMap(TIMap(t, u)) == u); + +type TyTag; + +function Tag(Ty) : TyTag; + +const unique TagBool: TyTag; + +const unique TagChar: TyTag; + +const unique TagInt: TyTag; + +const unique TagNat: TyTag; + +const unique TagReal: TyTag; + +const unique TagSet: TyTag; + +const unique TagISet: TyTag; + +const unique TagMultiSet: TyTag; + +const unique TagSeq: TyTag; + +const unique TagMap: TyTag; + +const unique TagIMap: TyTag; + +const unique TagClass: TyTag; + +axiom Tag(TBool) == TagBool; + +axiom Tag(TChar) == TagChar; + +axiom Tag(TInt) == TagInt; + +axiom Tag(TNat) == TagNat; + +axiom Tag(TReal) == TagReal; + +axiom (forall t: Ty :: { TSet(t) } Tag(TSet(t)) == TagSet); + +axiom (forall t: Ty :: { TISet(t) } Tag(TISet(t)) == TagISet); + +axiom (forall t: Ty :: { TMultiSet(t) } Tag(TMultiSet(t)) == TagMultiSet); + +axiom (forall t: Ty :: { TSeq(t) } Tag(TSeq(t)) == TagSeq); + +axiom (forall t: Ty, u: Ty :: { TMap(t, u) } Tag(TMap(t, u)) == TagMap); + +axiom (forall t: Ty, u: Ty :: { TIMap(t, u) } Tag(TIMap(t, u)) == TagIMap); + +function {:identity} LitInt(x: int) : int; + +axiom (forall x: int :: {:identity} { LitInt(x): int } LitInt(x): int == x); + +axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x))); + +function {:identity} LitReal(x: real) : real; + +axiom (forall x: real :: {:identity} { LitReal(x): real } LitReal(x): real == x); + +axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x))); + +function {:identity} Lit(x: T) : T; + +axiom (forall x: T :: {:identity} { Lit(x): T } Lit(x): T == x); + +axiom (forall x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x))); + +type char; + +function char#FromInt(int) : char; + +function char#ToInt(char) : int; + +axiom (forall ch: char :: { char#ToInt(ch) } char#FromInt(char#ToInt(ch)) == ch); + +axiom (forall n: int :: + { char#FromInt(n) } + 0 <= n && n < 65536 ==> char#ToInt(char#FromInt(n)) == n); + +type ref; + +const null: ref; + +const unique NoTraitAtAll: ClassName; + +function TraitParent(ClassName) : ClassName; + +type Box; + +const $ArbitraryBoxValue: Box; + +function $Box(T) : Box; + +function $Unbox(Box) : T; + +axiom (forall x: T :: { $Box(x) } $Unbox($Box(x)) == x); + +axiom (forall bx: Box :: + { $IsBox(bx, TInt) } + $IsBox(bx, TInt) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TInt)); + +axiom (forall bx: Box :: + { $IsBox(bx, TNat) } + $IsBox(bx, TNat) ==> $Box($Unbox(bx): int) == bx && $Is($Unbox(bx): int, TNat)); + +axiom (forall bx: Box :: + { $IsBox(bx, TReal) } + $IsBox(bx, TReal) + ==> $Box($Unbox(bx): real) == bx && $Is($Unbox(bx): real, TReal)); + +axiom (forall bx: Box :: + { $IsBox(bx, TBool) } + $IsBox(bx, TBool) + ==> $Box($Unbox(bx): bool) == bx && $Is($Unbox(bx): bool, TBool)); + +axiom (forall bx: Box :: + { $IsBox(bx, TChar) } + $IsBox(bx, TChar) + ==> $Box($Unbox(bx): char) == bx && $Is($Unbox(bx): char, TChar)); + +axiom (forall bx: Box, t: Ty :: + { $IsBox(bx, TSet(t)) } + $IsBox(bx, TSet(t)) + ==> $Box($Unbox(bx): Set Box) == bx && $Is($Unbox(bx): Set Box, TSet(t))); + +axiom (forall bx: Box, t: Ty :: + { $IsBox(bx, TISet(t)) } + $IsBox(bx, TISet(t)) + ==> $Box($Unbox(bx): ISet Box) == bx && $Is($Unbox(bx): ISet Box, TISet(t))); + +axiom (forall bx: Box, t: Ty :: + { $IsBox(bx, TMultiSet(t)) } + $IsBox(bx, TMultiSet(t)) + ==> $Box($Unbox(bx): MultiSet Box) == bx + && $Is($Unbox(bx): MultiSet Box, TMultiSet(t))); + +axiom (forall bx: Box, t: Ty :: + { $IsBox(bx, TSeq(t)) } + $IsBox(bx, TSeq(t)) + ==> $Box($Unbox(bx): Seq Box) == bx && $Is($Unbox(bx): Seq Box, TSeq(t))); + +axiom (forall bx: Box, s: Ty, t: Ty :: + { $IsBox(bx, TMap(s, t)) } + $IsBox(bx, TMap(s, t)) + ==> $Box($Unbox(bx): Map Box Box) == bx && $Is($Unbox(bx): Map Box Box, TMap(s, t))); + +axiom (forall bx: Box, s: Ty, t: Ty :: + { $IsBox(bx, TIMap(s, t)) } + $IsBox(bx, TIMap(s, t)) + ==> $Box($Unbox(bx): IMap Box Box) == bx + && $Is($Unbox(bx): IMap Box Box, TIMap(s, t))); + +axiom (forall v: T, t: Ty :: + { $IsBox($Box(v), t) } + $IsBox($Box(v), t) <==> $Is(v, t)); + +axiom (forall v: T, t: Ty, h: Heap :: + { $IsAllocBox($Box(v), t, h) } + $IsAllocBox($Box(v), t, h) <==> $IsAlloc(v, t, h)); + +function $Is(T, Ty) : bool; + +function $IsAlloc(T, Ty, Heap) : bool; + +function $IsBox(T, Ty) : bool; + +function $IsAllocBox(T, Ty, Heap) : bool; + +axiom (forall v: int :: { $Is(v, TInt) } $Is(v, TInt)); + +axiom (forall v: int :: { $Is(v, TNat) } $Is(v, TNat) <==> v >= 0); + +axiom (forall v: real :: { $Is(v, TReal) } $Is(v, TReal)); + +axiom (forall v: bool :: { $Is(v, TBool) } $Is(v, TBool)); + +axiom (forall v: char :: { $Is(v, TChar) } $Is(v, TChar)); + +axiom (forall h: Heap, v: int :: { $IsAlloc(v, TInt, h) } $IsAlloc(v, TInt, h)); + +axiom (forall h: Heap, v: int :: { $IsAlloc(v, TNat, h) } $IsAlloc(v, TNat, h)); + +axiom (forall h: Heap, v: real :: { $IsAlloc(v, TReal, h) } $IsAlloc(v, TReal, h)); + +axiom (forall h: Heap, v: bool :: { $IsAlloc(v, TBool, h) } $IsAlloc(v, TBool, h)); + +axiom (forall h: Heap, v: char :: { $IsAlloc(v, TChar, h) } $IsAlloc(v, TChar, h)); + +axiom (forall v: Set Box, t0: Ty :: + { $Is(v, TSet(t0)) } + $Is(v, TSet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0))); + +axiom (forall v: ISet Box, t0: Ty :: + { $Is(v, TISet(t0)) } + $Is(v, TISet(t0)) <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsBox(bx, t0))); + +axiom (forall v: MultiSet Box, t0: Ty :: + { $Is(v, TMultiSet(t0)) } + $Is(v, TMultiSet(t0)) + <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsBox(bx, t0))); + +axiom (forall v: MultiSet Box, t0: Ty :: + { $Is(v, TMultiSet(t0)) } + $Is(v, TMultiSet(t0)) ==> $IsGoodMultiSet(v)); + +axiom (forall v: Seq Box, t0: Ty :: + { $Is(v, TSeq(t0)) } + $Is(v, TSeq(t0)) + <==> (forall i: int :: + { Seq#Index(v, i) } + 0 <= i && i < Seq#Length(v) ==> $IsBox(Seq#Index(v, i), t0))); + +axiom (forall v: Set Box, t0: Ty, h: Heap :: + { $IsAlloc(v, TSet(t0), h) } + $IsAlloc(v, TSet(t0), h) + <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h))); + +axiom (forall v: ISet Box, t0: Ty, h: Heap :: + { $IsAlloc(v, TISet(t0), h) } + $IsAlloc(v, TISet(t0), h) + <==> (forall bx: Box :: { v[bx] } v[bx] ==> $IsAllocBox(bx, t0, h))); + +axiom (forall v: MultiSet Box, t0: Ty, h: Heap :: + { $IsAlloc(v, TMultiSet(t0), h) } + $IsAlloc(v, TMultiSet(t0), h) + <==> (forall bx: Box :: { v[bx] } 0 < v[bx] ==> $IsAllocBox(bx, t0, h))); + +axiom (forall v: Seq Box, t0: Ty, h: Heap :: + { $IsAlloc(v, TSeq(t0), h) } + $IsAlloc(v, TSeq(t0), h) + <==> (forall i: int :: + { Seq#Index(v, i) } + 0 <= i && i < Seq#Length(v) ==> $IsAllocBox(Seq#Index(v, i), t0, h))); + +axiom (forall v: Map Box Box, t0: Ty, t1: Ty :: + { $Is(v, TMap(t0, t1)) } + $Is(v, TMap(t0, t1)) + <==> (forall bx: Box :: + { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } + Map#Domain(v)[bx] ==> $IsBox(Map#Elements(v)[bx], t1) && $IsBox(bx, t0))); + +axiom (forall v: Map Box Box, t0: Ty, t1: Ty, h: Heap :: + { $IsAlloc(v, TMap(t0, t1), h) } + $IsAlloc(v, TMap(t0, t1), h) + <==> (forall bx: Box :: + { Map#Elements(v)[bx] } { Map#Domain(v)[bx] } + Map#Domain(v)[bx] + ==> $IsAllocBox(Map#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h))); + +axiom (forall v: IMap Box Box, t0: Ty, t1: Ty :: + { $Is(v, TIMap(t0, t1)) } + $Is(v, TIMap(t0, t1)) + <==> (forall bx: Box :: + { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } + IMap#Domain(v)[bx] ==> $IsBox(IMap#Elements(v)[bx], t1) && $IsBox(bx, t0))); + +axiom (forall v: IMap Box Box, t0: Ty, t1: Ty, h: Heap :: + { $IsAlloc(v, TIMap(t0, t1), h) } + $IsAlloc(v, TIMap(t0, t1), h) + <==> (forall bx: Box :: + { IMap#Elements(v)[bx] } { IMap#Domain(v)[bx] } + IMap#Domain(v)[bx] + ==> $IsAllocBox(IMap#Elements(v)[bx], t1, h) && $IsAllocBox(bx, t0, h))); + +type ClassName; + +const unique class._System.int: ClassName; + +const unique class._System.bool: ClassName; + +const unique class._System.set: ClassName; + +const unique class._System.seq: ClassName; + +const unique class._System.multiset: ClassName; + +function Tclass._System.object() : Ty; + +function dtype(ref) : Ty; + +function TypeTuple(a: ClassName, b: ClassName) : ClassName; + +function TypeTupleCar(ClassName) : ClassName; + +function TypeTupleCdr(ClassName) : ClassName; + +axiom (forall a: ClassName, b: ClassName :: + { TypeTuple(a, b) } + TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b); + +type HandleType; + +function SetRef_to_SetBox(s: [ref]bool) : Set Box; + +axiom (forall s: [ref]bool, bx: Box :: + { SetRef_to_SetBox(s)[bx] } + SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]); + +axiom (forall s: [ref]bool :: + { SetRef_to_SetBox(s) } + $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object()))); + +type DatatypeType; + +type DtCtorId; + +function DatatypeCtorId(DatatypeType) : DtCtorId; + +function DtRank(DatatypeType) : int; + +function BoxRank(Box) : int; + +axiom (forall d: DatatypeType :: { BoxRank($Box(d)) } BoxRank($Box(d)) == DtRank(d)); + +const $ModuleContextHeight: int; + +const $FunctionContextHeight: int; + +type LayerType; + +const $LZ: LayerType; + +function $LS(LayerType) : LayerType; + +function AtLayer([LayerType]A, LayerType) : A; + +axiom (forall f: [LayerType]A, ly: LayerType :: + { AtLayer(f, ly) } + AtLayer(f, ly) == f[ly]); + +axiom (forall f: [LayerType]A, ly: LayerType :: + { AtLayer(f, $LS(ly)) } + AtLayer(f, $LS(ly)) == AtLayer(f, ly)); + +type Field _; + +function FDim(Field T) : int; + +function IndexField(int) : Field Box; + +axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1); + +function IndexField_Inverse(Field T) : int; + +axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i); + +function MultiIndexField(Field Box, int) : Field Box; + +axiom (forall f: Field Box, i: int :: + { MultiIndexField(f, i) } + FDim(MultiIndexField(f, i)) == FDim(f) + 1); + +function MultiIndexField_Inverse0(Field T) : Field T; + +function MultiIndexField_Inverse1(Field T) : int; + +axiom (forall f: Field Box, i: int :: + { MultiIndexField(f, i) } + MultiIndexField_Inverse0(MultiIndexField(f, i)) == f + && MultiIndexField_Inverse1(MultiIndexField(f, i)) == i); + +function DeclType(Field T) : ClassName; + +type NameFamily; + +function DeclName(Field T) : NameFamily; + +function FieldOfDecl(ClassName, NameFamily) : Field alpha; + +axiom (forall cl: ClassName, nm: NameFamily :: + { FieldOfDecl(cl, nm): Field T } + DeclType(FieldOfDecl(cl, nm): Field T) == cl + && DeclName(FieldOfDecl(cl, nm): Field T) == nm); + +function $IsGhostField(Field T) : bool; + +axiom (forall h: Heap, k: Heap, v: T, t: Ty :: + { $HeapSucc(h, k), $IsAlloc(v, t, h) } + $HeapSucc(h, k) ==> $IsAlloc(v, t, h) ==> $IsAlloc(v, t, k)); + +axiom (forall h: Heap, k: Heap, bx: Box, t: Ty :: + { $HeapSucc(h, k), $IsAllocBox(bx, t, h) } + $HeapSucc(h, k) ==> $IsAllocBox(bx, t, h) ==> $IsAllocBox(bx, t, k)); + +const unique alloc: Field bool; + +axiom FDim(alloc) == 0 && !$IsGhostField(alloc); + +function _System.array.Length(a: ref) : int; + +axiom (forall o: ref :: 0 <= _System.array.Length(o)); + +function Int(x: real) : int; + +axiom (forall x: real :: { Int(x): int } Int(x): int == int(x)); + +function Real(x: int) : real; + +axiom (forall x: int :: { Real(x): real } Real(x): real == real(x)); + +axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i); + +function {:inline true} _System.real.Trunc(x: real) : int +{ + Int(x) +} + +type Heap = [ref,Field alpha]alpha; + +function {:inline true} read(H: Heap, r: ref, f: Field alpha) : alpha +{ + H[r, f] +} + +function {:inline true} update(H: Heap, r: ref, f: Field alpha, v: alpha) : Heap +{ + H[r, f := v] +} + +function $IsGoodHeap(Heap) : bool; + +function $IsHeapAnchor(Heap) : bool; + +var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap); + +function $HeapSucc(Heap, Heap) : bool; + +axiom (forall h: Heap, r: ref, f: Field alpha, x: alpha :: + { update(h, r, f, x) } + $IsGoodHeap(update(h, r, f, x)) ==> $HeapSucc(h, update(h, r, f, x))); + +axiom (forall a: Heap, b: Heap, c: Heap :: + { $HeapSucc(a, b), $HeapSucc(b, c) } + $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c)); + +axiom (forall h: Heap, k: Heap :: + { $HeapSucc(h, k) } + $HeapSucc(h, k) + ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc))); + +function $HeapSuccGhost(Heap, Heap) : bool; + +axiom (forall h: Heap, k: Heap :: + { $HeapSuccGhost(h, k) } + $HeapSuccGhost(h, k) + ==> $HeapSucc(h, k) + && (forall o: ref, f: Field alpha :: + { read(k, o, f) } + !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f))); + +type TickType; + +var $Tick: TickType; + +procedure $YieldHavoc(this: ref, rds: Set Box, nw: Set Box); + modifies $Heap; + ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> + $o == this || rds[$Box($o)] || nw[$Box($o)] + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + ensures $HeapSucc(old($Heap), $Heap); + + + +procedure $IterHavoc0(this: ref, rds: Set Box, modi: Set Box); + modifies $Heap; + ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> + rds[$Box($o)] && !modi[$Box($o)] && $o != this + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + ensures $HeapSucc(old($Heap), $Heap); + + + +procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box); + modifies $Heap; + ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f) + || $o == this + || modi[$Box($o)] + || nw[$Box($o)]); + ensures $HeapSucc(old($Heap), $Heap); + + + +procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box)) + returns (s: Set Box); + ensures (forall bx: Box :: + { s[bx] } + s[bx] + <==> read(newHeap, this, NW)[bx] + || ( + $Unbox(bx) != null + && !read(prevHeap, $Unbox(bx): ref, alloc) + && read(newHeap, $Unbox(bx): ref, alloc))); + + + +type Set T = [T]bool; + +function Set#Card(Set T) : int; + +axiom (forall s: Set T :: { Set#Card(s) } 0 <= Set#Card(s)); + +function Set#Empty() : Set T; + +axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]); + +axiom (forall s: Set T :: + { Set#Card(s) } + (Set#Card(s) == 0 <==> s == Set#Empty()) + && (Set#Card(s) != 0 ==> (exists x: T :: s[x]))); + +function Set#Singleton(T) : Set T; + +axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]); + +axiom (forall r: T, o: T :: + { Set#Singleton(r)[o] } + Set#Singleton(r)[o] <==> r == o); + +axiom (forall r: T :: + { Set#Card(Set#Singleton(r)) } + Set#Card(Set#Singleton(r)) == 1); + +function Set#UnionOne(Set T, T) : Set T; + +axiom (forall a: Set T, x: T, o: T :: + { Set#UnionOne(a, x)[o] } + Set#UnionOne(a, x)[o] <==> o == x || a[o]); + +axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]); + +axiom (forall a: Set T, x: T, y: T :: + { Set#UnionOne(a, x), a[y] } + a[y] ==> Set#UnionOne(a, x)[y]); + +axiom (forall a: Set T, x: T :: + { Set#Card(Set#UnionOne(a, x)) } + a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a)); + +axiom (forall a: Set T, x: T :: + { Set#Card(Set#UnionOne(a, x)) } + !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1); + +function Set#Union(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Union(a, b)[o] } + Set#Union(a, b)[o] <==> a[o] || b[o]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Union(a, b), a[y] } + a[y] ==> Set#Union(a, b)[y]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Union(a, b), b[y] } + b[y] ==> Set#Union(a, b)[y]); + +axiom (forall a: Set T, b: Set T :: + { Set#Union(a, b) } + Set#Disjoint(a, b) + ==> Set#Difference(Set#Union(a, b), a) == b + && Set#Difference(Set#Union(a, b), b) == a); + +function Set#Intersection(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Intersection(a, b)[o] } + Set#Intersection(a, b)[o] <==> a[o] && b[o]); + +axiom (forall a: Set T, b: Set T :: + { Set#Union(Set#Union(a, b), b) } + Set#Union(Set#Union(a, b), b) == Set#Union(a, b)); + +axiom (forall a: Set T, b: Set T :: + { Set#Union(a, Set#Union(a, b)) } + Set#Union(a, Set#Union(a, b)) == Set#Union(a, b)); + +axiom (forall a: Set T, b: Set T :: + { Set#Intersection(Set#Intersection(a, b), b) } + Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b)); + +axiom (forall a: Set T, b: Set T :: + { Set#Intersection(a, Set#Intersection(a, b)) } + Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b)); + +axiom (forall a: Set T, b: Set T :: + { Set#Card(Set#Union(a, b)) } { Set#Card(Set#Intersection(a, b)) } + Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) + == Set#Card(a) + Set#Card(b)); + +function Set#Difference(Set T, Set T) : Set T; + +axiom (forall a: Set T, b: Set T, o: T :: + { Set#Difference(a, b)[o] } + Set#Difference(a, b)[o] <==> a[o] && !b[o]); + +axiom (forall a: Set T, b: Set T, y: T :: + { Set#Difference(a, b), b[y] } + b[y] ==> !Set#Difference(a, b)[y]); + +axiom (forall a: Set T, b: Set T :: + { Set#Card(Set#Difference(a, b)) } + Set#Card(Set#Difference(a, b)) + + Set#Card(Set#Difference(b, a)) + + Set#Card(Set#Intersection(a, b)) + == Set#Card(Set#Union(a, b)) + && Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b))); + +function Set#Subset(Set T, Set T) : bool; + +axiom (forall a: Set T, b: Set T :: + { Set#Subset(a, b) } + Set#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o])); + +function Set#Equal(Set T, Set T) : bool; + +axiom (forall a: Set T, b: Set T :: + { Set#Equal(a, b) } + Set#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o])); + +axiom (forall a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b); + +function Set#Disjoint(Set T, Set T) : bool; + +axiom (forall a: Set T, b: Set T :: + { Set#Disjoint(a, b) } + Set#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o])); + +type ISet T = [T]bool; + +function ISet#Empty() : Set T; + +axiom (forall o: T :: { ISet#Empty()[o] } !ISet#Empty()[o]); + +function ISet#UnionOne(ISet T, T) : ISet T; + +axiom (forall a: ISet T, x: T, o: T :: + { ISet#UnionOne(a, x)[o] } + ISet#UnionOne(a, x)[o] <==> o == x || a[o]); + +axiom (forall a: ISet T, x: T :: { ISet#UnionOne(a, x) } ISet#UnionOne(a, x)[x]); + +axiom (forall a: ISet T, x: T, y: T :: + { ISet#UnionOne(a, x), a[y] } + a[y] ==> ISet#UnionOne(a, x)[y]); + +function ISet#Union(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Union(a, b)[o] } + ISet#Union(a, b)[o] <==> a[o] || b[o]); + +axiom (forall a: ISet T, b: ISet T, y: T :: + { ISet#Union(a, b), a[y] } + a[y] ==> ISet#Union(a, b)[y]); + +axiom (forall a: Set T, b: Set T, y: T :: + { ISet#Union(a, b), b[y] } + b[y] ==> ISet#Union(a, b)[y]); + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Union(a, b) } + ISet#Disjoint(a, b) + ==> ISet#Difference(ISet#Union(a, b), a) == b + && ISet#Difference(ISet#Union(a, b), b) == a); + +function ISet#Intersection(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Intersection(a, b)[o] } + ISet#Intersection(a, b)[o] <==> a[o] && b[o]); + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Union(ISet#Union(a, b), b) } + ISet#Union(ISet#Union(a, b), b) == ISet#Union(a, b)); + +axiom (forall a: Set T, b: Set T :: + { ISet#Union(a, ISet#Union(a, b)) } + ISet#Union(a, ISet#Union(a, b)) == ISet#Union(a, b)); + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Intersection(ISet#Intersection(a, b), b) } + ISet#Intersection(ISet#Intersection(a, b), b) == ISet#Intersection(a, b)); + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Intersection(a, ISet#Intersection(a, b)) } + ISet#Intersection(a, ISet#Intersection(a, b)) == ISet#Intersection(a, b)); + +function ISet#Difference(ISet T, ISet T) : ISet T; + +axiom (forall a: ISet T, b: ISet T, o: T :: + { ISet#Difference(a, b)[o] } + ISet#Difference(a, b)[o] <==> a[o] && !b[o]); + +axiom (forall a: ISet T, b: ISet T, y: T :: + { ISet#Difference(a, b), b[y] } + b[y] ==> !ISet#Difference(a, b)[y]); + +function ISet#Subset(ISet T, ISet T) : bool; + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Subset(a, b) } + ISet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o])); + +function ISet#Equal(ISet T, ISet T) : bool; + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Equal(a, b) } + ISet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o])); + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Equal(a, b) } + ISet#Equal(a, b) ==> a == b); + +function ISet#Disjoint(ISet T, ISet T) : bool; + +axiom (forall a: ISet T, b: ISet T :: + { ISet#Disjoint(a, b) } + ISet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o])); + +function Math#min(a: int, b: int) : int; + +axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a); + +axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b); + +axiom (forall a: int, b: int :: + { Math#min(a, b) } + Math#min(a, b) == a || Math#min(a, b) == b); + +function Math#clip(a: int) : int; + +axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a); + +axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0); + +type MultiSet T = [T]int; + +function $IsGoodMultiSet(ms: MultiSet T) : bool; + +axiom (forall ms: MultiSet T :: + { $IsGoodMultiSet(ms) } + $IsGoodMultiSet(ms) + <==> (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms))); + +function MultiSet#Card(MultiSet T) : int; + +axiom (forall s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s)); + +axiom (forall s: MultiSet T, x: T, n: int :: + { MultiSet#Card(s[x := n]) } + 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n); + +function MultiSet#Empty() : MultiSet T; + +axiom (forall o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0); + +axiom (forall s: MultiSet T :: + { MultiSet#Card(s) } + (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) + && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < s[x]))); + +function MultiSet#Singleton(T) : MultiSet T; + +axiom (forall r: T, o: T :: + { MultiSet#Singleton(r)[o] } + (MultiSet#Singleton(r)[o] == 1 <==> r == o) + && (MultiSet#Singleton(r)[o] == 0 <==> r != o)); + +axiom (forall r: T :: + { MultiSet#Singleton(r) } + MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); + +function MultiSet#UnionOne(MultiSet T, T) : MultiSet T; + +axiom (forall a: MultiSet T, x: T, o: T :: + { MultiSet#UnionOne(a, x)[o] } + 0 < MultiSet#UnionOne(a, x)[o] <==> o == x || 0 < a[o]); + +axiom (forall a: MultiSet T, x: T :: + { MultiSet#UnionOne(a, x) } + MultiSet#UnionOne(a, x)[x] == a[x] + 1); + +axiom (forall a: MultiSet T, x: T, y: T :: + { MultiSet#UnionOne(a, x), a[y] } + 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]); + +axiom (forall a: MultiSet T, x: T, y: T :: + { MultiSet#UnionOne(a, x), a[y] } + x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]); + +axiom (forall a: MultiSet T, x: T :: + { MultiSet#Card(MultiSet#UnionOne(a, x)) } + MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1); + +function MultiSet#Union(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall a: MultiSet T, b: MultiSet T, o: T :: + { MultiSet#Union(a, b)[o] } + MultiSet#Union(a, b)[o] == a[o] + b[o]); + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Card(MultiSet#Union(a, b)) } + MultiSet#Card(MultiSet#Union(a, b)) == MultiSet#Card(a) + MultiSet#Card(b)); + +function MultiSet#Intersection(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall a: MultiSet T, b: MultiSet T, o: T :: + { MultiSet#Intersection(a, b)[o] } + MultiSet#Intersection(a, b)[o] == Math#min(a[o], b[o])); + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } + MultiSet#Intersection(MultiSet#Intersection(a, b), b) + == MultiSet#Intersection(a, b)); + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } + MultiSet#Intersection(a, MultiSet#Intersection(a, b)) + == MultiSet#Intersection(a, b)); + +function MultiSet#Difference(MultiSet T, MultiSet T) : MultiSet T; + +axiom (forall a: MultiSet T, b: MultiSet T, o: T :: + { MultiSet#Difference(a, b)[o] } + MultiSet#Difference(a, b)[o] == Math#clip(a[o] - b[o])); + +axiom (forall a: MultiSet T, b: MultiSet T, y: T :: + { MultiSet#Difference(a, b), b[y], a[y] } + a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0); + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Card(MultiSet#Difference(a, b)) } + MultiSet#Card(MultiSet#Difference(a, b)) + + MultiSet#Card(MultiSet#Difference(b, a)) + + 2 * MultiSet#Card(MultiSet#Intersection(a, b)) + == MultiSet#Card(MultiSet#Union(a, b)) + && MultiSet#Card(MultiSet#Difference(a, b)) + == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b))); + +function MultiSet#Subset(MultiSet T, MultiSet T) : bool; + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Subset(a, b) } + MultiSet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <= b[o])); + +function MultiSet#Equal(MultiSet T, MultiSet T) : bool; + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Equal(a, b) } + MultiSet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == b[o])); + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Equal(a, b) } + MultiSet#Equal(a, b) ==> a == b); + +function MultiSet#Disjoint(MultiSet T, MultiSet T) : bool; + +axiom (forall a: MultiSet T, b: MultiSet T :: + { MultiSet#Disjoint(a, b) } + MultiSet#Disjoint(a, b) + <==> (forall o: T :: { a[o] } { b[o] } a[o] == 0 || b[o] == 0)); + +function MultiSet#FromSet(Set T) : MultiSet T; + +axiom (forall s: Set T, a: T :: + { MultiSet#FromSet(s)[a] } + (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) + && (MultiSet#FromSet(s)[a] == 1 <==> s[a])); + +axiom (forall s: Set T :: + { MultiSet#Card(MultiSet#FromSet(s)) } + MultiSet#Card(MultiSet#FromSet(s)) == Set#Card(s)); + +function MultiSet#FromSeq(Seq T) : MultiSet T; + +axiom (forall s: Seq T :: + { MultiSet#FromSeq(s) } + $IsGoodMultiSet(MultiSet#FromSeq(s))); + +axiom (forall s: Seq T :: + { MultiSet#Card(MultiSet#FromSeq(s)) } + MultiSet#Card(MultiSet#FromSeq(s)) == Seq#Length(s)); + +axiom (forall s: Seq T, v: T :: + { MultiSet#FromSeq(Seq#Build(s, v)) } + MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v)); + +axiom (forall :: + MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T); + +axiom (forall a: Seq T, b: Seq T :: + { MultiSet#FromSeq(Seq#Append(a, b)) } + MultiSet#FromSeq(Seq#Append(a, b)) + == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b))); + +axiom (forall s: Seq T, i: int, v: T, x: T :: + { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } + 0 <= i && i < Seq#Length(s) + ==> MultiSet#FromSeq(Seq#Update(s, i, v))[x] + == MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s, i))), + MultiSet#Singleton(v))[x]); + +axiom (forall s: Seq T, x: T :: + { MultiSet#FromSeq(s)[x] } + (exists i: int :: + { Seq#Index(s, i) } + 0 <= i && i < Seq#Length(s) && x == Seq#Index(s, i)) + <==> 0 < MultiSet#FromSeq(s)[x]); + +type Seq _; + +function Seq#Length(Seq T) : int; + +axiom (forall s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s)); + +function Seq#Empty() : Seq T; + +axiom (forall :: Seq#Length(Seq#Empty(): Seq T) == 0); + +axiom (forall s: Seq T :: + { Seq#Length(s) } + Seq#Length(s) == 0 ==> s == Seq#Empty()); + +axiom (forall t: Ty :: { $Is(Seq#Empty(): Seq T, t) } $Is(Seq#Empty(): Seq T, t)); + +function Seq#Singleton(T) : Seq T; + +axiom (forall t: T :: + { Seq#Length(Seq#Singleton(t)) } + Seq#Length(Seq#Singleton(t)) == 1); + +function Seq#Build(s: Seq T, val: T) : Seq T; + +axiom (forall s: Seq T, v: T :: + { Seq#Length(Seq#Build(s, v)) } + Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s)); + +axiom (forall s: Seq T, i: int, v: T :: + { Seq#Index(Seq#Build(s, v), i) } + (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v) + && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i))); + +axiom (forall s: Seq Box, bx: Box, t: Ty :: + { $Is(Seq#Build(s, bx), TSeq(t)) } + $Is(s, TSeq(t)) && $IsBox(bx, t) ==> $Is(Seq#Build(s, bx), TSeq(t))); + +function Seq#Append(Seq T, Seq T) : Seq T; + +axiom (forall s0: Seq T, s1: Seq T :: + { Seq#Length(Seq#Append(s0, s1)) } + Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1)); + +axiom (forall s0: Seq Box, s1: Seq Box, t: Ty :: + { $Is(Seq#Append(s0, s1), t) } + $Is(s0, t) && $Is(s1, t) ==> $Is(Seq#Append(s0, s1), t)); + +function Seq#Index(Seq T, int) : T; + +axiom (forall t: T :: + { Seq#Index(Seq#Singleton(t), 0) } + Seq#Index(Seq#Singleton(t), 0) == t); + +axiom (forall s0: Seq T, s1: Seq T, n: int :: + { Seq#Index(Seq#Append(s0, s1), n) } + (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n)) + && (Seq#Length(s0) <= n + ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0)))); + +function Seq#Update(Seq T, int, T) : Seq T; + +axiom (forall s: Seq T, i: int, v: T :: + { Seq#Length(Seq#Update(s, i, v)) } + 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s)); + +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Index(Seq#Update(s, i, v), n) } + 0 <= n && n < Seq#Length(s) + ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v) + && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n))); + +function Seq#Contains(Seq T, T) : bool; + +axiom (forall s: Seq T, x: T :: + { Seq#Contains(s, x) } + Seq#Contains(s, x) + <==> (exists i: int :: + { Seq#Index(s, i) } + 0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); + +axiom (forall x: T :: + { Seq#Contains(Seq#Empty(), x) } + !Seq#Contains(Seq#Empty(), x)); + +axiom (forall s0: Seq T, s1: Seq T, x: T :: + { Seq#Contains(Seq#Append(s0, s1), x) } + Seq#Contains(Seq#Append(s0, s1), x) + <==> Seq#Contains(s0, x) || Seq#Contains(s1, x)); + +axiom (forall s: Seq T, v: T, x: T :: + { Seq#Contains(Seq#Build(s, v), x) } + Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x)); + +axiom (forall s: Seq T, n: int, x: T :: + { Seq#Contains(Seq#Take(s, n), x) } + Seq#Contains(Seq#Take(s, n), x) + <==> (exists i: int :: + { Seq#Index(s, i) } + 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x)); + +axiom (forall s: Seq T, n: int, x: T :: + { Seq#Contains(Seq#Drop(s, n), x) } + Seq#Contains(Seq#Drop(s, n), x) + <==> (exists i: int :: + { Seq#Index(s, i) } + 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x)); + +function Seq#Equal(Seq T, Seq T) : bool; + +axiom (forall s0: Seq T, s1: Seq T :: + { Seq#Equal(s0, s1) } + Seq#Equal(s0, s1) + <==> Seq#Length(s0) == Seq#Length(s1) + && (forall j: int :: + { Seq#Index(s0, j) } { Seq#Index(s1, j) } + 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j))); + +axiom (forall a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b); + +function Seq#SameUntil(Seq T, Seq T, int) : bool; + +axiom (forall s0: Seq T, s1: Seq T, n: int :: + { Seq#SameUntil(s0, s1, n) } + Seq#SameUntil(s0, s1, n) + <==> (forall j: int :: + { Seq#Index(s0, j) } { Seq#Index(s1, j) } + 0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j))); + +function Seq#Take(s: Seq T, howMany: int) : Seq T; + +axiom (forall s: Seq T, n: int :: + { Seq#Length(Seq#Take(s, n)) } + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n); + +axiom (forall s: Seq T, n: int, j: int :: + {:weight 25} { Seq#Index(Seq#Take(s, n), j) } { Seq#Index(s, j), Seq#Take(s, n) } + 0 <= j && j < n && j < Seq#Length(s) + ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j)); + +function Seq#Drop(s: Seq T, howMany: int) : Seq T; + +axiom (forall s: Seq T, n: int :: + { Seq#Length(Seq#Drop(s, n)) } + 0 <= n && n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n); + +axiom (forall s: Seq T, n: int, j: int :: + {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } + 0 <= n && 0 <= j && j < Seq#Length(s) - n + ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n)); + +axiom (forall s: Seq T, n: int, k: int :: + {:weight 25} { Seq#Index(s, k), Seq#Drop(s, n) } + 0 <= n && n <= k && k < Seq#Length(s) + ==> Seq#Index(Seq#Drop(s, n), k - n) == Seq#Index(s, k)); + +axiom (forall s: Seq T, t: Seq T :: + { Seq#Append(s, t) } + Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s + && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t); + +function Seq#FromArray(h: Heap, a: ref) : Seq Box; + +axiom (forall h: Heap, a: ref :: + { Seq#Length(Seq#FromArray(h, a)) } + Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); + +axiom (forall h: Heap, a: ref :: + { Seq#FromArray(h, a) } + (forall i: int :: + { read(h, a, IndexField(i)) } { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } + 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) + ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); + +axiom (forall h0: Heap, h1: Heap, a: ref :: + { Seq#FromArray(h1, a), $HeapSucc(h0, h1) } + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && $HeapSucc(h0, h1) + && (forall i: int :: + 0 <= i && i < _System.array.Length(a) + ==> read(h0, a, IndexField(i)) == read(h1, a, IndexField(i))) + ==> Seq#FromArray(h0, a) == Seq#FromArray(h1, a)); + +axiom (forall h: Heap, i: int, v: Box, a: ref :: + { Seq#FromArray(update(h, a, IndexField(i), v), a) } + 0 <= i && i < _System.array.Length(a) + ==> Seq#FromArray(update(h, a, IndexField(i), v), a) + == Seq#Update(Seq#FromArray(h, a), i, v)); + +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Take(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n <= Seq#Length(s) + ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v)); + +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Take(Seq#Update(s, i, v), n) } + n <= i && i < Seq#Length(s) + ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n)); + +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= n && n <= i && i < Seq#Length(s) + ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i - n, v)); + +axiom (forall s: Seq T, i: int, v: T, n: int :: + { Seq#Drop(Seq#Update(s, i, v), n) } + 0 <= i && i < n && n < Seq#Length(s) + ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n)); + +axiom (forall h: Heap, a: ref, n0: int, n1: int :: + { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } + n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) + ==> Seq#Take(Seq#FromArray(h, a), n1) + == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field Box))); + +axiom (forall s: Seq T, v: T, n: int :: + { Seq#Drop(Seq#Build(s, v), n) } + 0 <= n && n <= Seq#Length(s) + ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v)); + +function Seq#Rank(Seq T) : int; + +axiom (forall s: Seq Box, i: int :: + { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) } + 0 <= i && i < Seq#Length(s) + ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s)); + +axiom (forall s: Seq T, i: int :: + { Seq#Rank(Seq#Drop(s, i)) } + 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s)); + +axiom (forall s: Seq T, i: int :: + { Seq#Rank(Seq#Take(s, i)) } + 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s)); + +axiom (forall s: Seq T, i: int, j: int :: + { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) } + 0 <= i && i < j && j <= Seq#Length(s) + ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s)); + +axiom (forall s: Seq T, n: int :: + { Seq#Drop(s, n) } + n == 0 ==> Seq#Drop(s, n) == s); + +axiom (forall s: Seq T, n: int :: + { Seq#Take(s, n) } + n == 0 ==> Seq#Take(s, n) == Seq#Empty()); + +axiom (forall s: Seq T, m: int, n: int :: + { Seq#Drop(Seq#Drop(s, m), n) } + 0 <= m && 0 <= n && m + n <= Seq#Length(s) + ==> Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m + n)); + +type Map _ _; + +function Map#Domain(Map U V) : [U]bool; + +function Map#Elements(Map U V) : [U]V; + +function Map#Card(Map U V) : int; + +axiom (forall m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m)); + +function Map#Empty() : Map U V; + +axiom (forall u: U :: + { Map#Domain(Map#Empty(): Map U V)[u] } + !Map#Domain(Map#Empty(): Map U V)[u]); + +axiom (forall m: Map U V :: + { Map#Card(m) } + (Map#Card(m) == 0 <==> m == Map#Empty()) + && (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x]))); + +function Map#Glue([U]bool, [U]V, Ty) : Map U V; + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { Map#Domain(Map#Glue(a, b, t)) } + Map#Domain(Map#Glue(a, b, t)) == a); + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { Map#Elements(Map#Glue(a, b, t)) } + Map#Elements(Map#Glue(a, b, t)) == b); + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { $Is(Map#Glue(a, b, t), t) } + $Is(Map#Glue(a, b, t), t)); + +function Map#Build(Map U V, U, V) : Map U V; + +axiom (forall m: Map U V, u: U, u': U, v: V :: + { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] } + (u' == u + ==> Map#Domain(Map#Build(m, u, v))[u'] && Map#Elements(Map#Build(m, u, v))[u'] == v) + && (u' != u + ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] + && Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u'])); + +axiom (forall m: Map U V, u: U, v: V :: + { Map#Card(Map#Build(m, u, v)) } + Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m)); + +axiom (forall m: Map U V, u: U, v: V :: + { Map#Card(Map#Build(m, u, v)) } + !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1); + +function Map#Equal(Map U V, Map U V) : bool; + +axiom (forall m: Map U V, m': Map U V :: + { Map#Equal(m, m') } + Map#Equal(m, m') + <==> (forall u: U :: Map#Domain(m)[u] == Map#Domain(m')[u]) + && (forall u: U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u])); + +axiom (forall m: Map U V, m': Map U V :: + { Map#Equal(m, m') } + Map#Equal(m, m') ==> m == m'); + +function Map#Disjoint(Map U V, Map U V) : bool; + +axiom (forall m: Map U V, m': Map U V :: + { Map#Disjoint(m, m') } + Map#Disjoint(m, m') + <==> (forall o: U :: + { Map#Domain(m)[o] } { Map#Domain(m')[o] } + !Map#Domain(m)[o] || !Map#Domain(m')[o])); + +type IMap _ _; + +function IMap#Domain(IMap U V) : [U]bool; + +function IMap#Elements(IMap U V) : [U]V; + +function IMap#Empty() : IMap U V; + +axiom (forall u: U :: + { IMap#Domain(IMap#Empty(): IMap U V)[u] } + !IMap#Domain(IMap#Empty(): IMap U V)[u]); + +function IMap#Glue([U]bool, [U]V, Ty) : IMap U V; + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { IMap#Domain(IMap#Glue(a, b, t)) } + IMap#Domain(IMap#Glue(a, b, t)) == a); + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { IMap#Elements(IMap#Glue(a, b, t)) } + IMap#Elements(IMap#Glue(a, b, t)) == b); + +axiom (forall a: [U]bool, b: [U]V, t: Ty :: + { $Is(IMap#Glue(a, b, t), t) } + $Is(IMap#Glue(a, b, t), t)); + +function IMap#Build(IMap U V, U, V) : IMap U V; + +axiom (forall m: IMap U V, u: U, u': U, v: V :: + { IMap#Domain(IMap#Build(m, u, v))[u'] } + { IMap#Elements(IMap#Build(m, u, v))[u'] } + (u' == u + ==> IMap#Domain(IMap#Build(m, u, v))[u'] + && IMap#Elements(IMap#Build(m, u, v))[u'] == v) + && (u' != u + ==> IMap#Domain(IMap#Build(m, u, v))[u'] == IMap#Domain(m)[u'] + && IMap#Elements(IMap#Build(m, u, v))[u'] == IMap#Elements(m)[u'])); + +function IMap#Equal(IMap U V, IMap U V) : bool; + +axiom (forall m: IMap U V, m': IMap U V :: + { IMap#Equal(m, m') } + IMap#Equal(m, m') + <==> (forall u: U :: IMap#Domain(m)[u] == IMap#Domain(m')[u]) + && (forall u: U :: + IMap#Domain(m)[u] ==> IMap#Elements(m)[u] == IMap#Elements(m')[u])); + +axiom (forall m: IMap U V, m': IMap U V :: + { IMap#Equal(m, m') } + IMap#Equal(m, m') ==> m == m'); + +function INTERNAL_add_boogie(x: int, y: int) : int; + +axiom (forall x: int, y: int :: + { INTERNAL_add_boogie(x, y): int } + INTERNAL_add_boogie(x, y): int == x + y); + +function INTERNAL_sub_boogie(x: int, y: int) : int; + +axiom (forall x: int, y: int :: + { INTERNAL_sub_boogie(x, y): int } + INTERNAL_sub_boogie(x, y): int == x - y); + +function INTERNAL_mul_boogie(x: int, y: int) : int; + +axiom (forall x: int, y: int :: + { INTERNAL_mul_boogie(x, y): int } + INTERNAL_mul_boogie(x, y): int == x * y); + +function INTERNAL_div_boogie(x: int, y: int) : int; + +axiom (forall x: int, y: int :: + { INTERNAL_div_boogie(x, y): int } + INTERNAL_div_boogie(x, y): int == x div y); + +function INTERNAL_mod_boogie(x: int, y: int) : int; + +axiom (forall x: int, y: int :: + { INTERNAL_mod_boogie(x, y): int } + INTERNAL_mod_boogie(x, y): int == x mod y); + +function {:never_pattern true} INTERNAL_lt_boogie(x: int, y: int) : bool; + +axiom (forall x: int, y: int :: + {:never_pattern true} { INTERNAL_lt_boogie(x, y): bool } + INTERNAL_lt_boogie(x, y): bool == (x < y)); + +function {:never_pattern true} INTERNAL_le_boogie(x: int, y: int) : bool; + +axiom (forall x: int, y: int :: + {:never_pattern true} { INTERNAL_le_boogie(x, y): bool } + INTERNAL_le_boogie(x, y): bool == (x <= y)); + +function {:never_pattern true} INTERNAL_gt_boogie(x: int, y: int) : bool; + +axiom (forall x: int, y: int :: + {:never_pattern true} { INTERNAL_gt_boogie(x, y): bool } + INTERNAL_gt_boogie(x, y): bool == (x > y)); + +function {:never_pattern true} INTERNAL_ge_boogie(x: int, y: int) : bool; + +axiom (forall x: int, y: int :: + {:never_pattern true} { INTERNAL_ge_boogie(x, y): bool } + INTERNAL_ge_boogie(x, y): bool == (x >= y)); + +const unique class._System.object: ClassName; + +// Tclass._System.object Tag +axiom Tag(Tclass._System.object()) == Tagclass._System.object; + +const unique Tagclass._System.object: TyTag; + +// Box/unbox axiom for Tclass._System.object +axiom (forall bx: Box :: + { $IsBox(bx, Tclass._System.object()) } + $IsBox(bx, Tclass._System.object()) + ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.object())); + +// object: Class $Is +axiom (forall $o: ref :: + { $Is($o, Tclass._System.object()) } + $Is($o, Tclass._System.object())); + +// object: Class $IsAlloc +axiom (forall $o: ref, $h: Heap :: + { $IsAlloc($o, Tclass._System.object(), $h) } + $IsAlloc($o, Tclass._System.object(), $h) <==> $o == null || read($h, $o, alloc)); + +const unique class._System.array: ClassName; + +function Tclass._System.array(Ty) : Ty; + +// Tclass._System.array Tag +axiom (forall #$arg: Ty :: + { Tclass._System.array(#$arg) } + Tag(Tclass._System.array(#$arg)) == Tagclass._System.array); + +const unique Tagclass._System.array: TyTag; + +// Tclass._System.array injectivity 0 +axiom (forall #$arg: Ty :: + { Tclass._System.array(#$arg) } + Tclass._System.array_0(Tclass._System.array(#$arg)) == #$arg); + +function Tclass._System.array_0(Ty) : Ty; + +// Box/unbox axiom for Tclass._System.array +axiom (forall #$arg: Ty, bx: Box :: + { $IsBox(bx, Tclass._System.array(#$arg)) } + $IsBox(bx, Tclass._System.array(#$arg)) + ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._System.array(#$arg))); + +// array.: Allocation axiom +axiom (forall #$arg: Ty, $i0: int, $h: Heap, $o: ref :: + { read($h, $o, IndexField($i0)), Tclass._System.array(#$arg) } + $IsGoodHeap($h) + && $o != null + && dtype($o) == Tclass._System.array(#$arg) + && + 0 <= $i0 + && $i0 < _System.array.Length($o) + ==> $IsBox(read($h, $o, IndexField($i0)), #$arg) + && (read($h, $o, alloc) ==> $IsAllocBox(read($h, $o, IndexField($i0)), #$arg, $h))); + +// array: Class $Is +axiom (forall #$arg: Ty, $o: ref :: + { $Is($o, Tclass._System.array(#$arg)) } + $Is($o, Tclass._System.array(#$arg)) + <==> $o == null || dtype($o) == Tclass._System.array(#$arg)); + +// array: Class $IsAlloc +axiom (forall #$arg: Ty, $o: ref, $h: Heap :: + { $IsAlloc($o, Tclass._System.array(#$arg), $h) } + $IsAlloc($o, Tclass._System.array(#$arg), $h) + <==> $o == null || read($h, $o, alloc)); + +// array.Length: Allocation axiom +axiom (forall #$arg: Ty, $h: Heap, $o: ref :: + $IsGoodHeap($h) && $o != null && dtype($o) == Tclass._System.array(#$arg) + ==> $Is(_System.array.Length($o), TInt) + && (read($h, $o, alloc) ==> $IsAlloc(_System.array.Length($o), TInt, $h))); + +function Tclass._System.___hFunc0(Ty) : Ty; + +// Tclass._System.___hFunc0 Tag +axiom (forall #$T0: Ty :: + { Tclass._System.___hFunc0(#$T0) } + Tag(Tclass._System.___hFunc0(#$T0)) == Tagclass._System.___hFunc0); + +const unique Tagclass._System.___hFunc0: TyTag; + +// Tclass._System.___hFunc0 injectivity 0 +axiom (forall #$T0: Ty :: + { Tclass._System.___hFunc0(#$T0) } + Tclass._System.___hFunc0_0(Tclass._System.___hFunc0(#$T0)) == #$T0); + +function Tclass._System.___hFunc0_0(Ty) : Ty; + +// Box/unbox axiom for Tclass._System.___hFunc0 +axiom (forall #$T0: Ty, bx: Box :: + { $IsBox(bx, Tclass._System.___hFunc0(#$T0)) } + $IsBox(bx, Tclass._System.___hFunc0(#$T0)) + ==> $Box($Unbox(bx): HandleType) == bx + && $Is($Unbox(bx): HandleType, Tclass._System.___hFunc0(#$T0))); + +function Handle0([Heap]Box, [Heap]bool, [Heap]Set Box) : HandleType; + +function Apply0(Ty, HandleType, Heap) : Box; + +function Requires0(Ty, HandleType, Heap) : bool; + +function Reads0(Ty, HandleType, Heap) : Set Box; + +axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: + { Apply0(t0, Handle0(h, r, rd), heap) } + Apply0(t0, Handle0(h, r, rd), heap) == h[heap]); + +axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box :: + { Requires0(t0, Handle0(h, r, rd), heap) } + r[heap] ==> Requires0(t0, Handle0(h, r, rd), heap)); + +axiom (forall t0: Ty, heap: Heap, h: [Heap]Box, r: [Heap]bool, rd: [Heap]Set Box, bx: Box :: + { Reads0(t0, Handle0(h, r, rd), heap)[bx] } + Reads0(t0, Handle0(h, r, rd), heap)[bx] == rd[heap][bx]); + +function {:inline true} _System.___hFunc0.requires(t0: Ty, heap: Heap, f: HandleType) : bool +{ + Requires0(t0, f, heap) +} + +function {:inline true} _System.___hFunc0.requires#canCall(t0: Ty, heap: Heap, f: HandleType) : bool +{ + true +} + +function {:inline true} _System.___hFunc0.reads(t0: Ty, heap: Heap, f: HandleType) : Set Box +{ + Reads0(t0, f, heap) +} + +function {:inline true} _System.___hFunc0.reads#canCall(t0: Ty, heap: Heap, f: HandleType) : bool +{ + true +} + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Reads0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h0)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Reads0(t0, f, h0) == Reads0(t0, f, h1)); + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Reads0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h1)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Reads0(t0, f, h0) == Reads0(t0, f, h1)); + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Requires0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h0)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Requires0(t0, f, h0) == Requires0(t0, f, h1)); + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Requires0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h1)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Requires0(t0, f, h0) == Requires0(t0, f, h1)); + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Apply0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h0)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Apply0(t0, f, h0) == Apply0(t0, f, h1)); + +axiom (forall t0: Ty, h0: Heap, h1: Heap, f: HandleType :: + { $HeapSucc(h0, h1), Apply0(t0, f, h1) } + $HeapSucc(h0, h1) + && + $IsGoodHeap(h0) + && $IsGoodHeap(h1) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h0) + && (forall o: ref, fld: Field a :: + o != null + && read(h0, o, alloc) + && read(h1, o, alloc) + && Reads0(t0, f, h1)[$Box(o)] + ==> read(h0, o, fld) == read(h1, o, fld)) + ==> Apply0(t0, f, h0) == Apply0(t0, f, h1)); + +axiom (forall t0: Ty, h: Heap, f: HandleType :: + { Apply0(t0, f, h) } + $IsGoodHeap(h) + && + $Is(f, Tclass._System.___hFunc0(t0)) + && $IsAlloc(f, Tclass._System.___hFunc0(t0), h) + ==> $IsBox(Apply0(t0, f, h), t0) && $IsAllocBox(Apply0(t0, f, h), t0, h)); + +const unique class._module.__default: ClassName; + +function Tclass._module.__default() : Ty; + +// Tclass._module.__default Tag +axiom Tag(Tclass._module.__default()) == Tagclass._module.__default; + +const unique Tagclass._module.__default: TyTag; + +// Box/unbox axiom for Tclass._module.__default +axiom (forall bx: Box :: + { $IsBox(bx, Tclass._module.__default()) } + $IsBox(bx, Tclass._module.__default()) + ==> $Box($Unbox(bx): ref) == bx && $Is($Unbox(bx): ref, Tclass._module.__default())); + +// _default: Class $Is +axiom (forall $o: ref :: + { $Is($o, Tclass._module.__default()) } + $Is($o, Tclass._module.__default()) + <==> $o == null || dtype($o) == Tclass._module.__default()); + +// _default: Class $IsAlloc +axiom (forall $o: ref, $h: Heap :: + { $IsAlloc($o, Tclass._module.__default(), $h) } + $IsAlloc($o, Tclass._module.__default(), $h) + <==> $o == null || read($h, $o, alloc)); + +procedure CheckWellformed$$_module.__default.test(); + free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight; + modifies $Heap, $Tick; + + + +implementation CheckWellformed$$_module.__default.test() +{ + var $_Frame: [ref,Field beta]bool; + + // AddMethodImpl: test, CheckWellformed$$_module.__default.test + $_Frame := (lambda $o: ref, $f: Field alpha :: + $o != null && read($Heap, $o, alloc) ==> false); + assume {:captureState "Bug136.dfy(4,7): initial state"} true; + havoc $Heap; + assume (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + assume $HeapSucc(old($Heap), $Heap); +} + + + +procedure InterModuleCall$$_module.__default.test(); + modifies $Heap, $Tick; + // frame condition + free ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + // boilerplate + free ensures $HeapSucc(old($Heap), $Heap); + + + +procedure IntraModuleCall$$_module.__default.test(); + modifies $Heap, $Tick; + // frame condition + free ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + // boilerplate + free ensures $HeapSucc(old($Heap), $Heap); + + + +procedure Impl$$_module.__default.test() returns ($_reverifyPost: bool); + free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight; + modifies $Heap, $Tick; + // frame condition + free ensures (forall $o: ref, $f: Field alpha :: + { read($Heap, $o, $f) } + $o != null && read(old($Heap), $o, alloc) + ==> read($Heap, $o, $f) == read(old($Heap), $o, $f)); + // boilerplate + free ensures $HeapSucc(old($Heap), $Heap); + + + +implementation Impl$$_module.__default.test() returns ($_reverifyPost: bool) +{ + var $_Frame: [ref,Field beta]bool; + + // AddMethodImpl: test, Impl$$_module.__default.test + $_Frame := (lambda $o: ref, $f: Field alpha :: + $o != null && read($Heap, $o, alloc) ==> false); + assume {:captureState "Bug136.dfy(5,1): initial state"} true; + $_reverifyPost := false; + // ----- assume statement ----- Bug136.dfy(6,5) + assume true; + assume false; + // ----- assert statement ----- Bug136.dfy(7,5) + assume true; + assert true; +} + + + +Dafny program verifier finished with 2 verified, 0 errors -- cgit v1.2.3