From 24939510897bdab39243e7293530417f71b8cec2 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Mon, 6 Feb 2023 20:11:24 +0000 Subject: [PATCH 01/41] Unique minimum proof --- src/Relations.dfy | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/src/Relations.dfy b/src/Relations.dfy index ac25532f..e7c6156d 100644 --- a/src/Relations.dfy +++ b/src/Relations.dfy @@ -55,4 +55,39 @@ module {:options "-functionSyntax:4"} Relations { requires TotalOrdering(lessThan) ensures SortedBy([x] + s, lessThan) {} + + /* An element in an ordered set is called minimal, if it is less than every element of the set. */ + ghost predicate IsMinimum(R: (T, T) -> bool, m: T, s: set) + { + m in s && forall y: T | y in s :: R(m, y) + } + + /* Any totally ordered set contains a unique minimal element. */ + lemma LemmaUniqueMinimum(R: (T, T) -> bool, s: set) + requires &&|s| > 0 + && TotalOrdering(R) + ensures && (exists m: T :: IsMinimum(R, m, s)) + && (forall m, n: T :: IsMinimum(R, m, s) && IsMinimum(R, n, s) ==> m == n) + { + var x :| x in s; + if s == {x} { + assert IsMinimum(R, x, s); + } else { + var s' := s - {x}; + LemmaUniqueMinimum(R, s'); + var z :| IsMinimum(R, z, s'); + if + case R(z, x) => { + forall y: T | y in s ensures R(z, y) { + } + assert IsMinimum(R, z, s); + } + case R(x, z) => { + forall y: T | y in s ensures R(x, y) { + } + assert IsMinimum(R, x, s); + } + assert exists m: T :: IsMinimum(R, m, s); + } + } } \ No newline at end of file From 4f8a020881874b16094fd10fd820188c1e2b70e9 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 16:09:44 +0000 Subject: [PATCH 02/41] skeleton --- examples/MutableMap/MutableMapExamples.dfy | 15 ++++++++ src/MutableMap/MutableMap.dfy | 40 ++++++++++++++++++++++ src/MutableMap/MutableMap.java | 4 +++ src/MutableMap/README.md | 21 ++++++++++++ 4 files changed, 80 insertions(+) create mode 100644 examples/MutableMap/MutableMapExamples.dfy create mode 100644 src/MutableMap/MutableMap.dfy create mode 100644 src/MutableMap/MutableMap.java create mode 100644 src/MutableMap/README.md diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy new file mode 100644 index 00000000..91863c33 --- /dev/null +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -0,0 +1,15 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +include "../../src/MutableMap/MutableMap.dfy" + +module MutableMapExamples { + import MutableMap + + method Main() { + } +} diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy new file mode 100644 index 00000000..c53c9fd7 --- /dev/null +++ b/src/MutableMap/MutableMap.dfy @@ -0,0 +1,40 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +module {:options "/functionSyntax:4"} MutableMap { + class MutableMap { + function {:extern} content(): map + + constructor {:extern} () + ensures this.content() == map[] + + method {:extern} Add(k: K, v: V) + modifies this + ensures k in content().Keys && v in content().Values + + function {:extern} Keys(): (keys: set) + reads this + ensures keys == content().Keys + + function {:extern} Values(): (values: set) + reads this + ensures values == content().Values + + function {:extern} Find(k: K): (v: V) + reads this + requires k in this.Keys() + ensures v in content().Values + + method {:extern} Remove(k: K) + modifies this + ensures this.content().Keys == old(this.content)().Keys - {k} + + function {:extern} Size(): (size: int) + reads this + ensures size == |content().Values| + } +} \ No newline at end of file diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java new file mode 100644 index 00000000..86b3227a --- /dev/null +++ b/src/MutableMap/MutableMap.java @@ -0,0 +1,4 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md new file mode 100644 index 00000000..fea702d0 --- /dev/null +++ b/src/MutableMap/README.md @@ -0,0 +1,21 @@ +# Mutable Map + +The `MutableMap` module introduces mutable maps for Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages. + +To use `MutableMap` in your code, you must: + +1. `include` and `import` the `MutableMap` module as you would any other library module +2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program + +For example, to run a `Program.dfy` file that depends on the `MutableMap` module, run the following. +(This assumes you have the `libraries` repository checked out within the working directory.) + +```bash +# Java +$ dafny run Program.dfy --target:java --include libraries/src/MutableMap/MutableMap.java +``` + +(If you aren't using `dafny run` to run your program, +then you should instead integrate the appropriate language-specific implementation file in your build system.) + +The `examples/MutableMap` directory contains more detailed examples of how to use the `MutableMap` module. \ No newline at end of file From c7ecbcf20a0215923ed61d2b4686ee318a8d784d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 16:09:44 +0000 Subject: [PATCH 03/41] skeleton --- examples/MutableMap/MutableMapExamples.dfy | 15 ++++++++ src/MutableMap/MutableMap.dfy | 40 ++++++++++++++++++++++ src/MutableMap/MutableMap.java | 4 +++ src/MutableMap/README.md | 21 ++++++++++++ 4 files changed, 80 insertions(+) create mode 100644 examples/MutableMap/MutableMapExamples.dfy create mode 100644 src/MutableMap/MutableMap.dfy create mode 100644 src/MutableMap/MutableMap.java create mode 100644 src/MutableMap/README.md diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy new file mode 100644 index 00000000..91863c33 --- /dev/null +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -0,0 +1,15 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +include "../../src/MutableMap/MutableMap.dfy" + +module MutableMapExamples { + import MutableMap + + method Main() { + } +} diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy new file mode 100644 index 00000000..c53c9fd7 --- /dev/null +++ b/src/MutableMap/MutableMap.dfy @@ -0,0 +1,40 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +module {:options "/functionSyntax:4"} MutableMap { + class MutableMap { + function {:extern} content(): map + + constructor {:extern} () + ensures this.content() == map[] + + method {:extern} Add(k: K, v: V) + modifies this + ensures k in content().Keys && v in content().Values + + function {:extern} Keys(): (keys: set) + reads this + ensures keys == content().Keys + + function {:extern} Values(): (values: set) + reads this + ensures values == content().Values + + function {:extern} Find(k: K): (v: V) + reads this + requires k in this.Keys() + ensures v in content().Values + + method {:extern} Remove(k: K) + modifies this + ensures this.content().Keys == old(this.content)().Keys - {k} + + function {:extern} Size(): (size: int) + reads this + ensures size == |content().Values| + } +} \ No newline at end of file diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java new file mode 100644 index 00000000..86b3227a --- /dev/null +++ b/src/MutableMap/MutableMap.java @@ -0,0 +1,4 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md new file mode 100644 index 00000000..fea702d0 --- /dev/null +++ b/src/MutableMap/README.md @@ -0,0 +1,21 @@ +# Mutable Map + +The `MutableMap` module introduces mutable maps for Dafny. At the moment, the API is intentionally limited in scope, and only supports compilation to Java. For the future, we plan to extend both the functionality and the range of supported languages. + +To use `MutableMap` in your code, you must: + +1. `include` and `import` the `MutableMap` module as you would any other library module +2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program + +For example, to run a `Program.dfy` file that depends on the `MutableMap` module, run the following. +(This assumes you have the `libraries` repository checked out within the working directory.) + +```bash +# Java +$ dafny run Program.dfy --target:java --include libraries/src/MutableMap/MutableMap.java +``` + +(If you aren't using `dafny run` to run your program, +then you should instead integrate the appropriate language-specific implementation file in your build system.) + +The `examples/MutableMap` directory contains more detailed examples of how to use the `MutableMap` module. \ No newline at end of file From deaf459e2a880f0669b41e46355fb5888cfbf0ca Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 16:23:28 +0000 Subject: [PATCH 04/41] remove relations --- src/Relations.dfy | 38 +------------------------------------- 1 file changed, 1 insertion(+), 37 deletions(-) diff --git a/src/Relations.dfy b/src/Relations.dfy index aa37a25d..dc1ba7cb 100644 --- a/src/Relations.dfy +++ b/src/Relations.dfy @@ -75,40 +75,4 @@ module {:options "-functionSyntax:4"} Relations { requires |s| == 0 || lessThan(x, s[0]) requires TotalOrdering(lessThan) ensures SortedBy([x] + s, lessThan) - {} - - /* An element in an ordered set is called minimal, if it is less than every element of the set. */ - ghost predicate IsMinimum(R: (T, T) -> bool, m: T, s: set) - { - m in s && forall y: T | y in s :: R(m, y) - } - - /* Any totally ordered set contains a unique minimal element. */ - lemma LemmaUniqueMinimum(R: (T, T) -> bool, s: set) - requires &&|s| > 0 - && TotalOrdering(R) - ensures && (exists m: T :: IsMinimum(R, m, s)) - && (forall m, n: T :: IsMinimum(R, m, s) && IsMinimum(R, n, s) ==> m == n) - { - var x :| x in s; - if s == {x} { - assert IsMinimum(R, x, s); - } else { - var s' := s - {x}; - LemmaUniqueMinimum(R, s'); - var z :| IsMinimum(R, z, s'); - if - case R(z, x) => { - forall y: T | y in s ensures R(z, y) { - } - assert IsMinimum(R, z, s); - } - case R(x, z) => { - forall y: T | y in s ensures R(x, y) { - } - assert IsMinimum(R, x, s); - } - assert exists m: T :: IsMinimum(R, m, s); - } - } -} \ No newline at end of file + {} \ No newline at end of file From 0e0b34bafdad54adfb08d92c86f5bd15eb76aa36 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 16:24:36 +0000 Subject: [PATCH 05/41] relations --- src/Relations.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Relations.dfy b/src/Relations.dfy index dc1ba7cb..edcbc75f 100644 --- a/src/Relations.dfy +++ b/src/Relations.dfy @@ -75,4 +75,5 @@ module {:options "-functionSyntax:4"} Relations { requires |s| == 0 || lessThan(x, s[0]) requires TotalOrdering(lessThan) ensures SortedBy([x] + s, lessThan) - {} \ No newline at end of file + {} +} \ No newline at end of file From 3c9d9eb50e315de1332d7c20f29e3c756f1e6623 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 16:28:18 +0000 Subject: [PATCH 06/41] relations --- src/Relations.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relations.dfy b/src/Relations.dfy index edcbc75f..a64635a3 100644 --- a/src/Relations.dfy +++ b/src/Relations.dfy @@ -75,5 +75,5 @@ module {:options "-functionSyntax:4"} Relations { requires |s| == 0 || lessThan(x, s[0]) requires TotalOrdering(lessThan) ensures SortedBy([x] + s, lessThan) - {} + {} } \ No newline at end of file From 765167ebc3c2b767fce83ec02a34aa4c38c3eec0 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 15 Feb 2023 19:17:26 +0000 Subject: [PATCH 07/41] feasability --- examples/MutableMap/MutableMapExamples.dfy | 17 ++- src/MutableMap/MutableMap.dfy | 143 ++++++++++++++++----- 2 files changed, 127 insertions(+), 33 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 91863c33..e42c25c4 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -8,8 +8,21 @@ include "../../src/MutableMap/MutableMap.dfy" module MutableMapExamples { - import MutableMap + import opened MutableMap method Main() { + var m := new MutableMap(); + assert m.Size() == 0; + assert "testkey" !in m.Keys(); + m.Put("testkey", "testvalue"); + //assert m.Size() == 1; + assert "testkey" in m.Keys(); + assert "testvalue" in m.Values(); + assert m.Find("testkey") == "testvalue"; + m.Remove("testkey"); + assert "testkey" !in m.Keys(); + m.Put("testkey", "testvalue"); + assert "testkey" in m.Keys(); + //assert m.Size() == 1; } -} +} \ No newline at end of file diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index c53c9fd7..66033044 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,36 +5,117 @@ // RUN: %dafny /compile:0 "%s" -module {:options "/functionSyntax:4"} MutableMap { - class MutableMap { - function {:extern} content(): map - - constructor {:extern} () - ensures this.content() == map[] - - method {:extern} Add(k: K, v: V) - modifies this - ensures k in content().Keys && v in content().Values - - function {:extern} Keys(): (keys: set) - reads this - ensures keys == content().Keys - - function {:extern} Values(): (values: set) - reads this - ensures values == content().Values - - function {:extern} Find(k: K): (v: V) - reads this - requires k in this.Keys() - ensures v in content().Values - - method {:extern} Remove(k: K) - modifies this - ensures this.content().Keys == old(this.content)().Keys - {k} - - function {:extern} Size(): (size: int) - reads this - ensures size == |content().Values| +module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { + class {:extern} MutableMap { + function {:extern} content(): map + reads this + + constructor {:extern} () + ensures this.content() == map[] + ensures |this.content()| == 0 + + method {:extern} Put(k: K, v: V) + modifies this + ensures k in this.content().Keys + ensures v in this.content().Values + ensures this.content()[k] == v + ensures + if k !in old(this.content)() then + |this.content()| == |old(this.content)()| + 1 + else + |this.content()| == |old(this.content)()| + + function {:extern} Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + + function {:extern} Values(): (values: set) + reads this + ensures values == this.content().Values + + function {:extern} Find(k: K): (v: V) + reads this + requires k in this.Keys() + ensures v in this.content().Values + ensures this.content()[k] == v + + method {:extern} Remove(k: K) + modifies this + ensures this.content().Keys == old(this.content)().Keys - {k} + ensures + if k in old(this.content)() then + && |this.content()| == |old(this.content)()| - 1 + && this.content().Values == old(this.content)().Values - { old(this.content)()[k] } + else + |this.content()| == |old(this.content)()| + + function {:extern} Size(): (size: int) + reads this + ensures size == |this.content()| + } +} + +module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { + class MutableMap ... { + var m: map + + function content(): map { + m + } + + constructor () + { + m := map[]; + } + + method Put(k: K, v: V) + { + m := m[k := v]; } + + function Keys(): (keys: set) + { + m.Keys + } + + function Values(): (values: set) + { + m.Values + } + + function Find(k: K): (v: V) + { + m[k] + } + + method Remove(k: K) + { + m := (map k' | k' in m && k' != k :: m[k']); + } + + function Size(): (size: int) + { + |m| + } + } +} + +module Program { + import opened MutableMapFeasability + + method Main() { + var m := new MutableMap(); + assert m.Size() == 0; + assert "testkey" !in m.Keys(); + m.Put("testkey", "testvalue"); + //assert m.Size() == 1; + assert "testkey" in m.Keys(); + assert "testvalue" in m.Values(); + assert m.Find("testkey") == "testvalue"; + m.Remove("testkey"); + assert "testkey" !in m.Keys(); + m.Put("testkey", "testvalue"); + assert "testkey" in m.Keys(); + //assert m.Size() == 1; + } } \ No newline at end of file From fd046b4274d21775f8bd7b5305923d88f8e0ad4f Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 02:22:53 +0000 Subject: [PATCH 08/41] java --- examples/MutableMap/MutableMapExamples.dfy | 29 +++++++++---- src/MutableMap/MutableMap.dfy | 50 +++++----------------- src/MutableMap/MutableMap.java | 35 +++++++++++++++ 3 files changed, 67 insertions(+), 47 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index e42c25c4..b6851138 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -12,17 +12,30 @@ module MutableMapExamples { method Main() { var m := new MutableMap(); + assert m.Keys() == {}; + assert m.Values() == {}; + assert m.Items() == {}; assert m.Size() == 0; - assert "testkey" !in m.Keys(); m.Put("testkey", "testvalue"); - //assert m.Size() == 1; - assert "testkey" in m.Keys(); - assert "testvalue" in m.Values(); assert m.Find("testkey") == "testvalue"; - m.Remove("testkey"); - assert "testkey" !in m.Keys(); - m.Put("testkey", "testvalue"); + assert m.Keys() == {"testkey"}; + assert m.Values() == {"testvalue"}; + assert m.Items() == {("testkey", "testvalue")}; + assert m.Size() == 1; + m.Put("testkey", "testvalue2"); + assert m.Keys() == {"testkey"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey", "testvalue2")}; + m.Put("testkey2", "testvalue2"); + assert m.Keys() == {"testkey", "testkey2"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}; + assert m.Size() == 2; assert "testkey" in m.Keys(); - //assert m.Size() == 1; + assert "testkey2" in m.Keys(); + m.Remove("testkey"); + /* assert m.Keys() == {"testkey2"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey2", "testvalue2")}; */ } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 66033044..96613b44 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -12,18 +12,10 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { constructor {:extern} () ensures this.content() == map[] - ensures |this.content()| == 0 method {:extern} Put(k: K, v: V) - modifies this - ensures k in this.content().Keys - ensures v in this.content().Values - ensures this.content()[k] == v - ensures - if k !in old(this.content)() then - |this.content()| == |old(this.content)()| + 1 - else - |this.content()| == |old(this.content)()| + modifies this + ensures this.content() == old(this.content())[k := v] function {:extern} Keys(): (keys: set) reads this @@ -33,6 +25,11 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { reads this ensures values == this.content().Values + function {:extern} Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + function {:extern} Find(k: K): (v: V) reads this requires k in this.Keys() @@ -41,17 +38,12 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { method {:extern} Remove(k: K) modifies this - ensures this.content().Keys == old(this.content)().Keys - {k} - ensures - if k in old(this.content)() then - && |this.content()| == |old(this.content)()| - 1 - && this.content().Values == old(this.content)().Values - { old(this.content)()[k] } - else - |this.content()| == |old(this.content)()| + ensures forall k' :: k' in old(this.content)().Keys && k' != k ==> k' in this.content().Keys && old(this.content)()[k'] == this.content()[k'] + ensures forall k' :: k' in this.content().Keys ==> k' in old(this.content)().Keys && k' != k function {:extern} Size(): (size: int) reads this - ensures size == |this.content()| + ensures size == |this.content().Items| } } @@ -90,7 +82,7 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { method Remove(k: K) { - m := (map k' | k' in m && k' != k :: m[k']); + m := map k' | k' in m.Keys && k' != k :: m[k']; } function Size(): (size: int) @@ -98,24 +90,4 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { |m| } } -} - -module Program { - import opened MutableMapFeasability - - method Main() { - var m := new MutableMap(); - assert m.Size() == 0; - assert "testkey" !in m.Keys(); - m.Put("testkey", "testvalue"); - //assert m.Size() == 1; - assert "testkey" in m.Keys(); - assert "testvalue" in m.Values(); - assert m.Find("testkey") == "testvalue"; - m.Remove("testkey"); - assert "testkey" !in m.Keys(); - m.Put("testkey", "testvalue"); - assert "testkey" in m.Keys(); - //assert m.Size() == 1; - } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 86b3227a..26cd2c88 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -2,3 +2,38 @@ * Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ + +import dafny.DafnySet; +import dafny.TypeDescriptor + +package MutableMap; + +public class MutableMap { + private m; + + public MutableMap() { + m = new ; + } + + public static void Put(K k, V v) { + } + + public static DafnySet Keys() { + } + + public static DafnySet Values() { + } + + public static DafnySet<(K,V)> Items() { + } + + public static V Find(K k) { + } + + public static void Remove(K k) { + + } + + public static int Size() { + } +} \ No newline at end of file From add14e127d1114fcc5cd5146b9e5f468bc4ce6e7 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 11:24:15 +0000 Subject: [PATCH 09/41] java implementation --- src/MutableMap/MutableMap.dfy | 22 ++++++++--------- src/MutableMap/MutableMap.java | 43 ++++++++++++++++++++++++---------- 2 files changed, 41 insertions(+), 24 deletions(-) diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 96613b44..67613057 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,43 +5,43 @@ // RUN: %dafny /compile:0 "%s" -module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { - class {:extern} MutableMap { - function {:extern} content(): map +module {:options "/functionSyntax:4"} MutableMap { + class MutableMap { + function {:extern "DafnyLibraries.MutableMap", "content"} content(): map reads this - constructor {:extern} () + constructor {:extern "DafnyLibraries.MutableMap", "MutableMap"} () ensures this.content() == map[] - method {:extern} Put(k: K, v: V) + method {:extern "DafnyLibraries.MutableMap", "put"} Put(k: K, v: V) modifies this ensures this.content() == old(this.content())[k := v] - function {:extern} Keys(): (keys: set) + function {:extern "DafnyLibraries.MutableMap", "keys"} Keys(): (keys: set) reads this ensures keys == this.content().Keys - function {:extern} Values(): (values: set) + function {:extern "DafnyLibraries.MutableMap", "values"} Values(): (values: set) reads this ensures values == this.content().Values - function {:extern} Items(): (items: set<(K,V)>) + function {:extern "DafnyLibraries.MutableMap", "items"} Items(): (items: set<(K,V)>) reads this ensures items == this.content().Items ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - function {:extern} Find(k: K): (v: V) + function {:extern "DafnyLibraries.MutableMap", "find"} Find(k: K): (v: V) reads this requires k in this.Keys() ensures v in this.content().Values ensures this.content()[k] == v - method {:extern} Remove(k: K) + method {:extern "DafnyLibraries.MutableMap", "remove"} Remove(k: K) modifies this ensures forall k' :: k' in old(this.content)().Keys && k' != k ==> k' in this.content().Keys && old(this.content)()[k'] == this.content()[k'] ensures forall k' :: k' in this.content().Keys ==> k' in old(this.content)().Keys && k' != k - function {:extern} Size(): (size: int) + function {:extern "DafnyLibraries.MutableMap", "size"} Size(): (size: int) reads this ensures size == |this.content().Items| } diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 26cd2c88..b4e9a5de 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -4,36 +4,53 @@ *******************************************************************************/ import dafny.DafnySet; -import dafny.TypeDescriptor +import dafny.DafnyMap; +import dafny.Tuple2; -package MutableMap; +import java.util.HashMap; -public class MutableMap { - private m; +package DafnyLibraries; - public MutableMap() { - m = new ; +public class MutableMap { + private HashMap m; + + public DafnyMap content() { + return new DafnyMap<>(m); } - public static void Put(K k, V v) { + public MutableMap() { + m = new HashMap<>(); } - public static DafnySet Keys() { + public void put(K k, V v) { + m.put(k, v); } - public static DafnySet Values() { + public DafnySet keys() { + return new DafnySet<>(m.keySet()); } - public static DafnySet<(K,V)> Items() { + public DafnySet values() { + return new DafnySet<>(m.values()); } - public static V Find(K k) { + public DafnySet> items() { + ArrayList> list = new ArrayList>(); + for (Entry entry : m.entrySet()) { + list.add(new Tuple2(entry.getKey(), entry.getValue())); + } + return new DafnySet>(list); } - public static void Remove(K k) { + public V find(K k) { + m.get(k); + } + public void remove(K k) { + m.remove(k); } - public static int Size() { + public int size() { + return m.size(); } } \ No newline at end of file From 712fcbbe1810a52ffb46d481e821ba68c42be5b4 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 11:30:58 +0000 Subject: [PATCH 10/41] java types --- src/MutableMap/MutableMap.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index b4e9a5de..fa03343f 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -14,7 +14,7 @@ public class MutableMap { private HashMap m; - public DafnyMap content() { + public DafnyMap> content() { return new DafnyMap<>(m); } @@ -26,15 +26,15 @@ public void put(K k, V v) { m.put(k, v); } - public DafnySet keys() { + public DafnySet keys() { return new DafnySet<>(m.keySet()); } - public DafnySet values() { + public DafnySet values() { return new DafnySet<>(m.values()); } - public DafnySet> items() { + public DafnySet> items() { ArrayList> list = new ArrayList>(); for (Entry entry : m.entrySet()) { list.add(new Tuple2(entry.getKey(), entry.getValue())); From 0484df0c33de825529285455fb21d61b64cf57e8 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 12:43:46 +0000 Subject: [PATCH 11/41] correct mapping --- src/MutableMap/MutableMap.dfy | 67 ++++-------------------- src/MutableMap/MutableMap.java | 3 +- src/MutableMap/MutableMapFeasability.dfy | 46 ++++++++++++++++ src/MutableMap/README.md | 2 +- 4 files changed, 59 insertions(+), 59 deletions(-) create mode 100644 src/MutableMap/MutableMapFeasability.dfy diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 67613057..9513bb35 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,89 +5,44 @@ // RUN: %dafny /compile:0 "%s" -module {:options "/functionSyntax:4"} MutableMap { - class MutableMap { - function {:extern "DafnyLibraries.MutableMap", "content"} content(): map +module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { + class {:extern "MutableMap"} MutableMap { + function {:extern "content"} content(): map reads this - constructor {:extern "DafnyLibraries.MutableMap", "MutableMap"} () + constructor {:extern"MutableMap"} () ensures this.content() == map[] - method {:extern "DafnyLibraries.MutableMap", "put"} Put(k: K, v: V) + method {:extern "put"} Put(k: K, v: V) modifies this ensures this.content() == old(this.content())[k := v] - function {:extern "DafnyLibraries.MutableMap", "keys"} Keys(): (keys: set) + function {:extern "keys"} Keys(): (keys: set) reads this ensures keys == this.content().Keys - function {:extern "DafnyLibraries.MutableMap", "values"} Values(): (values: set) + function {:extern "values"} Values(): (values: set) reads this ensures values == this.content().Values - function {:extern "DafnyLibraries.MutableMap", "items"} Items(): (items: set<(K,V)>) + function {:extern "items"} Items(): (items: set<(K,V)>) reads this ensures items == this.content().Items ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - function {:extern "DafnyLibraries.MutableMap", "find"} Find(k: K): (v: V) + function {:extern "find"} Find(k: K): (v: V) reads this requires k in this.Keys() ensures v in this.content().Values ensures this.content()[k] == v - method {:extern "DafnyLibraries.MutableMap", "remove"} Remove(k: K) + method {:extern "remove"} Remove(k: K) modifies this ensures forall k' :: k' in old(this.content)().Keys && k' != k ==> k' in this.content().Keys && old(this.content)()[k'] == this.content()[k'] ensures forall k' :: k' in this.content().Keys ==> k' in old(this.content)().Keys && k' != k - function {:extern "DafnyLibraries.MutableMap", "size"} Size(): (size: int) + function {:extern "size"} Size(): (size: int) reads this ensures size == |this.content().Items| } -} - -module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { - class MutableMap ... { - var m: map - - function content(): map { - m - } - - constructor () - { - m := map[]; - } - - method Put(k: K, v: V) - { - m := m[k := v]; - } - - function Keys(): (keys: set) - { - m.Keys - } - - function Values(): (values: set) - { - m.Values - } - - function Find(k: K): (v: V) - { - m[k] - } - - method Remove(k: K) - { - m := map k' | k' in m.Keys && k' != k :: m[k']; - } - - function Size(): (size: int) - { - |m| - } - } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index fa03343f..eb321f62 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -2,6 +2,7 @@ * Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ +package MutableMap; import dafny.DafnySet; import dafny.DafnyMap; @@ -9,8 +10,6 @@ import java.util.HashMap; -package DafnyLibraries; - public class MutableMap { private HashMap m; diff --git a/src/MutableMap/MutableMapFeasability.dfy b/src/MutableMap/MutableMapFeasability.dfy new file mode 100644 index 00000000..d6db289b --- /dev/null +++ b/src/MutableMap/MutableMapFeasability.dfy @@ -0,0 +1,46 @@ +include "MutableMap.dfy" + +module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { + class MutableMap ... { + var m: map + + function content(): map { + m + } + + constructor () + { + m := map[]; + } + + method Put(k: K, v: V) + { + m := m[k := v]; + } + + function Keys(): (keys: set) + { + m.Keys + } + + function Values(): (values: set) + { + m.Values + } + + function Find(k: K): (v: V) + { + m[k] + } + + method Remove(k: K) + { + m := map k' | k' in m.Keys && k' != k :: m[k']; + } + + function Size(): (size: int) + { + |m| + } + } +} \ No newline at end of file diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md index fea702d0..1975bd16 100644 --- a/src/MutableMap/README.md +++ b/src/MutableMap/README.md @@ -12,7 +12,7 @@ For example, to run a `Program.dfy` file that depends on the `MutableMap` module ```bash # Java -$ dafny run Program.dfy --target:java --include libraries/src/MutableMap/MutableMap.java +$ dafny run Program.dfy --target:java --input libraries/src/MutableMap/MutableMap.java ``` (If you aren't using `dafny run` to run your program, From 3ee5d7ccd79a1a74329ab7e1e6835c0104a203cb Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 14:08:16 +0000 Subject: [PATCH 12/41] type descriptor --- src/MutableMap/MutableMap.java | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index eb321f62..0bfd8e8f 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -7,13 +7,17 @@ import dafny.DafnySet; import dafny.DafnyMap; import dafny.Tuple2; +import dafny.TypeDescriptor; import java.util.HashMap; +import java.util.ArrayList; +import java.util.Map; + public class MutableMap { private HashMap m; - public DafnyMap> content() { + public DafnyMap content() { return new DafnyMap<>(m); } @@ -21,6 +25,10 @@ public MutableMap() { m = new HashMap<>(); } + public MutableMap(TypeDescriptor x, TypeDescriptor y) { + m = new HashMap<>(); + } + public void put(K k, V v) { m.put(k, v); } @@ -35,14 +43,14 @@ public DafnySet values() { public DafnySet> items() { ArrayList> list = new ArrayList>(); - for (Entry entry : m.entrySet()) { + for (Map.Entry entry : m.entrySet()) { list.add(new Tuple2(entry.getKey(), entry.getValue())); } return new DafnySet>(list); } public V find(K k) { - m.get(k); + return m.get(k); } public void remove(K k) { From 91ec370dd425cf04085d88f2a8ab2a87543cbdca Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 15:32:39 +0000 Subject: [PATCH 13/41] fixes --- src/MutableMap/MutableMap.dfy | 8 ++++---- src/MutableMap/MutableMapFeasability.dfy | 22 +++++++++++++++++++--- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 9513bb35..1e17d73a 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -6,11 +6,11 @@ // RUN: %dafny /compile:0 "%s" module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { - class {:extern "MutableMap"} MutableMap { + class {:extern "MutableMap"} MutableMap { function {:extern "content"} content(): map reads this - constructor {:extern"MutableMap"} () + constructor {:extern "MutableMap"} () ensures this.content() == map[] method {:extern "put"} Put(k: K, v: V) @@ -25,12 +25,12 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { reads this ensures values == this.content().Values - function {:extern "items"} Items(): (items: set<(K,V)>) + function {:extern "items"} Items(): (items: set<(K,V)>) reads this ensures items == this.content().Items ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - function {:extern "find"} Find(k: K): (v: V) + function {:extern "find"} Find(k: K): (v: V) reads this requires k in this.Keys() ensures v in this.content().Values diff --git a/src/MutableMap/MutableMapFeasability.dfy b/src/MutableMap/MutableMapFeasability.dfy index d6db289b..828926d0 100644 --- a/src/MutableMap/MutableMapFeasability.dfy +++ b/src/MutableMap/MutableMapFeasability.dfy @@ -1,7 +1,7 @@ include "MutableMap.dfy" module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { - class MutableMap ... { + class MutableMap ... { var m: map function content(): map { @@ -18,16 +18,32 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { m := m[k := v]; } - function Keys(): (keys: set) + function Keys(): set { m.Keys } - function Values(): (values: set) + function Values(): set { m.Values } + function Items(): set<(K,V)> + { + var items := set k | k in m.Keys :: (k, m[k]); + assert items == m.Items by { + forall k | k in m.Keys ensures (k, m[k]) in m.Items { + assert (k, m[k]) in m.Items; + } + assert items <= m.Items; + forall x | x in m.Items ensures x in items { + assert (x.0, m[x.0]) in items; + } + assert m.Items <= items; + } + items + } + function Find(k: K): (v: V) { m[k] From 36e2108e26dafbb9e082f5f0a273655d03791fd7 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 15:34:50 +0000 Subject: [PATCH 14/41] readme --- src/MutableMap/README.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md index 1975bd16..60fcc02d 100644 --- a/src/MutableMap/README.md +++ b/src/MutableMap/README.md @@ -7,12 +7,11 @@ To use `MutableMap` in your code, you must: 1. `include` and `import` the `MutableMap` module as you would any other library module 2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program -For example, to run a `Program.dfy` file that depends on the `MutableMap` module, run the following. -(This assumes you have the `libraries` repository checked out within the working directory.) +For example, to run the `MutableMapExamples.dfy` file in the `libraries/examples/MutableMap`directory that depends on the `MutableMap` module, run the following. ```bash # Java -$ dafny run Program.dfy --target:java --input libraries/src/MutableMap/MutableMap.java +$ dafny run MutableMapExamples.dfy --target:java --input ../../src/MutableMap/MutableMap.java ``` (If you aren't using `dafny run` to run your program, From 4f5f5bc9df1f709ea169fde0bb4cfa4c64245cfb Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 15:50:25 +0000 Subject: [PATCH 15/41] remove ensures --- examples/MutableMap/MutableMapExamples.dfy | 4 +++- src/MutableMap/MutableMap.dfy | 6 ++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index b6851138..e1e11c4e 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -34,7 +34,9 @@ module MutableMapExamples { assert "testkey" in m.Keys(); assert "testkey2" in m.Keys(); m.Remove("testkey"); - /* assert m.Keys() == {"testkey2"}; + assert "testkey" !in m.Keys(); +/* assert "testkey2" in m.Keys(); + assert m.Keys() == {"testkey2"}; assert m.Values() == {"testvalue2"}; assert m.Items() == {("testkey2", "testvalue2")}; */ } diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 1e17d73a..f6699679 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -38,8 +38,10 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { method {:extern "remove"} Remove(k: K) modifies this - ensures forall k' :: k' in old(this.content)().Keys && k' != k ==> k' in this.content().Keys && old(this.content)()[k'] == this.content()[k'] - ensures forall k' :: k' in this.content().Keys ==> k' in old(this.content)().Keys && k' != k + ensures forall k' | k' in old(this.content)().Keys :: k' != k ==> (k' in this.content().Keys && old(this.content)()[k'] == this.content()[k']) + ensures forall k' | k' in this.content().Keys :: k' in old(this.content)().Keys && k' != k + ensures k in old(this.content)().Keys ==> k !in this.content().Keys + ensures this.content().Values == set k' | k' in old(this.content)().Keys && k' != k :: this.content()[k'] function {:extern "size"} Size(): (size: int) reads this From 5e67baa09e1bbb7e94a50ae0723dec89a6b36b0d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 15:55:22 +0000 Subject: [PATCH 16/41] fix old clause --- examples/MutableMap/MutableMapExamples.dfy | 4 +--- src/MutableMap/MutableMap.dfy | 5 +---- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index e1e11c4e..64d8d9e8 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -34,10 +34,8 @@ module MutableMapExamples { assert "testkey" in m.Keys(); assert "testkey2" in m.Keys(); m.Remove("testkey"); - assert "testkey" !in m.Keys(); -/* assert "testkey2" in m.Keys(); assert m.Keys() == {"testkey2"}; assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey2", "testvalue2")}; */ + assert m.Items() == {("testkey2", "testvalue2")}; } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index f6699679..e05c1a40 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -38,10 +38,7 @@ module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { method {:extern "remove"} Remove(k: K) modifies this - ensures forall k' | k' in old(this.content)().Keys :: k' != k ==> (k' in this.content().Keys && old(this.content)()[k'] == this.content()[k']) - ensures forall k' | k' in this.content().Keys :: k' in old(this.content)().Keys && k' != k - ensures k in old(this.content)().Keys ==> k !in this.content().Keys - ensures this.content().Values == set k' | k' in old(this.content)().Keys && k' != k :: this.content()[k'] + ensures this.content() == old(this.content()) - {k} function {:extern "size"} Size(): (size: int) reads this From ab244dfddbe9dc0785910c9debecc502dba457f2 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 16:39:19 +0000 Subject: [PATCH 17/41] trait feasability --- .../MutableMap/MutableMap.java | 63 +++++++++++++++ src/MutableMap/MutableMapFeasability.dfy | 76 +++++++++++++++++-- 2 files changed, 133 insertions(+), 6 deletions(-) create mode 100644 src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java diff --git a/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java b/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java new file mode 100644 index 00000000..0bfd8e8f --- /dev/null +++ b/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java @@ -0,0 +1,63 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ +package MutableMap; + +import dafny.DafnySet; +import dafny.DafnyMap; +import dafny.Tuple2; +import dafny.TypeDescriptor; + +import java.util.HashMap; +import java.util.ArrayList; +import java.util.Map; + + +public class MutableMap { + private HashMap m; + + public DafnyMap content() { + return new DafnyMap<>(m); + } + + public MutableMap() { + m = new HashMap<>(); + } + + public MutableMap(TypeDescriptor x, TypeDescriptor y) { + m = new HashMap<>(); + } + + public void put(K k, V v) { + m.put(k, v); + } + + public DafnySet keys() { + return new DafnySet<>(m.keySet()); + } + + public DafnySet values() { + return new DafnySet<>(m.values()); + } + + public DafnySet> items() { + ArrayList> list = new ArrayList>(); + for (Map.Entry entry : m.entrySet()) { + list.add(new Tuple2(entry.getKey(), entry.getValue())); + } + return new DafnySet>(list); + } + + public V find(K k) { + return m.get(k); + } + + public void remove(K k) { + m.remove(k); + } + + public int size() { + return m.size(); + } +} \ No newline at end of file diff --git a/src/MutableMap/MutableMapFeasability.dfy b/src/MutableMap/MutableMapFeasability.dfy index 828926d0..5b20b8fa 100644 --- a/src/MutableMap/MutableMapFeasability.dfy +++ b/src/MutableMap/MutableMapFeasability.dfy @@ -1,10 +1,57 @@ include "MutableMap.dfy" -module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { - class MutableMap ... { +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +module {:options "/functionSyntax:4"} MutableMapTrait { + trait MutableMapTrait { + function content(): map + reads this + + method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] + + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + + function Values(): (values: set) + reads this + ensures values == this.content().Values + + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + + function Find(k: K): (v: V) + reads this + requires k in this.Keys() + ensures v in this.content().Values + ensures this.content()[k] == v + + method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} + + function Size(): (size: int) + reads this + ensures size == |this.content().Items| + } +} + +module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMapTrait { + class MutableMap extends MutableMapTrait { var m: map - function content(): map { + function content(): map + reads this + { m } @@ -14,21 +61,30 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { } method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] { m := m[k := v]; } - function Keys(): set + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys { m.Keys } - function Values(): set + function Values(): (values: set) + reads this + ensures values == this.content().Values { m.Values } - function Items(): set<(K,V)> + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) { var items := set k | k in m.Keys :: (k, m[k]); assert items == m.Items by { @@ -45,16 +101,24 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMap { } function Find(k: K): (v: V) + reads this + requires k in this.Keys() + ensures v in this.content().Values + ensures this.content()[k] == v { m[k] } method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} { m := map k' | k' in m.Keys && k' != k :: m[k']; } function Size(): (size: int) + reads this + ensures size == |this.content().Items| { |m| } From 8fb717781c6b11f3985f0d0c086a13302ad5c0db Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 17:12:42 +0000 Subject: [PATCH 18/41] space --- src/MutableMap/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md index 60fcc02d..d7260fb9 100644 --- a/src/MutableMap/README.md +++ b/src/MutableMap/README.md @@ -7,7 +7,7 @@ To use `MutableMap` in your code, you must: 1. `include` and `import` the `MutableMap` module as you would any other library module 2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program -For example, to run the `MutableMapExamples.dfy` file in the `libraries/examples/MutableMap`directory that depends on the `MutableMap` module, run the following. +For example, to run the `MutableMapExamples.dfy` file in the `libraries/examples/MutableMap` directory that depends on the `MutableMap` module, run the following. ```bash # Java From f05c75ff317392990549976f245b932089ad915e Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 17:15:01 +0000 Subject: [PATCH 19/41] remove files --- .../MutableMap/MutableMap.java | 63 ------------------- src/MutableMap/README.md | 2 +- 2 files changed, 1 insertion(+), 64 deletions(-) delete mode 100644 src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java diff --git a/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java b/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java deleted file mode 100644 index 0bfd8e8f..00000000 --- a/src/MutableMap/MutableMapFeasability-java/MutableMap/MutableMap.java +++ /dev/null @@ -1,63 +0,0 @@ -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ -package MutableMap; - -import dafny.DafnySet; -import dafny.DafnyMap; -import dafny.Tuple2; -import dafny.TypeDescriptor; - -import java.util.HashMap; -import java.util.ArrayList; -import java.util.Map; - - -public class MutableMap { - private HashMap m; - - public DafnyMap content() { - return new DafnyMap<>(m); - } - - public MutableMap() { - m = new HashMap<>(); - } - - public MutableMap(TypeDescriptor x, TypeDescriptor y) { - m = new HashMap<>(); - } - - public void put(K k, V v) { - m.put(k, v); - } - - public DafnySet keys() { - return new DafnySet<>(m.keySet()); - } - - public DafnySet values() { - return new DafnySet<>(m.values()); - } - - public DafnySet> items() { - ArrayList> list = new ArrayList>(); - for (Map.Entry entry : m.entrySet()) { - list.add(new Tuple2(entry.getKey(), entry.getValue())); - } - return new DafnySet>(list); - } - - public V find(K k) { - return m.get(k); - } - - public void remove(K k) { - m.remove(k); - } - - public int size() { - return m.size(); - } -} \ No newline at end of file diff --git a/src/MutableMap/README.md b/src/MutableMap/README.md index d7260fb9..d4619fbd 100644 --- a/src/MutableMap/README.md +++ b/src/MutableMap/README.md @@ -7,7 +7,7 @@ To use `MutableMap` in your code, you must: 1. `include` and `import` the `MutableMap` module as you would any other library module 2. incorporate the corresponding language-specific implementation file (that is, currently, `MutableMap.java`) when building or running your program -For example, to run the `MutableMapExamples.dfy` file in the `libraries/examples/MutableMap` directory that depends on the `MutableMap` module, run the following. +For example, to run the `MutableMapExamples.dfy` file in the `examples/MutableMap` directory that depends on the `MutableMap` module, run the following. ```bash # Java From ecf5e1f8817029314f504929a80bc1d18c14ca0a Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 16 Feb 2023 17:44:32 +0000 Subject: [PATCH 20/41] add print statement --- examples/MutableMap/MutableMapExamples.dfy | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 64d8d9e8..19d5aebf 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -31,6 +31,8 @@ module MutableMapExamples { assert m.Values() == {"testvalue2"}; assert m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}; assert m.Size() == 2; + print m.Find("testkey"), "\n"; + print m.Find("testkey2"), "\n"; assert "testkey" in m.Keys(); assert "testkey2" in m.Keys(); m.Remove("testkey"); From 4cfb77f5ab7df714eb5e8aa49b127830b05eb56d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 17 Feb 2023 15:27:05 +0000 Subject: [PATCH 21/41] traits problem --- examples/MutableMap/MutableMapExamples.dfy | 68 +++++++++++++--------- src/MutableMap/MutableMap.dfy | 46 ++++++++++----- src/MutableMap/MutableMapFeasability.dfy | 58 +++++------------- 3 files changed, 89 insertions(+), 83 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 19d5aebf..17c3cdbc 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -6,38 +6,54 @@ // RUN: %dafny /compile:0 "%s" include "../../src/MutableMap/MutableMap.dfy" +include "../../src/Wrappers.dfy" -module MutableMapExamples { +module {:options "-functionSyntax:4"} MutableMapExamples { import opened MutableMap + import opened Wrappers - method Main() { - var m := new MutableMap(); - assert m.Keys() == {}; - assert m.Values() == {}; - assert m.Items() == {}; - assert m.Size() == 0; + method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { + match maybeMsg { + case None => { + expect p; + } + case Some(msg) => { + expect p, msg; + } + } + } + + method Main() + { + var m := MutableMap.Make(); + AssertAndExpect(m.Keys() == {}); + AssertAndExpect(m.Values() == {}); + AssertAndExpect(m.Items() == {}); + AssertAndExpect(m.Size() == 0); m.Put("testkey", "testvalue"); - assert m.Find("testkey") == "testvalue"; - assert m.Keys() == {"testkey"}; - assert m.Values() == {"testvalue"}; - assert m.Items() == {("testkey", "testvalue")}; - assert m.Size() == 1; + AssertAndExpect(m.Select("testkey") == "testvalue"); + AssertAndExpect(m.Keys() == {"testkey"}); + AssertAndExpect(m.Values() == {"testvalue"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue")}); + AssertAndExpect(m.Size() == 1); m.Put("testkey", "testvalue2"); - assert m.Keys() == {"testkey"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey", "testvalue2")}; + AssertAndExpect(m.Keys() == {"testkey"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue2")}); m.Put("testkey2", "testvalue2"); - assert m.Keys() == {"testkey", "testkey2"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}; - assert m.Size() == 2; - print m.Find("testkey"), "\n"; - print m.Find("testkey2"), "\n"; - assert "testkey" in m.Keys(); - assert "testkey2" in m.Keys(); + AssertAndExpect(m.Keys() == {"testkey", "testkey2"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}); + AssertAndExpect(m.Size() == 2); + AssertAndExpect("testkey" in m.Keys()); + AssertAndExpect("testkey2" in m.Keys()); + print m.Select("testkey"), "\n"; + print m.Select("testkey2"), "\n"; m.Remove("testkey"); - assert m.Keys() == {"testkey2"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey2", "testvalue2")}; + AssertAndExpect(m.SelectOpt("testkey").None?); + AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); + AssertAndExpect(m.Keys() == {"testkey2"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index e05c1a40..9e138ce3 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,42 +5,62 @@ // RUN: %dafny /compile:0 "%s" -module {:extern "MutableMap"} {:options "/functionSyntax:4"} MutableMap { - class {:extern "MutableMap"} MutableMap { - function {:extern "content"} content(): map +include "../Wrappers.dfy" + +module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { + import opened Wrappers + + trait {:extern} MutableMap { + function content(): map reads this - constructor {:extern "MutableMap"} () - ensures this.content() == map[] + static method {:extern} Make() returns (m: MutableMap) + ensures m.content() == map[] + ensures fresh(m) - method {:extern "put"} Put(k: K, v: V) + method Put(k: K, v: V) modifies this ensures this.content() == old(this.content())[k := v] - function {:extern "keys"} Keys(): (keys: set) + function Keys(): (keys: set) reads this ensures keys == this.content().Keys - function {:extern "values"} Values(): (values: set) + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + + function Values(): (values: set) reads this ensures values == this.content().Values - function {:extern "items"} Items(): (items: set<(K,V)>) + function Items(): (items: set<(K,V)>) reads this ensures items == this.content().Items ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - function {:extern "find"} Find(k: K): (v: V) + function Select(k: K): (v: V) reads this - requires k in this.Keys() + requires this.HasKey(k) ensures v in this.content().Values ensures this.content()[k] == v + + function SelectOpt(k: K): (o: Option) + reads this + ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) + ensures o.None? ==> !this.HasKey(k) + { + if this.HasKey(k) then + Some(this.Select(k)) + else + None + } - method {:extern "remove"} Remove(k: K) + method Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} - function {:extern "size"} Size(): (size: int) + function Size(): (size: int) reads this ensures size == |this.content().Items| } diff --git a/src/MutableMap/MutableMapFeasability.dfy b/src/MutableMap/MutableMapFeasability.dfy index 5b20b8fa..f70d2629 100644 --- a/src/MutableMap/MutableMapFeasability.dfy +++ b/src/MutableMap/MutableMapFeasability.dfy @@ -1,5 +1,3 @@ -include "MutableMap.dfy" - /******************************************************************************* * Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT @@ -7,46 +5,10 @@ include "MutableMap.dfy" // RUN: %dafny /compile:0 "%s" -module {:options "/functionSyntax:4"} MutableMapTrait { - trait MutableMapTrait { - function content(): map - reads this - - method Put(k: K, v: V) - modifies this - ensures this.content() == old(this.content())[k := v] - - function Keys(): (keys: set) - reads this - ensures keys == this.content().Keys - - function Values(): (values: set) - reads this - ensures values == this.content().Values - - function Items(): (items: set<(K,V)>) - reads this - ensures items == this.content().Items - ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - - function Find(k: K): (v: V) - reads this - requires k in this.Keys() - ensures v in this.content().Values - ensures this.content()[k] == v - - method Remove(k: K) - modifies this - ensures this.content() == old(this.content()) - {k} - - function Size(): (size: int) - reads this - ensures size == |this.content().Items| - } -} - -module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMapTrait { - class MutableMap extends MutableMapTrait { +include "MutableMap.dfy" + +module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMap { + class MutableMapDafny extends MutableMap { var m: map function content(): map @@ -56,6 +18,7 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMapTr } constructor () + ensures this.content() == map[] { m := map[]; } @@ -74,6 +37,13 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMapTr m.Keys } + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + { + k in m.Keys + } + function Values(): (values: set) reads this ensures values == this.content().Values @@ -100,9 +70,9 @@ module {:options "/functionSyntax:4"} MutableMapFeasability refines MutableMapTr items } - function Find(k: K): (v: V) + function Select(k: K): (v: V) reads this - requires k in this.Keys() + requires this.HasKey(k) ensures v in this.content().Values ensures this.content()[k] == v { From 0e2a764d7fc4ebd823a3fec44bed123cb36bfa1d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 17 Feb 2023 15:27:44 +0000 Subject: [PATCH 22/41] traits --- src/MutableMap/MutableMap.java | 41 ++++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 17 deletions(-) diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 0bfd8e8f..f5543f60 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -2,46 +2,53 @@ * Copyright by the contributors to the Dafny Project * SPDX-License-Identifier: MIT *******************************************************************************/ -package MutableMap; +package DafnyLibraries; import dafny.DafnySet; import dafny.DafnyMap; import dafny.Tuple2; import dafny.TypeDescriptor; -import java.util.HashMap; +import java.util.concurrent.*; import java.util.ArrayList; import java.util.Map; - public class MutableMap { - private HashMap m; + private ConcurrentHashMap m; - public DafnyMap content() { - return new DafnyMap<>(m); + public DafnyMap Content() { + return new DafnyMap(m); } public MutableMap() { - m = new HashMap<>(); + m = new ConcurrentHashMap(); } public MutableMap(TypeDescriptor x, TypeDescriptor y) { - m = new HashMap<>(); + m = new ConcurrentHashMap(); + } + + public static MutableMap Make() { + return new MutableMap(); } - public void put(K k, V v) { + public void Put(K k, V v) { m.put(k, v); } - public DafnySet keys() { - return new DafnySet<>(m.keySet()); + public DafnySet Keys() { + return new DafnySet(m.keySet()); + } + + public boolean HasKey(K k) { + return m.containsKey(k); } - public DafnySet values() { - return new DafnySet<>(m.values()); + public DafnySet Values() { + return new DafnySet(m.values()); } - public DafnySet> items() { + public DafnySet> Items() { ArrayList> list = new ArrayList>(); for (Map.Entry entry : m.entrySet()) { list.add(new Tuple2(entry.getKey(), entry.getValue())); @@ -49,15 +56,15 @@ public DafnySet> items() { return new DafnySet>(list); } - public V find(K k) { + public V Select(K k) { return m.get(k); } - public void remove(K k) { + public void Remove(K k) { m.remove(k); } - public int size() { + public int Size() { return m.size(); } } \ No newline at end of file From 72e9eb3a5fcadf035d7a167274947a99fdc31174 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 17 Feb 2023 19:54:31 +0000 Subject: [PATCH 23/41] error-free version --- examples/MutableMap/MutableMapExamples.dfy | 64 ++++++++----------- src/MutableMap/MutableMap.dfy | 44 +++++-------- src/MutableMap/MutableMap.java | 5 +- ...MapFeasability.dfy => MutableMapDafny.dfy} | 6 +- src/MutableMap/MutableMapTrait.dfy | 63 ++++++++++++++++++ 5 files changed, 107 insertions(+), 75 deletions(-) rename src/MutableMap/{MutableMapFeasability.dfy => MutableMapDafny.dfy} (94%) create mode 100644 src/MutableMap/MutableMapTrait.dfy diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 17c3cdbc..96941e45 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -6,54 +6,40 @@ // RUN: %dafny /compile:0 "%s" include "../../src/MutableMap/MutableMap.dfy" -include "../../src/Wrappers.dfy" module {:options "-functionSyntax:4"} MutableMapExamples { import opened MutableMap - import opened Wrappers - method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { - match maybeMsg { - case None => { - expect p; - } - case Some(msg) => { - expect p, msg; - } - } - } - - method Main() - { - var m := MutableMap.Make(); - AssertAndExpect(m.Keys() == {}); - AssertAndExpect(m.Values() == {}); - AssertAndExpect(m.Items() == {}); - AssertAndExpect(m.Size() == 0); + method Main() { + var m := new MutableMap(); + assert m.Keys() == {}; + assert m.Values() == {}; + assert m.Items() == {}; + assert m.Size() == 0; m.Put("testkey", "testvalue"); - AssertAndExpect(m.Select("testkey") == "testvalue"); - AssertAndExpect(m.Keys() == {"testkey"}); - AssertAndExpect(m.Values() == {"testvalue"}); - AssertAndExpect(m.Items() == {("testkey", "testvalue")}); - AssertAndExpect(m.Size() == 1); + assert m.Select("testkey") == "testvalue"; + assert m.Keys() == {"testkey"}; + assert m.Values() == {"testvalue"}; + assert m.Items() == {("testkey", "testvalue")}; + assert m.Size() == 1; m.Put("testkey", "testvalue2"); - AssertAndExpect(m.Keys() == {"testkey"}); - AssertAndExpect(m.Values() == {"testvalue2"}); - AssertAndExpect(m.Items() == {("testkey", "testvalue2")}); + assert m.Keys() == {"testkey"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey", "testvalue2")}; m.Put("testkey2", "testvalue2"); - AssertAndExpect(m.Keys() == {"testkey", "testkey2"}); - AssertAndExpect(m.Values() == {"testvalue2"}); - AssertAndExpect(m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}); - AssertAndExpect(m.Size() == 2); - AssertAndExpect("testkey" in m.Keys()); - AssertAndExpect("testkey2" in m.Keys()); + assert m.Keys() == {"testkey", "testkey2"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}; + assert m.Size() == 2; + assert "testkey" in m.Keys(); + assert "testkey2" in m.Keys(); print m.Select("testkey"), "\n"; print m.Select("testkey2"), "\n"; m.Remove("testkey"); - AssertAndExpect(m.SelectOpt("testkey").None?); - AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); - AssertAndExpect(m.Keys() == {"testkey2"}); - AssertAndExpect(m.Values() == {"testvalue2"}); - AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); + assert m.SelectOpt("testkey").None?; + assert m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"; + assert m.Keys() == {"testkey2"}; + assert m.Values() == {"testvalue2"}; + assert m.Items() == {("testkey2", "testvalue2")}; } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 9e138ce3..400ed27f 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,62 +5,48 @@ // RUN: %dafny /compile:0 "%s" -include "../Wrappers.dfy" +include "MutableMapTrait.dfy" -module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { - import opened Wrappers +module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refines MutableMapTrait { + class {:extern} MutableMap extends MutableMapTrait { + constructor {:extern} () + ensures this.content() == map[] - trait {:extern} MutableMap { - function content(): map + function {:extern} content(): map reads this - static method {:extern} Make() returns (m: MutableMap) - ensures m.content() == map[] - ensures fresh(m) - - method Put(k: K, v: V) + method {:extern} Put(k: K, v: V) modifies this - ensures this.content() == old(this.content())[k := v] + ensures this.content() == old(this.content())[k := v] - function Keys(): (keys: set) + function {:extern} Keys(): (keys: set) reads this ensures keys == this.content().Keys - predicate HasKey(k: K) + predicate {:extern} HasKey(k: K) reads this ensures HasKey(k) <==> k in this.content().Keys - function Values(): (values: set) + function {:extern} Values(): (values: set) reads this ensures values == this.content().Values - function Items(): (items: set<(K,V)>) + function {:extern} Items(): (items: set<(K,V)>) reads this ensures items == this.content().Items ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - function Select(k: K): (v: V) + function {:extern} Select(k: K): (v: V) reads this requires this.HasKey(k) ensures v in this.content().Values ensures this.content()[k] == v - - function SelectOpt(k: K): (o: Option) - reads this - ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) - ensures o.None? ==> !this.HasKey(k) - { - if this.HasKey(k) then - Some(this.Select(k)) - else - None - } - method Remove(k: K) + method {:extern} Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} - function Size(): (size: int) + function {:extern} Size(): (size: int) reads this ensures size == |this.content().Items| } diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index f5543f60..7fd448bd 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -8,6 +8,7 @@ import dafny.DafnyMap; import dafny.Tuple2; import dafny.TypeDescriptor; +import dafny.Helpers; import java.util.concurrent.*; import java.util.ArrayList; @@ -28,10 +29,6 @@ public MutableMap(TypeDescriptor x, TypeDescriptor y) { m = new ConcurrentHashMap(); } - public static MutableMap Make() { - return new MutableMap(); - } - public void Put(K k, V v) { m.put(k, v); } diff --git a/src/MutableMap/MutableMapFeasability.dfy b/src/MutableMap/MutableMapDafny.dfy similarity index 94% rename from src/MutableMap/MutableMapFeasability.dfy rename to src/MutableMap/MutableMapDafny.dfy index f70d2629..a74667d3 100644 --- a/src/MutableMap/MutableMapFeasability.dfy +++ b/src/MutableMap/MutableMapDafny.dfy @@ -5,10 +5,10 @@ // RUN: %dafny /compile:0 "%s" -include "MutableMap.dfy" +include "MutableMapTrait.dfy" -module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMap { - class MutableMapDafny extends MutableMap { +module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMapTrait { + class MutableMapDafny extends MutableMapTrait { var m: map function content(): map diff --git a/src/MutableMap/MutableMapTrait.dfy b/src/MutableMap/MutableMapTrait.dfy new file mode 100644 index 00000000..d89a52fb --- /dev/null +++ b/src/MutableMap/MutableMapTrait.dfy @@ -0,0 +1,63 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +include "../Wrappers.dfy" + +module {:options "-functionSyntax:4"} MutableMapTrait { + import opened Wrappers + + trait MutableMapTrait { + function content(): map + reads this + + method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] + + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + + function Values(): (values: set) + reads this + ensures values == this.content().Values + + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + + function Select(k: K): (v: V) + reads this + requires this.HasKey(k) + ensures v in this.content().Values + ensures this.content()[k] == v + + function SelectOpt(k: K): (o: Option) + reads this + ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) + ensures o.None? ==> !this.HasKey(k) + { + if this.HasKey(k) then + Some(this.Select(k)) + else + None + } + + method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} + + function Size(): (size: int) + reads this + ensures size == |this.content().Items| + } +} \ No newline at end of file From 9597028f7957c9c9f517eab0ea6499943005588a Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Wed, 22 Feb 2023 15:28:18 +0000 Subject: [PATCH 24/41] sync with customer code --- src/MutableMap/MutableMap.dfy | 3 +++ src/MutableMap/MutableMapDafny.dfy | 33 ++++++++++++++++++++++++++++-- src/MutableMap/MutableMapTrait.dfy | 9 +++++--- 3 files changed, 40 insertions(+), 5 deletions(-) diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 400ed27f..b7421d97 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -18,6 +18,8 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refi method {:extern} Put(k: K, v: V) modifies this ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} function {:extern} Keys(): (keys: set) reads this @@ -45,6 +47,7 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refi method {:extern} Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values function {:extern} Size(): (size: int) reads this diff --git a/src/MutableMap/MutableMapDafny.dfy b/src/MutableMap/MutableMapDafny.dfy index a74667d3..f1072bb8 100644 --- a/src/MutableMap/MutableMapDafny.dfy +++ b/src/MutableMap/MutableMapDafny.dfy @@ -23,11 +23,30 @@ module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMapTrait { m := map[]; } - method Put(k: K, v: V) + method Put(k: K, v: V) modifies this - ensures this.content() == old(this.content())[k := v] + ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} { m := m[k := v]; + if k in old(m).Keys { + forall v' | v' in old(m).Values + {v} ensures v' in m.Values + {old(m)[k]} { + if v' == v || v' == old(m)[k] { + assert m[k] == v; + } else { + assert m.Keys == old(m).Keys + {k}; + } + } + } + if k !in old(m).Keys { + forall v' | v' in old(m).Values + {v} ensures v' in m.Values { + if v' == v { + } else { + assert m.Keys == old(m).Keys + {k}; + } + } + } } function Keys(): (keys: set) @@ -82,8 +101,18 @@ module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMapTrait { method Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values { m := map k' | k' in m.Keys && k' != k :: m[k']; + if k in old(m).Keys { + var v := old(m)[k]; + forall v' | v' in old(m).Values ensures v' in m.Values + {v} { + if v' == v { + } else { + assert exists k' | k' in m.Keys :: old(m)[k'] == v'; + } + } + } } function Size(): (size: int) diff --git a/src/MutableMap/MutableMapTrait.dfy b/src/MutableMap/MutableMapTrait.dfy index d89a52fb..5fcb6ef8 100644 --- a/src/MutableMap/MutableMapTrait.dfy +++ b/src/MutableMap/MutableMapTrait.dfy @@ -10,13 +10,15 @@ include "../Wrappers.dfy" module {:options "-functionSyntax:4"} MutableMapTrait { import opened Wrappers - trait MutableMapTrait { + trait {:termination false} MutableMapTrait { function content(): map reads this method Put(k: K, v: V) modifies this - ensures this.content() == old(this.content())[k := v] + ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} function Keys(): (keys: set) reads this @@ -55,7 +57,8 @@ module {:options "-functionSyntax:4"} MutableMapTrait { method Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} - + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + function Size(): (size: int) reads this ensures size == |this.content().Items| From 102cd098c1c238d8a25ec9004344412488fcc3c4 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 22 Feb 2023 18:42:10 -0800 Subject: [PATCH 25/41] Add first AssertAndExpect and make the example executable --- examples/MutableMap/MutableMapExamples.dfy | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 96941e45..eb73c495 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,16 +3,29 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %run -t:java "%s" --input ../../src/MutableMap/MutableMap.java include "../../src/MutableMap/MutableMap.dfy" +include "../../src/Wrappers.dfy" module {:options "-functionSyntax:4"} MutableMapExamples { import opened MutableMap + import opened Wrappers + + method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { + match maybeMsg { + case None => { + expect p; + } + case Some(msg) => { + expect p, msg; + } + } + } method Main() { var m := new MutableMap(); - assert m.Keys() == {}; + AssertAndExpect(m.Keys() == {}); assert m.Values() == {}; assert m.Items() == {}; assert m.Size() == 0; From 0680c1bfff28803499e10acedc62591f100ec917 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 13:42:18 +0000 Subject: [PATCH 26/41] comments --- examples/MutableMap/MutableMapDafny.dfy | 131 ++++++++++++++++++ examples/MutableMap/MutableMapExamples.dfy | 53 ++++--- .../MutableMap/MutableMapTrait.dfy | 7 +- src/MutableMap/MutableMap.dfy | 14 +- 4 files changed, 177 insertions(+), 28 deletions(-) create mode 100644 examples/MutableMap/MutableMapDafny.dfy rename {src => examples}/MutableMap/MutableMapTrait.dfy (84%) diff --git a/examples/MutableMap/MutableMapDafny.dfy b/examples/MutableMap/MutableMapDafny.dfy new file mode 100644 index 00000000..1c2bd859 --- /dev/null +++ b/examples/MutableMap/MutableMapDafny.dfy @@ -0,0 +1,131 @@ +/******************************************************************************* +* Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +// RUN: %dafny /compile:0 "%s" + +include "MutableMapTrait.dfy" + +/** + * Implements mutable maps in Dafny to guard against inconsistent specifications. + * Only exists to verify feasability; not meant for actual usage. + */ +module {:options "-functionSyntax:4"} MutableMapDafny { + import opened MutableMapTrait + + class MutableMapDafny extends MutableMapTrait { + var m: map + + function content(): map + reads this + { + m + } + + constructor () + ensures this.content() == map[] + { + m := map[]; + } + + method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} + { + m := m[k := v]; + if k in old(m).Keys { + forall v' | v' in old(m).Values + {v} ensures v' in m.Values + {old(m)[k]} { + if v' == v || v' == old(m)[k] { + assert m[k] == v; + } else { + assert m.Keys == old(m).Keys + {k}; + } + } + } + if k !in old(m).Keys { + forall v' | v' in old(m).Values + {v} ensures v' in m.Values { + if v' == v { + } else { + assert m.Keys == old(m).Keys + {k}; + } + } + } + } + + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + { + m.Keys + } + + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + { + k in m.Keys + } + + function Values(): (values: set) + reads this + ensures values == this.content().Values + { + m.Values + } + + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + { + var items := set k | k in m.Keys :: (k, m[k]); + assert items == m.Items by { + forall k | k in m.Keys ensures (k, m[k]) in m.Items { + assert (k, m[k]) in m.Items; + } + assert items <= m.Items; + forall x | x in m.Items ensures x in items { + assert (x.0, m[x.0]) in items; + } + assert m.Items <= items; + } + items + } + + function Select(k: K): (v: V) + reads this + requires this.HasKey(k) + ensures v in this.content().Values + ensures this.content()[k] == v + { + m[k] + } + + method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + { + m := map k' | k' in m.Keys && k' != k :: m[k']; + if k in old(m).Keys { + var v := old(m)[k]; + forall v' | v' in old(m).Values ensures v' in m.Values + {v} { + if v' == v { + } else { + assert exists k' | k' in m.Keys :: old(m)[k'] == v'; + } + } + } + } + + function Size(): (size: int) + reads this + ensures size == |this.content().Items| + { + |m| + } + } +} \ No newline at end of file diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index eb73c495..0225a1de 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -8,8 +8,11 @@ include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" +/** + * Tests the Java interfacing implementation of mutable maps. + */ module {:options "-functionSyntax:4"} MutableMapExamples { - import opened MutableMap + import opened DafnyLibraries import opened Wrappers method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { @@ -26,33 +29,37 @@ module {:options "-functionSyntax:4"} MutableMapExamples { method Main() { var m := new MutableMap(); AssertAndExpect(m.Keys() == {}); - assert m.Values() == {}; - assert m.Items() == {}; - assert m.Size() == 0; + AssertAndExpect(m.Values() == {}); + AssertAndExpect(m.Items() == {}); + //AssertAndExpect(m.Size() == 0); + m.Put("testkey", "testvalue"); - assert m.Select("testkey") == "testvalue"; - assert m.Keys() == {"testkey"}; - assert m.Values() == {"testvalue"}; - assert m.Items() == {("testkey", "testvalue")}; - assert m.Size() == 1; + AssertAndExpect(m.Select("testkey") == "testvalue"); + AssertAndExpect(m.Keys() == {"testkey"}); + AssertAndExpect(m.Values() == {"testvalue"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue")}); + + //AssertAndExpect(m.Size() == 1); m.Put("testkey", "testvalue2"); - assert m.Keys() == {"testkey"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey", "testvalue2")}; + AssertAndExpect(m.Keys() == {"testkey"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue2")}); + m.Put("testkey2", "testvalue2"); - assert m.Keys() == {"testkey", "testkey2"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}; - assert m.Size() == 2; - assert "testkey" in m.Keys(); - assert "testkey2" in m.Keys(); + AssertAndExpect(m.Keys() == {"testkey", "testkey2"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}); + //AssertAndExpect(m.Size() == 2); + AssertAndExpect("testkey" in m.Keys()); + AssertAndExpect("testkey2" in m.Keys()); print m.Select("testkey"), "\n"; print m.Select("testkey2"), "\n"; + m.Remove("testkey"); - assert m.SelectOpt("testkey").None?; - assert m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"; - assert m.Keys() == {"testkey2"}; - assert m.Values() == {"testvalue2"}; - assert m.Items() == {("testkey2", "testvalue2")}; + //AssertAndExpect(m.SelectOpt("testkey").None?); + //AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); + AssertAndExpect(m.Keys() == {"testkey2"}); + AssertAndExpect(m.Values() == {"testvalue2"}); + AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); } } \ No newline at end of file diff --git a/src/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy similarity index 84% rename from src/MutableMap/MutableMapTrait.dfy rename to examples/MutableMap/MutableMapTrait.dfy index 5fcb6ef8..fa0837d9 100644 --- a/src/MutableMap/MutableMapTrait.dfy +++ b/examples/MutableMap/MutableMapTrait.dfy @@ -5,8 +5,13 @@ // RUN: %dafny /compile:0 "%s" -include "../Wrappers.dfy" +include "../../src/Wrappers.dfy" +/* Specifications that should be satisfied by any implementation of mutable maps. + Possible instantiations are given in "MutableMapDafny.dfy" (not meant for usage, + only exists to verify feasability) and "../../src/MutableMap/MutableMap.dfy" + (meant for usage; interfaces with external code, e.g. "../../src/MutableMap/ + MutableMap.java"). */ module {:options "-functionSyntax:4"} MutableMapTrait { import opened Wrappers diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index b7421d97..ca3cc1a2 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,10 +5,16 @@ // RUN: %dafny /compile:0 "%s" -include "MutableMapTrait.dfy" +include "../../examples/Mutablemap/MutableMapTrait.dfy" -module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refines MutableMapTrait { - class {:extern} MutableMap extends MutableMapTrait { +/** + * Implements mutable maps by interfacing with external code, e.g. + * "MutableMap.java". + */ +module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries { + import opened MutableMapTrait + + class {:extern "MutableMap"} MutableMap extends MutableMapTrait { constructor {:extern} () ensures this.content() == map[] @@ -53,4 +59,4 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refi reads this ensures size == |this.content().Items| } -} \ No newline at end of file +} From 0c2b1b108e82798c2db9986cbc3908392432856d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 14:43:46 +0000 Subject: [PATCH 27/41] module names --- examples/MutableMap/MutableMapExamples.dfy | 2 +- examples/MutableMap/MutableMapTrait.dfy | 12 +++++++----- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 0225a1de..2a62fb91 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -12,7 +12,7 @@ include "../../src/Wrappers.dfy" * Tests the Java interfacing implementation of mutable maps. */ module {:options "-functionSyntax:4"} MutableMapExamples { - import opened DafnyLibraries + import opened MutableMap import opened Wrappers method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { diff --git a/examples/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy index fa0837d9..fba14960 100644 --- a/examples/MutableMap/MutableMapTrait.dfy +++ b/examples/MutableMap/MutableMapTrait.dfy @@ -7,11 +7,13 @@ include "../../src/Wrappers.dfy" -/* Specifications that should be satisfied by any implementation of mutable maps. - Possible instantiations are given in "MutableMapDafny.dfy" (not meant for usage, - only exists to verify feasability) and "../../src/MutableMap/MutableMap.dfy" - (meant for usage; interfaces with external code, e.g. "../../src/MutableMap/ - MutableMap.java"). */ +/** + * Specifications that should be satisfied by any implementation of mutable maps. + * Possible instantiations are given in "MutableMapDafny.dfy" (not meant for usage, + * only exists to verify feasability) and "../../src/MutableMap/MutableMap.dfy" + * (meant for usage; interfaces with external code, e.g. "../../src/MutableMap/ + * MutableMap.java"). + */ module {:options "-functionSyntax:4"} MutableMapTrait { import opened Wrappers From 35feb4b1e1da585d03e362d544137ac63f8dffe7 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 14:47:20 +0000 Subject: [PATCH 28/41] naming --- src/MutableMap/MutableMap.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index ca3cc1a2..bca9d5e6 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -11,7 +11,7 @@ include "../../examples/Mutablemap/MutableMapTrait.dfy" * Implements mutable maps by interfacing with external code, e.g. * "MutableMap.java". */ -module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries { +module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { import opened MutableMapTrait class {:extern "MutableMap"} MutableMap extends MutableMapTrait { From aaadab18026e725194ec088c0bd16e100f567e37 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 16:09:03 +0000 Subject: [PATCH 29/41] run cmmand --- examples/MutableMap/MutableMapDafny.dfy | 2 +- examples/MutableMap/MutableMapTrait.dfy | 2 +- src/MutableMap/MutableMap.dfy | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/MutableMap/MutableMapDafny.dfy b/examples/MutableMap/MutableMapDafny.dfy index 1c2bd859..8739184e 100644 --- a/examples/MutableMap/MutableMapDafny.dfy +++ b/examples/MutableMap/MutableMapDafny.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" include "MutableMapTrait.dfy" diff --git a/examples/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy index fba14960..43fc098b 100644 --- a/examples/MutableMap/MutableMapTrait.dfy +++ b/examples/MutableMap/MutableMapTrait.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" include "../../src/Wrappers.dfy" diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index bca9d5e6..68b4f743 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %dafny /compile:0 "%s" +// RUN: %verify "%s" include "../../examples/Mutablemap/MutableMapTrait.dfy" From 6436ea23aa394cb0303fbdaf88699a4e08db4cb6 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 16:14:34 +0000 Subject: [PATCH 30/41] remove file --- src/MutableMap/MutableMapDafny.dfy | 125 ----------------------------- 1 file changed, 125 deletions(-) delete mode 100644 src/MutableMap/MutableMapDafny.dfy diff --git a/src/MutableMap/MutableMapDafny.dfy b/src/MutableMap/MutableMapDafny.dfy deleted file mode 100644 index f1072bb8..00000000 --- a/src/MutableMap/MutableMapDafny.dfy +++ /dev/null @@ -1,125 +0,0 @@ -/******************************************************************************* -* Copyright by the contributors to the Dafny Project -* SPDX-License-Identifier: MIT -*******************************************************************************/ - -// RUN: %dafny /compile:0 "%s" - -include "MutableMapTrait.dfy" - -module {:options "-functionSyntax:4"} MutableMapDafny refines MutableMapTrait { - class MutableMapDafny extends MutableMapTrait { - var m: map - - function content(): map - reads this - { - m - } - - constructor () - ensures this.content() == map[] - { - m := map[]; - } - - method Put(k: K, v: V) - modifies this - ensures this.content() == old(this.content())[k := v] - ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} - ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} - { - m := m[k := v]; - if k in old(m).Keys { - forall v' | v' in old(m).Values + {v} ensures v' in m.Values + {old(m)[k]} { - if v' == v || v' == old(m)[k] { - assert m[k] == v; - } else { - assert m.Keys == old(m).Keys + {k}; - } - } - } - if k !in old(m).Keys { - forall v' | v' in old(m).Values + {v} ensures v' in m.Values { - if v' == v { - } else { - assert m.Keys == old(m).Keys + {k}; - } - } - } - } - - function Keys(): (keys: set) - reads this - ensures keys == this.content().Keys - { - m.Keys - } - - predicate HasKey(k: K) - reads this - ensures HasKey(k) <==> k in this.content().Keys - { - k in m.Keys - } - - function Values(): (values: set) - reads this - ensures values == this.content().Values - { - m.Values - } - - function Items(): (items: set<(K,V)>) - reads this - ensures items == this.content().Items - ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) - { - var items := set k | k in m.Keys :: (k, m[k]); - assert items == m.Items by { - forall k | k in m.Keys ensures (k, m[k]) in m.Items { - assert (k, m[k]) in m.Items; - } - assert items <= m.Items; - forall x | x in m.Items ensures x in items { - assert (x.0, m[x.0]) in items; - } - assert m.Items <= items; - } - items - } - - function Select(k: K): (v: V) - reads this - requires this.HasKey(k) - ensures v in this.content().Values - ensures this.content()[k] == v - { - m[k] - } - - method Remove(k: K) - modifies this - ensures this.content() == old(this.content()) - {k} - ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values - { - m := map k' | k' in m.Keys && k' != k :: m[k']; - if k in old(m).Keys { - var v := old(m)[k]; - forall v' | v' in old(m).Values ensures v' in m.Values + {v} { - if v' == v { - } else { - assert exists k' | k' in m.Keys :: old(m)[k'] == v'; - } - } - } - } - - function Size(): (size: int) - reads this - ensures size == |this.content().Items| - { - |m| - } - } -} \ No newline at end of file From 196714bd686613c8387b22f55e84a0f5ccdcb56d Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 19:19:28 +0000 Subject: [PATCH 31/41] clean --- examples/MutableMap/MutableMapExamples.dfy | 7 ++++--- examples/MutableMap/MutableMapTrait.dfy | 4 ++-- src/MutableMap/MutableMap.dfy | 6 +++--- src/MutableMap/MutableMap.java | 5 +++-- 4 files changed, 12 insertions(+), 10 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 2a62fb91..8bcda1c5 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -31,15 +31,16 @@ module {:options "-functionSyntax:4"} MutableMapExamples { AssertAndExpect(m.Keys() == {}); AssertAndExpect(m.Values() == {}); AssertAndExpect(m.Items() == {}); - //AssertAndExpect(m.Size() == 0); + AssertAndExpect(m.Size() == 0); m.Put("testkey", "testvalue"); AssertAndExpect(m.Select("testkey") == "testvalue"); AssertAndExpect(m.Keys() == {"testkey"}); AssertAndExpect(m.Values() == {"testvalue"}); AssertAndExpect(m.Items() == {("testkey", "testvalue")}); + print m.Select("testkey"), "\n"; - //AssertAndExpect(m.Size() == 1); + AssertAndExpect(m.Size() == 1); m.Put("testkey", "testvalue2"); AssertAndExpect(m.Keys() == {"testkey"}); AssertAndExpect(m.Values() == {"testvalue2"}); @@ -49,7 +50,7 @@ module {:options "-functionSyntax:4"} MutableMapExamples { AssertAndExpect(m.Keys() == {"testkey", "testkey2"}); AssertAndExpect(m.Values() == {"testvalue2"}); AssertAndExpect(m.Items() == {("testkey", "testvalue2"), ("testkey2", "testvalue2")}); - //AssertAndExpect(m.Size() == 2); + AssertAndExpect(m.Size() == 2); AssertAndExpect("testkey" in m.Keys()); AssertAndExpect("testkey2" in m.Keys()); print m.Select("testkey"), "\n"; diff --git a/examples/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy index 43fc098b..8672bf4d 100644 --- a/examples/MutableMap/MutableMapTrait.dfy +++ b/examples/MutableMap/MutableMapTrait.dfy @@ -49,7 +49,7 @@ module {:options "-functionSyntax:4"} MutableMapTrait { requires this.HasKey(k) ensures v in this.content().Values ensures this.content()[k] == v - + function SelectOpt(k: K): (o: Option) reads this ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) @@ -60,7 +60,7 @@ module {:options "-functionSyntax:4"} MutableMapTrait { else None } - + method Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 68b4f743..b27ab257 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -8,13 +8,13 @@ include "../../examples/Mutablemap/MutableMapTrait.dfy" /** - * Implements mutable maps by interfacing with external code, e.g. - * "MutableMap.java". + * Implements mutable maps by interfacing with external code, e.g. "MutableMap.java". */ + module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { import opened MutableMapTrait - class {:extern "MutableMap"} MutableMap extends MutableMapTrait { + class {:extern} MutableMap extends MutableMapTrait { constructor {:extern} () ensures this.content() == map[] diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 7fd448bd..0d9ac4ae 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -13,6 +13,7 @@ import java.util.concurrent.*; import java.util.ArrayList; import java.util.Map; +import java.math.BigInteger; public class MutableMap { private ConcurrentHashMap m; @@ -61,7 +62,7 @@ public void Remove(K k) { m.remove(k); } - public int Size() { - return m.size(); + public BigInteger Size() { + return BigInteger.valueOf(m.size()); } } \ No newline at end of file From e1bd53a51b413d9e9932234e25f344eaaa893903 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 19:39:46 +0000 Subject: [PATCH 32/41] externbase --- examples/MutableMap/MutableMapExamples.dfy | 4 ++-- examples/MutableMap/MutableMapTrait.dfy | 15 --------------- src/MutableMap/MutableMap.dfy | 13 +++++++++++++ src/MutableMap/MutableMap.java | 21 +++++++++++---------- 4 files changed, 26 insertions(+), 27 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 8bcda1c5..f4de28c7 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} MutableMapExamples { } method Main() { - var m := new MutableMap(); +/* var m := new MutableMap(); AssertAndExpect(m.Keys() == {}); AssertAndExpect(m.Values() == {}); AssertAndExpect(m.Items() == {}); @@ -61,6 +61,6 @@ module {:options "-functionSyntax:4"} MutableMapExamples { //AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); AssertAndExpect(m.Keys() == {"testkey2"}); AssertAndExpect(m.Values() == {"testvalue2"}); - AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); + AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); */ } } \ No newline at end of file diff --git a/examples/MutableMap/MutableMapTrait.dfy b/examples/MutableMap/MutableMapTrait.dfy index 8672bf4d..80d47a31 100644 --- a/examples/MutableMap/MutableMapTrait.dfy +++ b/examples/MutableMap/MutableMapTrait.dfy @@ -5,8 +5,6 @@ // RUN: %verify "%s" -include "../../src/Wrappers.dfy" - /** * Specifications that should be satisfied by any implementation of mutable maps. * Possible instantiations are given in "MutableMapDafny.dfy" (not meant for usage, @@ -15,8 +13,6 @@ include "../../src/Wrappers.dfy" * MutableMap.java"). */ module {:options "-functionSyntax:4"} MutableMapTrait { - import opened Wrappers - trait {:termination false} MutableMapTrait { function content(): map reads this @@ -49,17 +45,6 @@ module {:options "-functionSyntax:4"} MutableMapTrait { requires this.HasKey(k) ensures v in this.content().Values ensures this.content()[k] == v - - function SelectOpt(k: K): (o: Option) - reads this - ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) - ensures o.None? ==> !this.HasKey(k) - { - if this.HasKey(k) then - Some(this.Select(k)) - else - None - } method Remove(k: K) modifies this diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index b27ab257..fb6780c5 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -6,6 +6,7 @@ // RUN: %verify "%s" include "../../examples/Mutablemap/MutableMapTrait.dfy" +include "../../src/Wrappers.dfy" /** * Implements mutable maps by interfacing with external code, e.g. "MutableMap.java". @@ -13,6 +14,7 @@ include "../../examples/Mutablemap/MutableMapTrait.dfy" module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { import opened MutableMapTrait + import opened Wrappers class {:extern} MutableMap extends MutableMapTrait { constructor {:extern} () @@ -50,6 +52,17 @@ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { ensures v in this.content().Values ensures this.content()[k] == v + function SelectOpt(k: K): (o: Option) + reads this + ensures o.Some? ==> (this.HasKey(k) && o.value in this.content().Values && this.content()[k] == o.value) + ensures o.None? ==> !this.HasKey(k) + { + if this.HasKey(k) then + Some(this.Select(k)) + else + None + } + method {:extern} Remove(k: K) modifies this ensures this.content() == old(this.content()) - {k} diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 0d9ac4ae..cedc3004 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -15,37 +15,35 @@ import java.util.Map; import java.math.BigInteger; -public class MutableMap { +public class MutableMap extends _ExternBase_MutableMap { private ConcurrentHashMap m; - public DafnyMap Content() { + @Override + public DafnyMap content() { return new DafnyMap(m); } - public MutableMap() { - m = new ConcurrentHashMap(); - } - - public MutableMap(TypeDescriptor x, TypeDescriptor y) { - m = new ConcurrentHashMap(); - } - + @Override public void Put(K k, V v) { m.put(k, v); } + @Override public DafnySet Keys() { return new DafnySet(m.keySet()); } + @Override public boolean HasKey(K k) { return m.containsKey(k); } + @Override public DafnySet Values() { return new DafnySet(m.values()); } + @Override public DafnySet> Items() { ArrayList> list = new ArrayList>(); for (Map.Entry entry : m.entrySet()) { @@ -54,14 +52,17 @@ public DafnySet> Items() { return new DafnySet>(list); } + @Override public V Select(K k) { return m.get(k); } + @Override public void Remove(K k) { m.remove(k); } + @Override public BigInteger Size() { return BigInteger.valueOf(m.size()); } From 53475a65da8819d493fb678aff09a570e857f011 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 23 Feb 2023 11:46:03 -0800 Subject: [PATCH 33/41] Missing thunk constructor (added by compiler in supertype) --- src/MutableMap/MutableMap.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index cedc3004..6b4b1300 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -18,6 +18,10 @@ public class MutableMap extends _ExternBase_MutableMap { private ConcurrentHashMap m; + public MutableMap(dafny.TypeDescriptor _td_K, dafny.TypeDescriptor _td_V) { + super(_td_K, _td_V); + } + @Override public DafnyMap content() { return new DafnyMap(m); From 0255b9a1f49e77a8cb7939554a462e414649c40e Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 23 Feb 2023 19:54:13 +0000 Subject: [PATCH 34/41] fix all --- examples/MutableMap/MutableMapExamples.dfy | 8 ++++---- src/MutableMap/MutableMap.java | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index f4de28c7..11c45831 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} MutableMapExamples { } method Main() { -/* var m := new MutableMap(); + var m := new MutableMap(); AssertAndExpect(m.Keys() == {}); AssertAndExpect(m.Values() == {}); AssertAndExpect(m.Items() == {}); @@ -57,10 +57,10 @@ module {:options "-functionSyntax:4"} MutableMapExamples { print m.Select("testkey2"), "\n"; m.Remove("testkey"); - //AssertAndExpect(m.SelectOpt("testkey").None?); - //AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); + AssertAndExpect(m.SelectOpt("testkey").None?); + AssertAndExpect(m.SelectOpt("testkey2").Some? && m.SelectOpt("testkey2").value == "testvalue2"); AssertAndExpect(m.Keys() == {"testkey2"}); AssertAndExpect(m.Values() == {"testvalue2"}); - AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); */ + AssertAndExpect(m.Items() == {("testkey2", "testvalue2")}); } } \ No newline at end of file diff --git a/src/MutableMap/MutableMap.java b/src/MutableMap/MutableMap.java index 6b4b1300..afd8325a 100644 --- a/src/MutableMap/MutableMap.java +++ b/src/MutableMap/MutableMap.java @@ -20,6 +20,7 @@ public class MutableMap extends _ExternBase_MutableMap { public MutableMap(dafny.TypeDescriptor _td_K, dafny.TypeDescriptor _td_V) { super(_td_K, _td_V); + m = new ConcurrentHashMap(); } @Override From 4b6af12767e0f5ef3ba4e43c69505cdb1cb3ae40 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 13:04:34 +0000 Subject: [PATCH 35/41] run command --- examples/MutableMap/MutableMapExamples.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 11c45831..7ac7843e 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run -t:java "%s" --input ../../src/MutableMap/MutableMap.java +// RUN: %run -target:java "%s" --input "%S/../../src/MutableMap/MutableMap.java" include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" From dd3f0396b1d9304edfe6944cec09527705252942 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 13:15:36 +0000 Subject: [PATCH 36/41] run command --- examples/MutableMap/MutableMapExamples.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 7ac7843e..e0910879 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run -target:java "%s" --input "%S/../../src/MutableMap/MutableMap.java" +// RUN: %run --target:java "%s" --input ../../src/MutableMap/MutableMap.java include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" From 8b367a19fc32fd241c1cd89e882fa35c73e97949 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 17:13:55 +0000 Subject: [PATCH 37/41] run command test --- examples/MutableMap/MutableMapExamples.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index e0910879..fef1b771 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run --target:java "%s" --input ../../src/MutableMap/MutableMap.java +// RUN: %run --target:java "%s" --input ../../src/MutableMap/MutableMap.java MutableMapTrait.dfy include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" From 9a6c0e9f066092f46002502c2f84a86aceeb6f65 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 17:20:06 +0000 Subject: [PATCH 38/41] run command --- examples/MutableMap/MutableMapExamples.dfy | 2 +- src/MutableMap/MutableMap.dfy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index fef1b771..955cd394 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run --target:java "%s" --input ../../src/MutableMap/MutableMap.java MutableMapTrait.dfy +// RUN: %run --no-verify --target:java "%s" --input /../../src/MutableMap/MutableMap.java include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index fb6780c5..a2601d88 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,7 +5,7 @@ // RUN: %verify "%s" -include "../../examples/Mutablemap/MutableMapTrait.dfy" +include "../../examples/MutableMap/MutableMapTrait.dfy" include "../../src/Wrappers.dfy" /** From 3971c056e556f4cc041b07b6c75605cad68bf6f7 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 17:21:11 +0000 Subject: [PATCH 39/41] run command --- examples/MutableMap/MutableMapExamples.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index 955cd394..e466ef87 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run --no-verify --target:java "%s" --input /../../src/MutableMap/MutableMap.java +// RUN: %run --target:java "%s" --input /../../src/MutableMap/MutableMap.java include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" From e27af4d60c805440b73ec8913ff7ea66c3a20757 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 18:56:26 +0000 Subject: [PATCH 40/41] rename module, run command --- examples/MutableMap/MutableMapExamples.dfy | 4 ++-- src/MutableMap/MutableMap.dfy | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/MutableMap/MutableMapExamples.dfy b/examples/MutableMap/MutableMapExamples.dfy index e466ef87..8b646834 100644 --- a/examples/MutableMap/MutableMapExamples.dfy +++ b/examples/MutableMap/MutableMapExamples.dfy @@ -3,7 +3,7 @@ * SPDX-License-Identifier: MIT *******************************************************************************/ -// RUN: %run --target:java "%s" --input /../../src/MutableMap/MutableMap.java +// RUN: %run --target:java "%s" --input "%S/../../src/MutableMap/MutableMap.java" include "../../src/MutableMap/MutableMap.dfy" include "../../src/Wrappers.dfy" @@ -12,7 +12,7 @@ include "../../src/Wrappers.dfy" * Tests the Java interfacing implementation of mutable maps. */ module {:options "-functionSyntax:4"} MutableMapExamples { - import opened MutableMap + import opened DafnyLibraries import opened Wrappers method AssertAndExpect(p: bool, maybeMsg: Option := None) requires p { diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index a2601d88..16720780 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -12,7 +12,7 @@ include "../../src/Wrappers.dfy" * Implements mutable maps by interfacing with external code, e.g. "MutableMap.java". */ -module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap { +module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries { import opened MutableMapTrait import opened Wrappers From 56f493f8fdf6ca64a143a7e3e7260ece2c1f3c56 Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Fri, 24 Feb 2023 19:12:35 +0000 Subject: [PATCH 41/41] addressing #2500 --- examples/MutableMap/MutableMapDafny.dfy | 50 +++++++++++++++++++++++-- src/MutableMap/MutableMap.dfy | 49 +++++++++++++++++++++++- 2 files changed, 93 insertions(+), 6 deletions(-) diff --git a/examples/MutableMap/MutableMapDafny.dfy b/examples/MutableMap/MutableMapDafny.dfy index 8739184e..9bf9dbcb 100644 --- a/examples/MutableMap/MutableMapDafny.dfy +++ b/examples/MutableMap/MutableMapDafny.dfy @@ -4,16 +4,58 @@ *******************************************************************************/ // RUN: %verify "%s" - -include "MutableMapTrait.dfy" /** * Implements mutable maps in Dafny to guard against inconsistent specifications. * Only exists to verify feasability; not meant for actual usage. */ module {:options "-functionSyntax:4"} MutableMapDafny { - import opened MutableMapTrait - + /** + * NOTE: Only here because of #2500; once resolved import "MutableMapTrait.dfy". + */ + trait {:termination false} MutableMapTrait { + function content(): map + reads this + + method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} + + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + + function Values(): (values: set) + reads this + ensures values == this.content().Values + + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + + function Select(k: K): (v: V) + reads this + requires this.HasKey(k) + ensures v in this.content().Values + ensures this.content()[k] == v + + method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + + function Size(): (size: int) + reads this + ensures size == |this.content().Items| + } + class MutableMapDafny extends MutableMapTrait { var m: map diff --git a/src/MutableMap/MutableMap.dfy b/src/MutableMap/MutableMap.dfy index 16720780..b0001440 100644 --- a/src/MutableMap/MutableMap.dfy +++ b/src/MutableMap/MutableMap.dfy @@ -5,7 +5,6 @@ // RUN: %verify "%s" -include "../../examples/MutableMap/MutableMapTrait.dfy" include "../../src/Wrappers.dfy" /** @@ -13,9 +12,55 @@ include "../../src/Wrappers.dfy" */ module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} DafnyLibraries { - import opened MutableMapTrait import opened Wrappers + /** + * NOTE: Only here because of #2500; once resolved import "../../examples/MutableMap/ + * MutableMapTrait.dfy". + */ + trait {:termination false} MutableMapTrait { + function content(): map + reads this + + method Put(k: K, v: V) + modifies this + ensures this.content() == old(this.content())[k := v] + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + {v} + ensures k !in old(this.content()).Keys ==> this.content().Values == old(this.content()).Values + {v} + + function Keys(): (keys: set) + reads this + ensures keys == this.content().Keys + + predicate HasKey(k: K) + reads this + ensures HasKey(k) <==> k in this.content().Keys + + function Values(): (values: set) + reads this + ensures values == this.content().Values + + function Items(): (items: set<(K,V)>) + reads this + ensures items == this.content().Items + ensures items == set k | k in this.content().Keys :: (k, this.content()[k]) + + function Select(k: K): (v: V) + reads this + requires this.HasKey(k) + ensures v in this.content().Values + ensures this.content()[k] == v + + method Remove(k: K) + modifies this + ensures this.content() == old(this.content()) - {k} + ensures k in old(this.content()).Keys ==> this.content().Values + {old(this.content())[k]} == old(this.content()).Values + + function Size(): (size: int) + reads this + ensures size == |this.content().Items| + } + class {:extern} MutableMap extends MutableMapTrait { constructor {:extern} () ensures this.content() == map[]