diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-03-20 15:21:31 +0100 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-03-20 15:21:31 +0100 |
| commit | d072e064a960b4e01dfe66ef769f8d4d5fdefa41 (patch) | |
| tree | 3d76eb63bb5c180161b505341a6da269edc2ae59 /Test | |
| parent | e360598b592c207b2372ba450e90288f834c9317 (diff) | |
Added multiset update.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 7 | ||||
| -rw-r--r-- | Test/dafny0/MultiSets.dfy | 15 |
2 files changed, 20 insertions, 2 deletions
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<G> { 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<bool>;
+ 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
+}
+
|