From e360598b592c207b2372ba450e90288f834c9317 Mon Sep 17 00:00:00 2001 From: Nadia Polikarpova Date: Wed, 20 Mar 2013 14:37:12 +0100 Subject: Added multiset indexing. --- Source/Dafny/Resolver.cs | 7 +++++++ Source/Dafny/Translator.cs | 9 ++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a8e3d5fa..52b666a3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3350,6 +3350,13 @@ namespace Microsoft.Dafny if (!UnifyTypes(iProxy.Domain, ((MapType)t).Domain)) { return false; } + } else if (t is MultiSetType) { + if (!UnifyTypes(iProxy.Arg, Type.Int)) { + return false; + } + if (!UnifyTypes(iProxy.Domain, ((MultiSetType)t).Arg)) { + return false; + } } else { return false; } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 257cdf3b..31faea2d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2968,6 +2968,8 @@ namespace Microsoft.Dafny { Bpl.Expr inDomain = FunctionCall(expr.tok, BuiltinFunction.MapDomain, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); inDomain = Bpl.Expr.Select(inDomain, etran.BoxIfNecessary(e.tok, e0, e.E0.Type)); builder.Add(Assert(expr.tok, inDomain, "element may not be in domain", options.AssertKv)); + } else if (e.Seq.Type is MultiSetType) { + // cool } else { if (e.E0 != null) { @@ -7514,6 +7516,9 @@ namespace Microsoft.Dafny { } else if (e.Seq.Type is MapType) { domainType = ((MapType)e.Seq.Type).Domain; elmtType = ((MapType)e.Seq.Type).Range; + } else if (e.Seq.Type is MultiSetType) { + domainType = ((MultiSetType)e.Seq.Type).Arg; + elmtType = Type.Int; } else { Contract.Assert(false); } Bpl.Type elType = translator.TrType(elmtType); Bpl.Type dType = translator.TrType(domainType); @@ -7530,8 +7535,10 @@ namespace Microsoft.Dafny { } else if (e.Seq.Type is MapType) { x = translator.FunctionCall(expr.tok, BuiltinFunction.MapElements, predef.MapType(e.tok, predef.BoxType, predef.BoxType), seq); x = Bpl.Expr.Select(x, BoxIfNecessary(e.tok, e0, domainType)); + } else if (e.Seq.Type is MultiSetType) { + x = Bpl.Expr.SelectTok(expr.tok, TrExpr(e.Seq), BoxIfNecessary(expr.tok, e0, domainType)); } else { Contract.Assert(false); x = null; } - if (!ModeledAsBoxType(elmtType)) { + if (!ModeledAsBoxType(elmtType) && !(e.Seq.Type is MultiSetType)) { x = translator.FunctionCall(expr.tok, BuiltinFunction.Unbox, elType, x); } return x; -- cgit v1.2.3 From d072e064a960b4e01dfe66ef769f8d4d5fdefa41 Mon Sep 17 00:00:00 2001 From: Nadia Polikarpova Date: Wed, 20 Mar 2013 15:21:31 +0100 Subject: Added multiset update. --- Source/Dafny/Resolver.cs | 11 +++++++++++ Source/Dafny/Translator.cs | 19 +++++++++++++++---- Test/dafny0/Answer | 7 ++++++- Test/dafny0/MultiSets.dfy | 15 ++++++++++++++- 4 files changed, 46 insertions(+), 6 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 52b666a3..447ca994 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -5130,6 +5130,17 @@ namespace Microsoft.Dafny Error(e.Value, "map update requires the value to have the range type {0} (got {1})", rangeType, e.Value.Type); } expr.Type = e.Seq.Type; + } else if (UnifyTypes(e.Seq.Type, new MultiSetType(elementType))) { + ResolveExpression(e.Index, twoState, codeContext); + if (!UnifyTypes(e.Index.Type, elementType)) { + Error(e.Index, "multiset update requires domain element to be of type {0} (got {1})", elementType, e.Index.Type); + } + ResolveExpression(e.Value, twoState, codeContext); + if (!UnifyTypes(e.Value.Type, Type.Int)) { + Error(e.Value, "multiset update requires integer value (got {0})", e.Value.Type); + } + expr.Type = e.Seq.Type; + } else { Error(expr, "update requires a sequence or map (got {0})", e.Seq.Type); } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 31faea2d..ffcf40cf 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3021,12 +3021,16 @@ namespace Microsoft.Dafny { CheckWellformed(e.Seq, options, locals, builder, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); Bpl.Expr index = etran.TrExpr(e.Index); + Bpl.Expr value = etran.TrExpr(e.Value); CheckWellformed(e.Index, options, locals, builder, etran); if (e.Seq.Type is SeqType) { builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv)); + } else if (e.Seq.Type is MapType) { + // updates to maps are always valid if the values are well formed + } else if (e.Seq.Type is MultiSetType) { + builder.Add(Assert(expr.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), value), "new number of occurrences might be negative", options.AssertKv)); } else { - Contract.Assert(e.Seq.Type is MapType); - // updates add to maps, so are always valid if the values are well formed. + Contract.Assert(false); } CheckWellformed(e.Value, options, locals, builder, etran); } else if (expr is FunctionCallExpr) { @@ -7564,13 +7568,20 @@ namespace Microsoft.Dafny { Bpl.Expr index = TrExpr(e.Index); Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), elmtType); return translator.FunctionCall(expr.tok, BuiltinFunction.SeqUpdate, predef.BoxType, seq, index, val); - } else { - Contract.Assert(e.Seq.Type is MapType); + } else if (e.Seq.Type is MapType) { MapType mt = (MapType)e.Seq.Type; Bpl.Type maptype = predef.MapType(expr.tok, predef.BoxType, predef.BoxType); Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), mt.Domain); Bpl.Expr val = BoxIfNecessary(expr.tok, TrExpr(e.Value), mt.Range); return translator.FunctionCall(expr.tok, "Map#Build", maptype, seq, index, val); + } else if (e.Seq.Type is MultiSetType) { + Type elmtType = cce.NonNull((MultiSetType)e.Seq.Type).Arg; + Bpl.Expr index = BoxIfNecessary(expr.tok, TrExpr(e.Index), elmtType); + Bpl.Expr val = TrExpr(e.Value); + return Bpl.Expr.StoreTok(expr.tok, seq, index, val); + } else { + Contract.Assert(false); + throw new cce.UnreachableException(); } } else if (expr is MultiSelectExpr) { MultiSelectExpr e = (MultiSelectExpr)expr; diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 2e1bd93c..72c142ac 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1689,8 +1689,13 @@ MultiSets.dfy(163,3): Error BP5003: A postcondition might not hold on this retur MultiSets.dfy(162,15): Related location: This is the postcondition that might not hold. Execution trace: (0,0): anon0 +MultiSets.dfy(176,11): Error: new number of occurrences might be negative +Execution trace: + (0,0): anon0 + (0,0): anon4_Then + (0,0): anon3 -Dafny program verifier finished with 38 verified, 2 errors +Dafny program verifier finished with 39 verified, 3 errors -------------------- PredExpr.dfy -------------------- PredExpr.dfy(4,12): Error: condition in assert expression might not hold diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 22b93442..a3a28222 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -161,5 +161,18 @@ class BoxTests { requires forall x :: x in a ==> x in b; ensures a <= b; // error: this property does not hold for multisets { - } + } } + +// ---------- indexing and updates ---------- +method test12(a: nat, b: nat, c: int) +{ + var m0, m1, m2: multiset; + m0 := multiset{false, true, true}; + m1 := multiset{true}[false := a]; + m2 := multiset{}[false := b]; + assert (m0 + m1 + m2)[true] == 3; + assert (m1 * m2)[false] == if a <= b then a else b; + m2 := m2[true := c]; // error: c might be negative +} + -- cgit v1.2.3