summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl6
-rw-r--r--Source/Dafny/DafnyAst.cs1
-rw-r--r--Source/Dafny/Translator.cs187
-rw-r--r--Test/dafny0/Answer39
-rw-r--r--Test/dafny0/Computations.dfy152
-rw-r--r--Test/dafny0/ComputationsNeg.dfy22
-rw-r--r--Test/dafny0/runtest.bat3
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 46ae0706..b7ba8a72 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 35be1f25..4b4b6aa3 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -496,6 +496,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;
@@ -1486,23 +1504,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));
@@ -1597,16 +1639,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
@@ -1626,10 +1685,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);
@@ -1655,6 +1710,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 {
@@ -1667,24 +1726,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) {
@@ -7187,6 +7253,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);
@@ -7820,9 +7888,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
}
@@ -8063,6 +8131,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:
@@ -8097,14 +8167,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:
@@ -8112,6 +8197,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) {
@@ -8119,25 +8205,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:
@@ -8238,8 +8334,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);
@@ -8667,7 +8767,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));
}
@@ -8783,6 +8885,8 @@ namespace Microsoft.Dafny {
enum BuiltinFunction
{
+ Lit,
+
SetCard,
SetEmpty,
SetUnionOne,
@@ -8860,6 +8964,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)
{
@@ -8869,6 +8999,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 085ef78a..8f138bcd 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 11:14:59 +0000