Computations!

Generates 'computing' axioms for both all formals and just decreasing formals.
Supported are literal datatypes, booleans and numbers.
The axioms are given a weight of 10, which seems enough for Z3 to give up when
it is sane to do so.

7 files changed, 373 insertions, 37 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 5d0b647f..349da0fd 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -8,6 +8,12 @@ const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as
 axiom $$Language$Dafny;        // coming from a Dafny program.

 

 // ---------------------------------------------------------------

+// -- Literals ---------------------------------------------------

+// ---------------------------------------------------------------

+function {:identity} Lit<T>(x: T): T { x }

+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );

+

+// ---------------------------------------------------------------

 // -- References -------------------------------------------------

 // ---------------------------------------------------------------

 

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 1993b88d..4a48b404 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -4036,6 +4036,7 @@ namespace Microsoft.Dafny {
   public class UnaryExpr : Expression

   {

     public enum Opcode {

+      Lit,

       Not,

       SeqLength

     }

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 49173230..14e9aa24 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -489,6 +489,24 @@ namespace Microsoft.Dafny {
         q = new Bpl.ForallExpr(ctor.tok, bvs, trg, Bpl.Expr.Imp(isGoodHeap, Bpl.Expr.Iff(lhs, pt)));

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

 

+        if (dt is IndDatatypeDecl) {

+          // Add Lit axiom:

+          // axiom (forall p0, ..., pn :: #dt.ctor(Lit(p0), ..., Lit(pn)) == Lit(#dt.ctor(p0, .., pn)));

+          CreateBoundVariables(ctor.Formals, out bvs, out args);

+          List<Bpl.Expr> litargs = new List<Bpl.Expr>();

+          foreach (Bpl.Expr arg in args) {

+            litargs.Add(Lit(arg));

+          }

+          lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs);

+          Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType);

+          q = Bpl.Expr.Eq(lhs, rhs);

+          if (bvs.Count() > 0) {

+            Bpl.Trigger tr = new Bpl.Trigger(ctor.tok, true, new Bpl.ExprSeq(lhs));

+            q = new Bpl.ForallExpr(ctor.tok, bvs, tr, q);

+          }

+          sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

+        }

+

         // Add injectivity axioms:

         Contract.Assert(ctor.Formals.Count == ctor.Destructors.Count);  // even nameless destructors are included in ctor.Destructors

         i = 0;

@@ -1475,23 +1493,47 @@ namespace Microsoft.Dafny {
     }

 

     void AddFunctionAxiom(Function/*!*/ f, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {

+      var vs = new List<FunctionAxiomVisibility>();

       if (f is Predicate || f is CoPredicate) {

-        var ax = FunctionAxiom(f, FunctionAxiomVisibility.IntraModuleOnly, body, ens, specialization, layerOffset);

-        sink.TopLevelDeclarations.Add(ax);

-        ax = FunctionAxiom(f, FunctionAxiomVisibility.ForeignModuleOnly, body, ens, specialization, layerOffset);

-        sink.TopLevelDeclarations.Add(ax);

-        if (f is CoPredicate) {

-          AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);

-        }

+        vs.Add(FunctionAxiomVisibility.IntraModuleOnly);

+        vs.Add(FunctionAxiomVisibility.ForeignModuleOnly);

       } else {

-        var ax = FunctionAxiom(f, FunctionAxiomVisibility.All, body, ens, specialization, layerOffset);

+        vs.Add(FunctionAxiomVisibility.All);

+      }

+      foreach (var v in vs) {

+        var ax = FunctionAxiom(f, v, body, ens, specialization, layerOffset, null);

         sink.TopLevelDeclarations.Add(ax);

+        // TODO(namin) Is checking f.Reads.Count()==0 excluding Valid() of BinaryTree in the right way?

+        //             I don't see how this in the decreasing clause would help there.

+        if (!(f is CoPredicate) && f.Reads.Count() == 0 && layerOffset == 0) {

+          var decs = new List<Formal>();

+          foreach (var e in f.Decreases.Expressions) {

+            foreach (var se in e.SubExpressions) {

+              if (se is IdentifierExpr) {

+                var id = (IdentifierExpr)se;

+                if (id.Var is Formal) {

+                  decs.Add((Formal)id.Var);

+                }

+              }

+            }

+          }

+          Contract.Assert(decs.Count() <= f.Formals.Count());

+          if (0 < decs.Count() && decs.Count() < f.Formals.Count()) {

+            ax = FunctionAxiom(f, v, body, ens, specialization, layerOffset, decs);

+            sink.TopLevelDeclarations.Add(ax);

+          }

+          ax = FunctionAxiom(f, v, body, ens, specialization, layerOffset, f.Formals);

+          sink.TopLevelDeclarations.Add(ax);

+        }

+      }

+      if (f is CoPredicate) {

+        AddPrefixPredicateAxioms(((CoPredicate)f).PrefixPredicate);

       }

     }

 

     enum FunctionAxiomVisibility { All, IntraModuleOnly, ForeignModuleOnly }

 

-    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, FunctionAxiomVisibility visibility, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset) {

+    Bpl.Axiom/*!*/ FunctionAxiom(Function/*!*/ f, FunctionAxiomVisibility visibility, Expression body, List<Expression/*!*/>/*!*/ ens, Specialization specialization, int layerOffset, ICollection<Formal> lits) {

       Contract.Requires(f != null);

       Contract.Requires(ens != null);

       Contract.Requires(layerOffset == 0 || (layerOffset == 1 && f.IsRecursive));

@@ -1586,16 +1628,33 @@ namespace Microsoft.Dafny {
       } else {

         specializationFormals = specialization.Formals;

       }

+      var substMap = new Dictionary<IVariable, Expression>();

+      if (specialization != null)

+      {

+        substMap = specialization.SubstMap;

+      }

+

       foreach (Formal p in f.Formals) {

         int i = specializationFormals == null ? -1 : specializationFormals.FindIndex(val => val == p);

         if (i == -1) {

           bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

           formals.Add(bv);

           Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);

-          args.Add(formal);

-          // add well-typedness conjunct to antecedent

-          Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);

-          if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

+          if (lits!=null && lits.Contains(p) && !substMap.ContainsKey(p)) {

+            args.Add(Lit(formal));

+            IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

+            ie.Var = p; ie.Type = ie.Var.Type;

+            UnaryExpr l = new UnaryExpr(p.tok, UnaryExpr.Opcode.Lit, ie);

+            l.Type = ie.Var.Type;

+            substMap.Add(p, l);

+          } else {

+            args.Add(formal);

+          }

+          if (lits==null) {

+            // add well-typedness conjunct to antecedent

+            Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);

+            if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

+          }

         } else {

           args.Add(etran.TrExpr(specialization.ReplacementExprs[i]));

           // note, well-typedness conjuncts for the replacement formals has already been done above

@@ -1615,10 +1674,6 @@ namespace Microsoft.Dafny {
         visibility == FunctionAxiomVisibility.All ? Bpl.Expr.Or(activateForeign, activateIntra) :

         visibility == FunctionAxiomVisibility.IntraModuleOnly ? activateIntra : activateForeign;

 

-      var substMap = new Dictionary<IVariable, Expression>();

-      if (specialization != null) {

-        substMap = specialization.SubstMap;

-      }

       Bpl.IdentifierExpr funcID = new Bpl.IdentifierExpr(f.tok, FunctionName(f, 1+layerOffset), TrType(f.ResultType));

       Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(funcID), args);

 

@@ -1644,6 +1699,10 @@ namespace Microsoft.Dafny {
       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

       Bpl.Expr meat;

+      var etranLimited = etran.LimitedFunctions(f);

+      if (lits!=null) {

+        etranLimited = etran;

+      }

       if (body == null) {

         meat = Bpl.Expr.True;

       } else {

@@ -1656,24 +1715,31 @@ namespace Microsoft.Dafny {
           meat = Bpl.Expr.And(

             CanCallAssumption(bodyWithSubst, etran),

             visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

-              Bpl.Expr.Imp(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)) :

-              Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));

+              Bpl.Expr.Imp(funcAppl, etranLimited.TrExpr(bodyWithSubst)) :

+              Bpl.Expr.Eq(funcAppl, etranLimited.TrExpr(bodyWithSubst)));

         } else {

           meat = visibility == FunctionAxiomVisibility.ForeignModuleOnly && (f is Predicate || f is CoPredicate) ?

             Bpl.Expr.Imp(funcAppl, etran.TrExpr(bodyWithSubst)) :

             Bpl.Expr.Eq(funcAppl, etran.TrExpr(bodyWithSubst));

         }

       }

