Mutable maps via Java extern

examples/MutableMap/MutableMapExamples.dfy

@@ -0,0 +1,45 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %dafny /compile:0 "%s"
+
+include "../../src/MutableMap/MutableMap.dfy"
+
+module {:options "-functionSyntax:4"} MutableMapExamples {
+  import opened MutableMap
+
+  method Main() {
+    var m := new MutableMap<string,string>();
+    assert m.Keys() == {};
+    assert m.Values() == {};
+    assert m.Items() == {};
+    assert 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;
+    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 "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")};
+  }
+}

src/MutableMap/MutableMap.dfy

@@ -0,0 +1,56 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+
+// RUN: %dafny /compile:0 "%s"
+
+include "MutableMapTrait.dfy"
+
+module {:extern "DafnyLibraries"} {:options "-functionSyntax:4"} MutableMap refines MutableMapTrait {
+  class {:extern} MutableMap<K(==),V(==)> extends MutableMapTrait<K,V> {
+    constructor {:extern} ()
+      ensures this.content() == map[]
+
+    function {:extern} content(): map<K, V>
+      reads this
+
+    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<K>)
+      reads this
+      ensures keys == this.content().Keys
+
+    predicate {:extern} HasKey(k: K)
+      reads this
+      ensures HasKey(k) <==> k in this.content().Keys
+
+    function {:extern} Values(): (values: set<V>)
+      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} Select(k: K): (v: V)
+      reads this
+      requires this.HasKey(k)
+      ensures v in this.content().Values
+      ensures this.content()[k] == v
+
+    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
+      ensures size == |this.content().Items|
+  }
+}

src/MutableMap/MutableMap.java

@@ -0,0 +1,67 @@
+/*******************************************************************************
+*  Copyright by the contributors to the Dafny Project
+*  SPDX-License-Identifier: MIT
+*******************************************************************************/
+package DafnyLibraries;
+
+import dafny.DafnySet;
+import dafny.DafnyMap;
+import dafny.Tuple2;
+import dafny.TypeDescriptor;
+import dafny.Helpers;
+
+import java.util.concurrent.*;
+import java.util.ArrayList;
+import java.util.Map;
+
+public class MutableMap<K,V> {
+  private ConcurrentHashMap<K,V> m;
+
+  public DafnyMap<K,V> Content() {
+    return new DafnyMap<K,V>(m);
+  }
+
+  public MutableMap() {
+    m = new ConcurrentHashMap<K,V>();
+  }
+
+  public MutableMap(TypeDescriptor<K> x, TypeDescriptor<V> y) {
+    m = new ConcurrentHashMap<K,V>();
+  }
+
+  public void Put(K k, V v) {
+    m.put(k, v);
+  }
+
+  public DafnySet<? extends K> Keys() {
+    return new DafnySet(m.keySet());
+  }
+
+  public boolean HasKey(K k) {
+    return m.containsKey(k);
+  }
+
+  public DafnySet<? extends V> Values() {
+    return new DafnySet(m.values());
+  }
+
+  public DafnySet<? extends Tuple2<K,V>> Items() {
+    ArrayList<Tuple2<K, V>> list = new ArrayList<Tuple2<K, V>>();
+    for (Map.Entry<K, V> entry : m.entrySet()) {
+      list.add(new Tuple2<K, V>(entry.getKey(), entry.getValue()));
+    }
+    return new DafnySet<Tuple2<K, V>>(list);
+  }
+
+  public V Select(K k) {
+    return m.get(k);
+  }
+
+  public void Remove(K k) {
+    m.remove(k);
+  }
+
+  public int Size() {
+    return m.size();
+  }
+}

src/MutableMap/MutableMapDafny.dfy

@@ -0,0 +1,125 @@
+/*******************************************************************************
+*  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<K(==),V(==)> extends MutableMapTrait<K,V> {
+    var m: map<K,V>
+
+    function content(): map<K, V> 
+      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<K>)
+      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<V>)
+      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|
+    }
+  }
+}

src/MutableMap/MutableMapTrait.dfy

@@ -0,0 +1,66 @@
+/*******************************************************************************
+*  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 {:termination false} MutableMapTrait<K(==),V(==)> {
+    function content(): map<K, V>
+      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<K>)
+      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<V>)
+      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<V>)
+      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}
+      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|
+  }
+}

src/MutableMap/README.md

@@ -0,0 +1,20 @@
+# 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 the `MutableMapExamples.dfy` file in the `examples/MutableMap` directory that depends on the `MutableMap` module, run the following.
+
+```bash
+# Java
+$ dafny run MutableMapExamples.dfy --target:java --input ../../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.