diff options
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 59 | ||||
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 69 |
2 files changed, 128 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index b3fc7e24..09b6efcf 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -358,6 +358,49 @@ axiom (forall<T> s: Seq T, v: T, n: int :: 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
// ---------------------------------------------------------------
+// -- Axiomatization of Maps -------------------------------------
+// ---------------------------------------------------------------
+
+type Map U V;
+
+function Map#Domain<U, V>(Map U V): [U] bool;
+function Map#Elements<U, V>(Map U V): [U]V;
+
+function Map#Empty<U, V>(): Map U V;
+axiom (forall<U, V> u: U ::
+ { Map#Domain(Map#Empty(): Map U V)[u] }
+ !Map#Domain(Map#Empty(): Map U V)[u]);
+
+//Build is used in displays, and for map updates
+function Map#Build<U, V>(Map U V, U, V): Map U V;
+/*axiom (forall<U, V> m: Map U V, u: U, v: V ::
+ { Map#Domain(Map#Build(m, u, v))[u] } { Map#Elements(Map#Build(m, u, v))[u] }
+ Map#Domain(Map#Build(m, u, v))[u] && Map#Elements(Map#Build(m, u, v))[u] == v);*/
+
+axiom (forall<U, V> m: Map U V, u: U, u': U, v: V ::
+ { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Elements(Map#Build(m, u, v))[u'] }
+ (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] &&
+ Map#Elements(Map#Build(m, u, v))[u'] == v) &&
+ (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] &&
+ Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u']));
+
+//equality for maps
+function Map#Equal<U, V>(Map U V, Map U V): bool;
+axiom (forall<U, V> m: Map U V, m': Map U V::
+ { Map#Equal(m, m') }
+ Map#Equal(m, m') <==> (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) &&
+ (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]));
+// extensionality
+axiom (forall<U, V> m: Map U V, m': Map U V::
+ { Map#Equal(m, m') }
+ Map#Equal(m, m') ==> m == m');
+
+function Map#Disjoint<U, V>(Map U V, Map U V): bool;
+axiom (forall<U, V> m: Map U V, m': Map U V ::
+ { Map#Disjoint(m, m') }
+ Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));
+
+// ---------------------------------------------------------------
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
@@ -371,6 +414,7 @@ axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b); axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);
axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
+axiom (forall b: BoxType :: { $Unbox(b): Map BoxType BoxType } $Box($Unbox(b): Map BoxType BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);
// Note: an axiom like this for bool would not be sound; instead, we do:
function $IsCanonicalBoolBox(BoxType): bool;
@@ -470,11 +514,26 @@ axiom (forall b: BoxType, h: HeapType :: { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }
GenericAlloc(b, h) ==>
$Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);
+//seqs
axiom (forall b: BoxType, h: HeapType, i: int ::
{ GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) }
GenericAlloc(b, h) &&
0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==>
GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) );
+
+//maps
+//seq-like axiom, talking about the range elements
+axiom (forall b: BoxType, h: HeapType, i: BoxType ::
+ { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[i] }
+ GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[i] ==>
+ GenericAlloc( Map#Elements($Unbox(b): Map BoxType BoxType)[i], h ) );
+//set-like axiom, talking about the domain elements
+axiom (forall b: BoxType, h: HeapType, t: BoxType ::
+ { GenericAlloc(b, h), Map#Domain($Unbox(b): Map BoxType BoxType)[t] }
+ GenericAlloc(b, h) && Map#Domain($Unbox(b): Map BoxType BoxType)[t] ==>
+ GenericAlloc(t, h));
+
+//sets
axiom (forall b: BoxType, h: HeapType, t: BoxType ::
{ GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }
GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 2f8d2764..67669245 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -275,6 +275,75 @@ namespace Dafny return new MultiSet<T>(r);
}
}
+
+ public class Map<U, V>
+ {
+ Dictionary<U, V> dict;
+ public Map() { }
+ Map(Dictionary<U, V> d) {
+ dict = d;
+ }
+ public static Map<U, V> Empty {
+ get {
+ return new Map<U, V>(new Dictionary<U,V>());
+ }
+ }
+ public static Map<U, V> FromElements(params Pair<U,V>[] values) {
+ Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+ foreach (Pair<U,V> p in values) {
+ d[p.Car] = p.Cdr;
+ }
+ return new Map<U, V>(d);
+ }
+ public bool Equals(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ V v1, v2;
+ if (!dict.TryGetValue(u, out v1)) {
+ return false; // this shouldn't happen
+ }
+ if (!other.dict.TryGetValue(u, out v2)) {
+ return false; // other dictionary does not contain this element
+ }
+ if (!v1.Equals(v2)) {
+ return false;
+ }
+ }
+ foreach (U u in other.dict.Keys) {
+ if (!dict.ContainsKey(u)) {
+ return false; // this shouldn't happen
+ }
+ }
+ return true;
+ }
+ public override bool Equals(object other) {
+ return other is Map<U, V> && Equals((Map<U, V>)other);
+ }
+ public override int GetHashCode() {
+ return dict.GetHashCode();
+ }
+ public bool IsDisjointFrom(Map<U, V> other) {
+ foreach (U u in dict.Keys) {
+ if (other.dict.ContainsKey(u))
+ return false;
+ }
+ foreach (U u in other.dict.Keys) {
+ if (dict.ContainsKey(u))
+ return false;
+ }
+ return true;
+ }
+ public bool Contains(U u) {
+ return dict.ContainsKey(u);
+ }
+ public V Select(U index) {
+ return dict[index];
+ }
+ public Map<U, V> Update(U index, V val) {
+ Dictionary<U, V> d = new Dictionary<U, V>(dict);
+ d[index] = val;
+ return new Map<U, V>(d);
+ }
+ }
public class Sequence<T>
{
T[] elmts;
|