-      if (layerOffset == 0) {

+      if (layerOffset == 0 && lits==null) {

         foreach (Expression p in ens) {

-          Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));

+          Bpl.Expr q = etranLimited.TrExpr(Substitute(p, null, substMap));

           meat = BplAnd(meat, q);

         }

         Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);

         if (whr != null) { meat = Bpl.Expr.And(meat, whr); }

       }

-      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));

+      QKeyValue kv = null;

+      if (lits != null) {

+        kv = new QKeyValue(f.tok, "weight", new List<object>() { Bpl.Expr.Literal(10) }, null);

+      }

+      Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, kv, tr, Bpl.Expr.Imp(ante, meat));

       string comment = "definition axiom for " + FunctionName(f, 1+layerOffset);

+      if (lits!=null) {

+        comment += " for literals";

+      }

       if (visibility == FunctionAxiomVisibility.IntraModuleOnly) {

         comment += " (intra-module)";

       } else if (visibility == FunctionAxiomVisibility.ForeignModuleOnly) {

@@ -7155,6 +7221,8 @@ namespace Microsoft.Dafny {
         TrStmt_CheckWellformed(e.Expr, builder, locals, etran, true);

 

         Bpl.Expr bRhs = etran.TrExpr(e.Expr);

+        // TODO(namin): Once Boogie knows about Lit, this is not needed.

+        bRhs = RemoveLit(bRhs);

         CheckSubrange(tok, bRhs, checkSubrangeType, builder);

         bRhs = etran.CondApplyBox(tok, bRhs, e.Expr.Type, lhsType);

 

@@ -7735,9 +7803,9 @@ namespace Microsoft.Dafny {
           if (e.Value == null) {

             return predef.Null;

           } else if (e.Value is bool) {

-            return new Bpl.LiteralExpr(e.tok, (bool)e.Value);

+            return translator.Lit(new Bpl.LiteralExpr(e.tok, (bool)e.Value));

           } else if (e.Value is BigInteger) {

-            return Bpl.Expr.Literal(Microsoft.Basetypes.BigNum.FromBigInt((BigInteger)e.Value));

+            return translator.Lit(Bpl.Expr.Literal(Microsoft.Basetypes.BigNum.FromBigInt((BigInteger)e.Value)));

           } else {

             Contract.Assert(false); throw new cce.UnreachableException();  // unexpected literal

           }

@@ -7962,6 +8030,8 @@ namespace Microsoft.Dafny {
           UnaryExpr e = (UnaryExpr)expr;

           Bpl.Expr arg = TrExpr(e.E);

           switch (e.Op) {

+            case UnaryExpr.Opcode.Lit:

+              return translator.Lit(arg);

             case UnaryExpr.Opcode.Not:

               return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);

             case UnaryExpr.Opcode.SeqLength:

@@ -7996,14 +8066,29 @@ namespace Microsoft.Dafny {
           }

           Bpl.Expr e1 = TrExpr(e.E1);

           BinaryOperator.Opcode bOpcode;

+          Bpl.Type typ;

+          var lit0 = translator.GetLit(e0);

+          var lit1 = translator.GetLit(e1);

+          // TODO(namin): Once Boogie knows about Lit, we can keep the Lit when not lifting.

+          bool liftLit = lit0 != null && lit1 != null;

+          if (lit0 != null) {

+            e0 = lit0;

+          }

+          if (lit1 != null) {

+            e1 = lit1;

+          }

           switch (e.ResolvedOp) {

             case BinaryExpr.ResolvedOpcode.Iff:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Iff; break;

             case BinaryExpr.ResolvedOpcode.Imp:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Imp; break;

             case BinaryExpr.ResolvedOpcode.And:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.And; break;

             case BinaryExpr.ResolvedOpcode.Or:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Or; break;

 

             case BinaryExpr.ResolvedOpcode.EqCommon:

@@ -8011,6 +8096,7 @@ namespace Microsoft.Dafny {
                 var cot = e.E0.Type.AsCoDatatype;

                 return translator.FunctionCall(expr.tok, "$Eq#" + cot.FullSanitizedName, Bpl.Type.Bool, e0, e1);

               }

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Eq; break;

             case BinaryExpr.ResolvedOpcode.NeqCommon:

               if (e.E0.Type.IsCoDatatype) {

@@ -8018,25 +8104,35 @@ namespace Microsoft.Dafny {
                 var x = translator.FunctionCall(expr.tok, "$Eq#" + cot.FullSanitizedName, Bpl.Type.Bool, e0, e1);

                 return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, x);

               }

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Neq; break;

 

             case BinaryExpr.ResolvedOpcode.Lt:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Lt; break;

             case BinaryExpr.ResolvedOpcode.Le:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Le; break;

             case BinaryExpr.ResolvedOpcode.Ge:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Ge; break;

             case BinaryExpr.ResolvedOpcode.Gt:

+              typ = Bpl.Type.Bool;

               bOpcode = BinaryOperator.Opcode.Gt; break;

             case BinaryExpr.ResolvedOpcode.Add:

+              typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Add; break;

             case BinaryExpr.ResolvedOpcode.Sub:

+              typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Sub; break;

             case BinaryExpr.ResolvedOpcode.Mul:

+              typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Mul; break;

             case BinaryExpr.ResolvedOpcode.Div:

+              typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Div; break;

             case BinaryExpr.ResolvedOpcode.Mod:

+              typ = Bpl.Type.Int;

               bOpcode = BinaryOperator.Opcode.Mod; break;

 

             case BinaryExpr.ResolvedOpcode.SetEq:

@@ -8137,8 +8233,12 @@ namespace Microsoft.Dafny {
             default:

               Contract.Assert(false); throw new cce.UnreachableException();  // unexpected binary expression

           }

-          return Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

 

+          Bpl.Expr re = Bpl.Expr.Binary(expr.tok, bOpcode, e0, e1);

+          if (liftLit) {

+            re = translator.Lit(re, typ);

+          }

+          return re;

         } else if (expr is TernaryExpr) {

           var e = (TernaryExpr)expr;

           var e0 = TrExpr(e.E0);

@@ -8569,7 +8669,9 @@ namespace Microsoft.Dafny {
           List<object> parms = new List<object>();

           foreach (Attributes.Argument arg in attrs.Args) {

             if (arg.E != null) {

-              parms.Add(TrExpr(arg.E));

+              var e = TrExpr(arg.E);

+              e = translator.RemoveLit(e);

+              parms.Add(e);

             } else {

               parms.Add(cce.NonNull(arg.S));

             }

@@ -8685,6 +8787,8 @@ namespace Microsoft.Dafny {
 

     enum BuiltinFunction

     {

+      Lit,

+

       SetCard,

       SetEmpty,

       SetUnionOne,

@@ -8762,6 +8866,32 @@ namespace Microsoft.Dafny {
       GenericAlloc,

     }

 

+    Bpl.Expr Lit(Bpl.Expr expr, Bpl.Type typ) {

+      return FunctionCall(expr.tok, BuiltinFunction.Lit, typ, expr);

+    }

+

+    Bpl.Expr Lit(Bpl.Expr expr) {

+      return Lit(expr, expr.Type);

+    }

+

+    Bpl.Expr GetLit(Bpl.Expr expr) {

+      if (expr is NAryExpr) {

+        NAryExpr app = (NAryExpr)expr;

+        if (app.Fun.FunctionName == "Lit") {

+          return app.Args[0];

+        }

+      }

+      return null;

+    }

+

+    Bpl.Expr RemoveLit(Bpl.Expr expr) {

+      var e = GetLit(expr);

+      if (e == null) {

+        e = expr; 

+      }

+      return e;

+    }

+

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

     Bpl.NAryExpr FunctionCall(IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args)

     {

@@ -8771,6 +8901,11 @@ namespace Microsoft.Dafny {
       Contract.Ensures(Contract.Result<Bpl.NAryExpr>() != null);

 

       switch (f) {

+        case BuiltinFunction.Lit:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation != null);

+          return FunctionCall(tok, "Lit", typeInstantiation, args);

+

         case BuiltinFunction.SetCard:

           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index e20227e7..1d1fc2d9 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1701,37 +1701,56 @@ Execution trace:
 

 Dafny program verifier finished with 1 verified, 4 errors

 

--------------------- Superposition.dfy --------------------

+-------------------- Computations.dfy --------------------

+

+Dafny program verifier finished with 46 verified, 0 errors

+

+-------------------- ComputationsNeg.dfy --------------------

+ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure

+Execution trace:

+    (0,0): anon3_Else

+ComputationsNeg.dfy(8,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(7,17): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+ComputationsNeg.dfy(20,1): Error BP5003: A postcondition might not hold on this return path.

+ComputationsNeg.dfy(19,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 3 errors

 

+-------------------- Superposition.dfy --------------------

+
 Verifying CheckWellformed$$_0_M0.C.M ...

   [0 proof obligations]  verified

-

+
 Verifying Impl$$_0_M0.C.M ...

   [4 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_0_M0.C.P ...

   [4 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_0_M0.C.Q ...

   [3 proof obligations]  error

 Superposition.dfy(24,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(25,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-

+
 Verifying CheckWellformed$$_0_M0.C.R ...

   [3 proof obligations]  error

 Superposition.dfy(30,15): Error BP5003: A postcondition might not hold on this return path.

 Superposition.dfy(31,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon5_Else

-

+
 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

-

+
 Verifying Impl$$_1_M1.C.M ...

   [1 proof obligation]  verified

-

+
 Verifying CheckWellformed$$_1_M1.C.P ...

   [1 proof obligation]  error

 Superposition.dfy(47,15): Error BP5003: A postcondition might not hold on this return path.

@@ -1740,10 +1759,10 @@ Execution trace:
     (0,0): anon7_Else

     (0,0): anon9_Then

     (0,0): anon6

-

+
 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified

-

+
 Verifying CheckWellformed$$_1_M1.C.R ...

   [0 proof obligations]  verified

 

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
new file mode 100644
index 00000000..641b8207
--- /dev/null
+++ b/Test/dafny0/Computations.dfy
@@ -0,0 +1,152 @@
+function fact6(n: nat): nat

+{

+  fact(n+6)

+}

+

+function fact(n: nat): nat

+{

+  if (n==0) then 1 else n*fact(n-1)

+}

+ghost method compute_fact6()

+  ensures fact(6)==720;

+{

+}

+ghost method compute_fact6_plus()

+  ensures fact6(0)==720;

+{

+}

+

+datatype intlist = IntNil | IntCons(head: int, tail: intlist);

+function intsize(l: intlist): nat

+{

+  if (l.IntNil?) then 0 else 1+intsize(l.tail)

+}

+function intapp(a: intlist, b: intlist): intlist

+{

+  if (a.IntNil?) then b else IntCons(a.head, intapp(a.tail, b))

+}

+ghost method compute_intappsize()

+  ensures intsize(intapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;

+{

+}

+ghost method compute_intsize4()

+  ensures intsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;

+{

+}

+function cintsize(l: intlist): nat

+{

+  match l

+  case IntNil => 0

+  case IntCons(hd, tl) => 1+cintsize(tl)

+}

+function cintapp(a: intlist, b: intlist): intlist

+{

+  match a

+  case IntNil => b

+  case IntCons(hd, tl) => IntCons(hd, cintapp(tl, b))

+}

+ghost method compute_cintappsize()

+  ensures cintsize(cintapp(IntCons(1, IntCons(2, IntNil)), IntCons(3, IntCons(4, IntNil))))==4;

+{

+}

+ghost method compute_cintsize4()

+  ensures cintsize(IntCons(1, IntCons(2, IntCons(3, IntCons(4, IntNil))))) == 4;

+{

+}

+datatype list<A> = Nil | Cons(head: A, tail: list);

+function size(l: list): nat

+{

+  if (l.Nil?) then 0 else 1+size(l.tail)

+}

+function app(a: list, b: list): list

+{

+  if (a.Nil?) then b else Cons(a.head, app(a.tail, b))

+}

+ghost method compute_size4()

+  ensures size(Cons(1, Cons(2, Cons(3, Cons(4, Nil))))) == 4;

+{

+}

+ghost method compute_size4_cons()

+  ensures size(Cons(IntNil, Cons(IntNil, Cons(IntNil, Cons(IntNil, Nil))))) == 4;

+{

+}

+ghost method compute_appsize()

+  ensures size(app(Cons(1, Cons(2, Nil)), Cons(3, Cons(4, Nil))))==4;

+{

+}

+

+datatype exp = Plus(e1: exp, e2: exp) | Num(n: int) | Var(x: int);

+function interp(env: map<int,int>, e: exp): int

+  decreases e;

+{

+  if (e.Plus?) then interp(env, e.e1)+interp(env, e.e2)

+  else if (e.Num?) then e.n

+  else if (e.Var? && e.x in env) then env[e.x]

+  else 0

+}

+ghost method compute_interp1()

+  ensures interp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;

+{

+}

+ghost method compute_interp2(env: map<int,int>)

+  requires 0 in env && env[0]==10;

+  ensures interp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;

+{

+}

+ghost method compute_interp3(env: map<int,int>)

+  requires 0 in env && env[0]==10 && 1 !in env;

+  ensures interp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;

+{

+}

+function cinterp(env: map<int,int>, e: exp): int

+  decreases e;

+{

+  match e

+  case Plus(e1, e2) => cinterp(env, e1)+cinterp(env, e2)

+  case Num(n) => n

+  case Var(x) => if x in env then env[x] else 0

+}

+ghost method compute_cinterp1()

+  ensures cinterp(map[], Plus(Plus(Num(1), Num(2)), Plus(Num(3), Num(4))))==10;

+{

+}

+ghost method compute_cinterp2(env: map<int,int>)

+  requires 0 in env && env[0]==10;

+  ensures cinterp(env, Plus(Plus(Var(0), Num(1)), Num(0)))==11;

+{

+}

+ghost method compute_cinterp3(env: map<int,int>)

+  requires 0 in env && env[0]==10 && 1 !in env;

+  ensures cinterp(env, Plus(Var(0), Plus(Var(1), Var(0))))==20;

+{

+}

+

+function opt(e: exp): exp

+{

+  match e

+  case Num(n) => e

+  case Var(x) => e

+  case Plus(e1, e2) =>

+    var o1 := opt(e1);

+    if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)

+}

+ghost method opt_test()

+  ensures opt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);

+{

+}

+function copt(e: exp): exp

+{

+  match e

+  case Num(n) => e

+  case Var(x) => e

+  case Plus(e1, e2) => match e1

+    case Num(n) => if n==0 then e2 else e

+    case Var(x) => e

+    case Plus(e11, e12) =>

+      var o1 := copt(e1);

+      if (o1.Num? && o1.n==0) then e2 else Plus(o1, e2)

+}

+ghost method copt_test()

+  ensures copt(Plus(Plus(Plus(Num(0), Num(0)), Num(0)), Num(1)))==Num(1);

+{

+}

diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
new file mode 100644
index 00000000..72e249d8
--- /dev/null
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -0,0 +1,22 @@
+function bad(n: nat): nat

+  decreases n;

+{

+  bad(n+1)

+}

+ghost method go_bad()

+  ensures bad(0)==0;

+{

+}

+

+datatype Nat = Zero | Succ(tail: Nat)

+predicate ThProperty(step: nat, t: Nat, r: nat)

+{

+  match t

+  case Zero => true

+  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)

+}

+ghost method test_ThProperty()

+  ensures ThProperty(10, Succ(Zero), 0);

+{

+//  assert ThProperty(9, Zero, 0);

+}
\ No newline at end of file
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c238b1f4..18f34345 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -26,7 +26,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
             Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy

             RefinementModificationChecking.dfy TailCalls.dfy

             Calculations.dfy IteratorResolution.dfy Iterators.dfy

-            RankPos.dfy RankNeg.dfy) do (

+            RankPos.dfy RankNeg.dfy

+            Computations.dfy ComputationsNeg.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f