Dafny: Boogie error messages are appeared

Oct 7, 2012 at 6:43 PM
Edited Oct 7, 2012 at 6:44 PM

Dafny 2.2.40819.0703 says for the program

 

function domain<U, V>(m : map<U, V>) : set<U>
ensures forall i :: i in domain(m) <==> i in m;
{
set x | x in m
}

ghost method Lemma(m : map<int, int>, m2 : map<int, int>)
requires (forall x :: x in m2
==> x in m ) ;
ensures domain(m2) <= domain(m) ;
{
}

 

 

 

Dafny program verifier version 2.2.40819.0703, Copyright (c) 2003-2012, Microsof
t.
(0,-1): Error: invalid argument types (Map BoxType BoxType and ref) to binary op
erator ==
(0,-1): Error: invalid argument types (Map BoxType BoxType and ref) to binary op
erator !=
(0,-1): Error: invalid argument types (Map BoxType BoxType and ref) to binary op
erator !=
(0,-1): Error: invalid argument types (Map BoxType BoxType and ref) to binary op
erator ==
(0,-1): Error: invalid argument types (Map BoxType BoxType and ref) to binary op
erator !=
5 type checking errors detected in C:\Users\user_2\Local\AppData\Temp\md.bpl

*** Encountered internal translation error - re-running Boogie to get better deb
ug information

C:\Users\user_2\Local\AppData\Temp\md.bpl(595,202): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator ==
C:\Users\user_2\Local\AppData\Temp\md.bpl(595,217): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator !=
C:\Users\user_2\Local\AppData\Temp\md.bpl(595,241): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator !=
C:\Users\user_2\Local\AppData\Temp\md.bpl(595,258): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator !=
C:\Users\user_2\Local\AppData\Temp\md.bpl(595,281): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator ==
C:\Users\user_2\Local\AppData\Temp\md.bpl(595,297): Error: invalid argument type
s (Map BoxType BoxType and ref) to binary operator !=
6 type checking errors detected in C:\Users\user_2\Local\AppData\Temp\md.bpl

 

Oct 7, 2012 at 6:45 PM

 

// Dafny program verifier version 2.2.40819.0703, Copyright (c) 2003-2012, Microsoft.
// Command Line Options: Desktop\md.dfy

const $$Language$Dafny: bool;

axiom $$Language$Dafny;

type ref;

const null: ref;

type Set T = [T]bool;

function Set#Empty<T>() : Set T;

axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);

function Set#Singleton<T>(T) : Set T;

axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);

axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);

function Set#UnionOne<T>(Set T, T) : Set T;

axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a, x)[o] } Set#UnionOne(a, x)[o] <==> o == x || a[o]);

axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]);

axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } a[y] ==> Set#UnionOne(a, x)[y]);

function Set#Union<T>(Set T, Set T) : Set T;

axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a, b)[o] } Set#Union(a, b)[o] <==> a[o] || b[o]);

axiom (forall<T> a: Set T, b: Set T, y: T :: { Set#Union(a, b), a[y] } a[y] ==> Set#Union(a, b)[y]);

axiom (forall<T> a: Set T, b: Set T, y: T :: { Set#Union(a, b), b[y] } b[y] ==> Set#Union(a, b)[y]);

axiom (forall<T> a: Set T, b: Set T :: { Set#Union(a, b) } Set#Disjoint(a, b) ==> Set#Difference(Set#Union(a, b), a) == b && Set#Difference(Set#Union(a, b), b) == a);

function Set#Intersection<T>(Set T, Set T) : Set T;

axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a, b)[o] } Set#Intersection(a, b)[o] <==> a[o] && b[o]);

axiom (forall<T> a: Set T, b: Set T :: { Set#Union(Set#Union(a, b), b) } Set#Union(Set#Union(a, b), b) == Set#Union(a, b));

axiom (forall<T> a: Set T, b: Set T :: { Set#Union(a, Set#Union(a, b)) } Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));

axiom (forall<T> a: Set T, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) } Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));

axiom (forall<T> a: Set T, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) } Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

function Set#Difference<T>(Set T, Set T) : Set T;

axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a, b)[o] } Set#Difference(a, b)[o] <==> a[o] && !b[o]);

axiom (forall<T> a: Set T, b: Set T, y: T :: { Set#Difference(a, b), b[y] } b[y] ==> !Set#Difference(a, b)[y]);

function Set#Subset<T>(Set T, Set T) : bool;

axiom (forall<T> a: Set T, b: Set T :: { Set#Subset(a, b) } Set#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] ==> b[o]));

function Set#Equal<T>(Set T, Set T) : bool;

axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <==> b[o]));

axiom (forall<T> a: Set T, b: Set T :: { Set#Equal(a, b) } Set#Equal(a, b) ==> a == b);

function Set#Disjoint<T>(Set T, Set T) : bool;

axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a, b) } Set#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } !a[o] || !b[o]));

function Set#Choose<T>(Set T, TickType) : T;

axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) } a != Set#Empty() ==> a[Set#Choose(a, tick)]);

function Math#min(a: int, b: int) : int;

axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a);

axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b);

axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b);

function Math#clip(a: int) : int;

axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a);

axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0);

type MultiSet T = [T]int;

function $IsGoodMultiSet<T>(ms: MultiSet T) : bool;

axiom (forall<T> ms: MultiSet T :: { $IsGoodMultiSet(ms) } $IsGoodMultiSet(ms) <==> (forall o: T :: { ms[o] } 0 <= ms[o]));

function MultiSet#Empty<T>() : MultiSet T;

axiom (forall<T> o: T :: { MultiSet#Empty()[o] } MultiSet#Empty()[o] == 0);

function MultiSet#Singleton<T>(T) : MultiSet T;

axiom (forall<T> r: T, o: T :: { MultiSet#Singleton(r)[o] } (MultiSet#Singleton(r)[o] == 1 <==> r == o) && (MultiSet#Singleton(r)[o] == 0 <==> r != o));

axiom (forall<T> r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r));

function MultiSet#UnionOne<T>(MultiSet T, T) : MultiSet T;

axiom (forall<T> a: MultiSet T, x: T, o: T :: { MultiSet#UnionOne(a, x)[o] } 0 < MultiSet#UnionOne(a, x)[o] <==> o == x || 0 < a[o]);

axiom (forall<T> a: MultiSet T, x: T :: { MultiSet#UnionOne(a, x) } MultiSet#UnionOne(a, x)[x] == a[x] + 1);

axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] } 0 < a[y] ==> 0 < MultiSet#UnionOne(a, x)[y]);

axiom (forall<T> a: MultiSet T, x: T, y: T :: { MultiSet#UnionOne(a, x), a[y] } x != y ==> a[y] == MultiSet#UnionOne(a, x)[y]);

function MultiSet#Union<T>(MultiSet T, MultiSet T) : MultiSet T;

axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a, b)[o] } MultiSet#Union(a, b)[o] == a[o] + b[o]);

axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] } 0 < a[y] ==> 0 < MultiSet#Union(a, b)[y]);

axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] } 0 < b[y] ==> 0 < MultiSet#Union(a, b)[y]);

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Union(a, b) } MultiSet#Difference(MultiSet#Union(a, b), a) == b && MultiSet#Difference(MultiSet#Union(a, b), b) == a);

function MultiSet#Intersection<T>(MultiSet T, MultiSet T) : MultiSet T;

axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a, b)[o] } MultiSet#Intersection(a, b)[o] == Math#min(a[o], b[o]));

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b));

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b));

function MultiSet#Difference<T>(MultiSet T, MultiSet T) : MultiSet T;

axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Difference(a, b)[o] } MultiSet#Difference(a, b)[o] == Math#clip(a[o] - b[o]));

axiom (forall<T> a: MultiSet T, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), b[y], a[y] } a[y] <= b[y] ==> MultiSet#Difference(a, b)[y] == 0);

function MultiSet#Subset<T>(MultiSet T, MultiSet T) : bool;

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a, b) } MultiSet#Subset(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] <= b[o]));

function MultiSet#Equal<T>(MultiSet T, MultiSet T) : bool;

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a, b) } MultiSet#Equal(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == b[o]));

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a, b) } MultiSet#Equal(a, b) ==> a == b);

function MultiSet#Disjoint<T>(MultiSet T, MultiSet T) : bool;

axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a, b) } MultiSet#Disjoint(a, b) <==> (forall o: T :: { a[o] } { b[o] } a[o] == 0 || b[o] == 0));

function MultiSet#FromSet<T>(Set T) : MultiSet T;

axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] } (MultiSet#FromSet(s)[a] == 0 <==> !s[a]) && (MultiSet#FromSet(s)[a] == 1 <==> s[a]));

function MultiSet#FromSeq<T>(Seq T) : MultiSet T;

axiom (forall<T> s: Seq T :: { MultiSet#FromSeq(s) } $IsGoodMultiSet(MultiSet#FromSeq(s)));

axiom (forall<T> s: Seq T, v: T :: { MultiSet#FromSeq(Seq#Build(s, v)) } MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v));

axiom (forall<T> :: MultiSet#FromSeq(Seq#Empty(): Seq T) == MultiSet#Empty(): MultiSet T);

axiom (forall<T> a: Seq T, b: Seq T :: { MultiSet#FromSeq(Seq#Append(a, b)) } MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)));

axiom (forall<T> s: Seq T, i: int, v: T, x: T :: { MultiSet#FromSeq(Seq#Update(s, i, v))[x] } 0 <= i && i < Seq#Length(s) ==> MultiSet#FromSeq(Seq#Update(s, i, v))[x] == MultiSet#Union(MultiSet#Difference(MultiSet#FromSeq(s), MultiSet#Singleton(Seq#Index(s, i))), MultiSet#Singleton(v))[x]);

axiom (forall<T> s: Seq T, x: T :: { MultiSet#FromSeq(s)[x] } (exists i: int :: { Seq#Index(s, i) } 0 <= i && i < Seq#Length(s) && x == Seq#Index(s, i)) <==> 0 < MultiSet#FromSeq(s)[x]);

type Seq _;

function Seq#Length<T>(Seq T) : int;

axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));

function Seq#Empty<T>() : Seq T;

axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);

axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

function Seq#Singleton<T>(T) : Seq T;

axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);

function Seq#Build<T>(s: Seq T, val: T) : Seq T;

axiom (forall<T> s: Seq T, v: T :: { Seq#Length(Seq#Build(s, v)) } Seq#Length(Seq#Build(s, v)) == 1 + Seq#Length(s));

axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s, v), i) } (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == v) && (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s, v), i) == Seq#Index(s, i)));

function Seq#Append<T>(Seq T, Seq T) : Seq T;

axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0, s1)) } Seq#Length(Seq#Append(s0, s1)) == Seq#Length(s0) + Seq#Length(s1));

function Seq#Index<T>(Seq T, int) : T;

axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);

axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0, s1), n) } (n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s0, n)) && (Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0, s1), n) == Seq#Index(s1, n - Seq#Length(s0))));

function Seq#Update<T>(Seq T, int, T) : Seq T;

axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s, i, v)) } 0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s, i, v)) == Seq#Length(s));

axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s, i, v), n) } 0 <= n && n < Seq#Length(s) ==> (i == n ==> Seq#Index(Seq#Update(s, i, v), n) == v) && (i != n ==> Seq#Index(Seq#Update(s, i, v), n) == Seq#Index(s, n)));

function Seq#Contains<T>(Seq T, T) : bool;

axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s, x) } Seq#Contains(s, x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

axiom (forall x: ref :: { Seq#Contains(Seq#Empty(), x) } !Seq#Contains(Seq#Empty(), x));

axiom (forall<T> s0: Seq T, s1: Seq T, x: T :: { Seq#Contains(Seq#Append(s0, s1), x) } Seq#Contains(Seq#Append(s0, s1), x) <==> Seq#Contains(s0, x) || Seq#Contains(s1, x));

axiom (forall<T> s: Seq T, v: T, x: T :: { Seq#Contains(Seq#Build(s, v), x) } Seq#Contains(Seq#Build(s, v), x) <==> v == x || Seq#Contains(s, x));

axiom (forall<T> s: Seq T, n: int, x: T :: { Seq#Contains(Seq#Take(s, n), x) } Seq#Contains(Seq#Take(s, n), x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= i && i < n && i < Seq#Length(s) && Seq#Index(s, i) == x));

axiom (forall<T> s: Seq T, n: int, x: T :: { Seq#Contains(Seq#Drop(s, n), x) } Seq#Contains(Seq#Drop(s, n), x) <==> (exists i: int :: { Seq#Index(s, i) } 0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));

function Seq#Equal<T>(Seq T, Seq T) : bool;

axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0, s1) } Seq#Equal(s0, s1) <==> Seq#Length(s0) == Seq#Length(s1) && (forall j: int :: { Seq#Index(s0, j) } { Seq#Index(s1, j) } 0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0, j) == Seq#Index(s1, j)));

axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a, b) } Seq#Equal(a, b) ==> a == b);

function Seq#SameUntil<T>(Seq T, Seq T, int) : bool;

axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0, s1, n) } Seq#SameUntil(s0, s1, n) <==> (forall j: int :: { Seq#Index(s0, j) } { Seq#Index(s1, j) } 0 <= j && j < n ==> Seq#Index(s0, j) == Seq#Index(s1, j)));

function Seq#Take<T>(s: Seq T, howMany: int) : Seq T;

axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s, n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s, n)) == n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Take(s, n)) == Seq#Length(s)));

axiom (forall<T> s: Seq T, n: int, j: int :: {:weight 25} { Seq#Index(Seq#Take(s, n), j) } 0 <= j && j < n && j < Seq#Length(s) ==> Seq#Index(Seq#Take(s, n), j) == Seq#Index(s, j));

function Seq#Drop<T>(s: Seq T, howMany: int) : Seq T;

axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s, n)) } 0 <= n ==> (n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s, n)) == Seq#Length(s) - n) && (Seq#Length(s) < n ==> Seq#Length(Seq#Drop(s, n)) == 0));

axiom (forall<T> s: Seq T, n: int, j: int :: {:weight 25} { Seq#Index(Seq#Drop(s, n), j) } 0 <= n && 0 <= j && j < Seq#Length(s) - n ==> Seq#Index(Seq#Drop(s, n), j) == Seq#Index(s, j + n));

axiom (forall<T> s: Seq T, t: Seq T :: { Seq#Append(s, t) } Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s && Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);

function Seq#FromArray(h: HeapType, a: ref) : Seq BoxType;

axiom (forall h: HeapType, a: ref :: { Seq#Length(Seq#FromArray(h, a)) } Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));

axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a): Seq BoxType } (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));

axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref :: { Seq#FromArray(update(h, o, f, v), a) } o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a));

axiom (forall h: HeapType, i: int, v: BoxType, a: ref :: { Seq#FromArray(update(h, a, IndexField(i), v), a) } 0 <= i && i < _System.array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v));

axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Take(Seq#Update(s, i, v), n) } 0 <= i && i < n && n <= Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Update(Seq#Take(s, n), i, v));

axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Take(Seq#Update(s, i, v), n) } n <= i && i < Seq#Length(s) ==> Seq#Take(Seq#Update(s, i, v), n) == Seq#Take(s, n));

axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Drop(Seq#Update(s, i, v), n) } 0 <= n && n <= i && i < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Update(Seq#Drop(s, n), i - n, v));

axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Drop(Seq#Update(s, i, v), n) } 0 <= i && i < n && n < Seq#Length(s) ==> Seq#Drop(Seq#Update(s, i, v), n) == Seq#Drop(s, n));

axiom (forall h: HeapType, a: ref, n0: int, n1: int :: { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) } n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)));

axiom (forall<T> s: Seq T, v: T, n: int :: { Seq#Drop(Seq#Build(s, v), n) } 0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v));

type Map _ _;

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]);

function Map#Glue<U,V>([U]bool, [U]V) : Map U V;

axiom (forall<U,V> a: [U]bool, b: [U]V :: { Map#Domain(Map#Glue(a, b)) } Map#Domain(Map#Glue(a, b)) == a);

axiom (forall<U,V> a: [U]bool, b: [U]V :: { Map#Elements(Map#Glue(a, b)) } Map#Elements(Map#Glue(a, b)) == b);

function Map#Build<U,V>(Map U V, U, V) : Map 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']));

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]));

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]));

type BoxType;

function $Box<T>(T) : BoxType;

function $Unbox<T>(BoxType) : T;

axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

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);

function $IsCanonicalBoolBox(BoxType) : bool;

axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));

axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);

type ClassName;

const unique class._System.int: ClassName;

const unique class._System.bool: ClassName;

const unique class._System.set: ClassName;

const unique class._System.seq: ClassName;

const unique class._System.multiset: ClassName;

const unique class._System.array: ClassName;

function dtype(ref) : ClassName;

function TypeParams(ref, int) : ClassName;

function TypeTuple(a: ClassName, b: ClassName) : ClassName;

function TypeTupleCar(ClassName) : ClassName;

function TypeTupleCdr(ClassName) : ClassName;

axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a, b) } TypeTupleCar(TypeTuple(a, b)) == a && TypeTupleCdr(TypeTuple(a, b)) == b);

type DatatypeType;

function DtType(DatatypeType) : ClassName;

function DtTypeParams(DatatypeType, int) : ClassName;

type DtCtorId;

function DatatypeCtorId(DatatypeType) : DtCtorId;

function DtRank(DatatypeType) : int;

const $ModuleContextHeight: int;

const $FunctionContextHeight: int;

const $InMethodContext: bool;

type Field _;

function FDim<T>(Field T) : int;

function IndexField(int) : Field BoxType;

axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);

function IndexField_Inverse<T>(Field T) : int;

axiom (forall i: int :: { IndexField(i) } IndexField_Inverse(IndexField(i)) == i);

function MultiIndexField(Field BoxType, int) : Field BoxType;

axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f, i) } FDim(MultiIndexField(f, i)) == FDim(f) + 1);

function MultiIndexField_Inverse0<T>(Field T) : Field T;

function MultiIndexField_Inverse1<T>(Field T) : int;

axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f, i) } MultiIndexField_Inverse0(MultiIndexField(f, i)) == f && MultiIndexField_Inverse1(MultiIndexField(f, i)) == i);

function DeclType<T>(Field T) : ClassName;

type NameFamily;

function DeclName<T>(Field T) : NameFamily;

function FieldOfDecl<alpha>(ClassName, NameFamily) : Field alpha;

axiom (forall<T> cl: ClassName, nm: NameFamily :: { FieldOfDecl(cl, nm): Field T } DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);

const unique alloc: Field bool;

axiom FDim(alloc) == 0;

function DtAlloc(DatatypeType, HeapType) : bool;

axiom (forall h: HeapType, k: HeapType, d: DatatypeType :: { $HeapSucc(h, k), DtAlloc(d, h) } { $HeapSucc(h, k), DtAlloc(d, k) } $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));

function GenericAlloc(BoxType, HeapType) : bool;

axiom (forall h: HeapType, k: HeapType, d: BoxType :: { $HeapSucc(h, k), GenericAlloc(d, h) } { $HeapSucc(h, k), GenericAlloc(d, k) } $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));

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]);

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));

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));

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));

axiom (forall b: BoxType, h: HeapType, t: BoxType :: { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] } GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==> GenericAlloc(t, h));

axiom (forall b: BoxType, h: HeapType :: { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) } GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));

axiom (forall b: bool, h: HeapType :: $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));

axiom (forall x: int, h: HeapType :: $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));

axiom (forall r: ref, h: HeapType :: { GenericAlloc($Box(r), h) } $IsGoodHeap(h) && (r == null || h[r, alloc]) ==> GenericAlloc($Box(r), h));

axiom (forall r: ref, f: Field BoxType, h: HeapType :: { GenericAlloc(read(h, r, f), h) } $IsGoodHeap(h) && r != null && read(h, r, alloc) ==> GenericAlloc(read(h, r, f), h));

function _System.array.Length(a: ref) : int;

axiom (forall o: ref :: 0 <= _System.array.Length(o));

type HeapType = <alpha>[ref,Field alpha]alpha;

function {:inline true} read<alpha>(H: HeapType, r: ref, f: Field alpha) : alpha
{
H[r, f]
}

function {:inline true} update<alpha>(H: HeapType, r: ref, f: Field alpha, v: alpha) : HeapType
{
H[r, f := v]
}

function $IsGoodHeap(HeapType) : bool;

var $Heap: HeapType where $IsGoodHeap($Heap);

function $HeapSucc(HeapType, HeapType) : bool;

axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) } $IsGoodHeap(update(h, r, f, x)) ==> $HeapSucc(h, update(h, r, f, x)));

axiom (forall a: HeapType, b: HeapType, c: HeapType :: { $HeapSucc(a, b), $HeapSucc(b, c) } $HeapSucc(a, b) && $HeapSucc(b, c) ==> $HeapSucc(a, c));

axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h, k) } $HeapSucc(h, k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));

type TickType;

var $Tick: TickType;

axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y);

axiom (forall x: int, y: int :: { x % y } 0 < y ==> 0 <= x % y && x % y < y);

axiom (forall x: int, y: int :: { x % y } y < 0 ==> 0 <= x % y && x % y < 0 - y);

axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b);

const unique class._System.object: ClassName;

const unique class._module.__default: ClassName;

function _module.__default.domain($heap: HeapType, this: ref, m#0: Map BoxType BoxType) : Set BoxType;

function _module.__default.domain#limited($heap: HeapType, this: ref, m#0: Map BoxType BoxType) : Set BoxType;

function _module.__default.domain#2($heap: HeapType, this: ref, m#0: Map BoxType BoxType) : Set BoxType;

function _module.__default.domain#canCall($heap: HeapType, this: ref, m#0: Map BoxType BoxType) : bool;

axiom (forall $Heap: HeapType, this: ref, m#0: Map BoxType BoxType :: { _module.__default.domain#2($Heap, this, m#0) } _module.__default.domain#2($Heap, this, m#0) == _module.__default.domain($Heap, this, m#0));

axiom (forall $Heap: HeapType, this: ref, m#0: Map BoxType BoxType :: { _module.__default.domain($Heap, this, m#0) } _module.__default.domain($Heap, this, m#0) == _module.__default.domain#limited($Heap, this, m#0));

// definition axiom for _module.__default.domain
axiom 0 < $ModuleContextHeight || (0 == $ModuleContextHeight && (0 <= $FunctionContextHeight || $InMethodContext)) ==> (forall $Heap: HeapType, this: ref, m#0: Map BoxType BoxType :: { _module.__default.domain($Heap, this, m#0) } _module.__default.domain#canCall($Heap, this, m#0) || ((0 != $ModuleContextHeight || 0 != $FunctionContextHeight || $InMethodContext) && $IsGoodHeap($Heap) && this != null && read($Heap, this, alloc) && dtype(this) == class._module.__default && (forall $t#0: BoxType :: { Map#Domain(m#0)[$t#0] } Map#Domain(m#0)[$t#0] ==> GenericAlloc($t#0, $Heap)) && (forall $t#0: BoxType :: { Map#Elements(m#0)[$t#0] } Map#Domain(m#0)[$t#0] ==> GenericAlloc($t#0, $Heap))) ==> _module.__default.domain($Heap, this, m#0) == (lambda $y#1: BoxType :: (exists x#2: BoxType :: GenericAlloc(x#2, $Heap) && Map#Domain(m#0)[x#2] && $y#1 == x#2)) && (forall i#1: BoxType :: GenericAlloc(i#1, $Heap) ==> (_module.__default.domain#limited($Heap, this, m#0)[i#1] <==> Map#Domain(m#0)[i#1])) && (forall $t#2: BoxType :: { _module.__default.domain($Heap, this, m#0)[$t#2] } _module.__default.domain($Heap, this, m#0)[$t#2] ==> GenericAlloc($t#2, $Heap)));

// definition axiom for _module.__default.domain#2
axiom 0 < $ModuleContextHeight || (0 == $ModuleContextHeight && (0 <= $FunctionContextHeight || $InMethodContext)) ==> (forall $Heap: HeapType, this: ref, m#0: Map BoxType BoxType :: { _module.__default.domain#2($Heap, this, m#0) } _module.__default.domain#canCall($Heap, this, m#0) || ((0 != $ModuleContextHeight || 0 != $FunctionContextHeight || $InMethodContext) && $IsGoodHeap($Heap) && this != null && read($Heap, this, alloc) && dtype(this) == class._module.__default && (forall $t#3: BoxType :: { Map#Domain(m#0)[$t#3] } Map#Domain(m#0)[$t#3] ==> GenericAlloc($t#3, $Heap)) && (forall $t#3: BoxType :: { Map#Elements(m#0)[$t#3] } Map#Domain(m#0)[$t#3] ==> GenericAlloc($t#3, $Heap))) ==> _module.__default.domain#2($Heap, this, m#0) == (lambda $y#4: BoxType :: (exists x#2: BoxType :: GenericAlloc(x#2, $Heap) && Map#Domain(m#0)[x#2] && $y#4 == x#2)));

// frame axiom for _module.__default.domain
axiom (forall $h0: HeapType, $h1: HeapType, this: ref, m#0: Map BoxType BoxType :: { $HeapSucc($h0, $h1), _module.__default.domain($h1, this, m#0) } $IsGoodHeap($h0) && $IsGoodHeap($h1) && this != null && read($h0, this, alloc) && dtype(this) == class._module.__default && read($h1, this, alloc) && dtype(this) == class._module.__default && (forall $t#5: BoxType :: { Map#Domain(m#0)[$t#5] } Map#Domain(m#0)[$t#5] ==> GenericAlloc($t#5, $h0)) && (forall $t#5: BoxType :: { Map#Elements(m#0)[$t#5] } Map#Domain(m#0)[$t#5] ==> GenericAlloc($t#5, $h0)) && (forall $t#6: BoxType :: { Map#Domain(m#0)[$t#6] } Map#Domain(m#0)[$t#6] ==> GenericAlloc($t#6, $h1)) && (forall $t#6: BoxType :: { Map#Elements(m#0)[$t#6] } Map#Domain(m#0)[$t#6] ==> GenericAlloc($t#6, $h1)) && $HeapSucc($h0, $h1) ==> (forall<alpha> $o: ref, $f: Field alpha :: false ==> read($h0, $o, $f) == read($h1, $o, $f)) ==> _module.__default.domain($h0, this, m#0) == _module.__default.domain($h1, this, m#0));

axiom (forall $h0: HeapType, $h1: HeapType, this: ref, m#0: Map BoxType BoxType :: { $HeapSucc($h0, $h1), _module.__default.domain#limited($h1, this, m#0) } $IsGoodHeap($h0) && $IsGoodHeap($h1) && this != null && read($h0, this, alloc) && dtype(this) == class._module.__default && read($h1, this, alloc) && dtype(this) == class._module.__default && (forall $t#5: BoxType :: { Map#Domain(m#0)[$t#5] } Map#Domain(m#0)[$t#5] ==> GenericAlloc($t#5, $h0)) && (forall $t#5: BoxType :: { Map#Elements(m#0)[$t#5] } Map#Domain(m#0)[$t#5] ==> GenericAlloc($t#5, $h0)) && (forall $t#6: BoxType :: { Map#Domain(m#0)[$t#6] } Map#Domain(m#0)[$t#6] ==> GenericAlloc($t#6, $h1)) && (forall $t#6: BoxType :: { Map#Elements(m#0)[$t#6] } Map#Domain(m#0)[$t#6] ==> GenericAlloc($t#6, $h1)) && $HeapSucc($h0, $h1) ==> (forall<alpha> $o: ref, $f: Field alpha :: false ==> read($h0, $o, $f) == read($h1, $o, $f)) ==> _module.__default.domain#limited($h0, this, m#0) == _module.__default.domain#limited($h1, this, m#0));

procedure CheckWellformed$$_module.__default.domain(this: ref where this != null && read($Heap, this, alloc) && dtype(this) == class._module.__default, m#0: Map BoxType BoxType where (forall $t#7: BoxType :: { Map#Domain(m#0)[$t#7] } Map#Domain(m#0)[$t#7] ==> GenericAlloc($t#7, $Heap)) && (forall $t#7: BoxType :: { Map#Elements(m#0)[$t#7] } Map#Domain(m#0)[$t#7] ==> GenericAlloc($t#7, $Heap)));
free requires 0 == $ModuleContextHeight && 0 == $FunctionContextHeight;
ensures (forall i#1: BoxType :: GenericAlloc(i#1, $Heap) ==> (_module.__default.domain#2($Heap, this, m#0)[i#1] <==> Map#Domain(m#0)[i#1]));



implementation CheckWellformed$$_module.__default.domain(this: ref, m#0: Map BoxType BoxType)
{
var i#12: BoxType;
var m#13: Map BoxType BoxType;
var $_Frame: <beta>[ref,Field beta]bool;
var x#14: BoxType;

if (*)
{
assume (forall $t#8: BoxType :: { _module.__default.domain($Heap, this, m#0)[$t#8] } _module.__default.domain($Heap, this, m#0)[$t#8] ==> GenericAlloc($t#8, $Heap));
havoc i#12;
assume GenericAlloc(i#12, $Heap);
m#13 := m#0;
assert this == this && m#0 == m#0;
assume (this == this && m#0 == m#0) || _module.__default.domain#canCall($Heap, this, m#0);
assume (forall i#1: BoxType :: GenericAlloc(i#1, $Heap) ==> (_module.__default.domain($Heap, this, m#0)[i#1] <==> Map#Domain(m#0)[i#1]));
assume false;
}
else
{
$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
havoc x#14;
assume GenericAlloc(x#14, $Heap);
if (Map#Domain(m#0)[x#14])
{
}

assume _module.__default.domain($Heap, this, m#0) == (lambda $y#9: BoxType :: (exists x#2: BoxType :: GenericAlloc(x#2, $Heap) && Map#Domain(m#0)[x#2] && $y#9 == x#2));
assume true;
}
}



procedure CheckWellformed$$_module.__default.Lemma(this: ref where this != null && read($Heap, this, alloc) && dtype(this) == class._module.__default, m#3: Map BoxType BoxType, m2#4: Map BoxType BoxType);
free requires 0 == $ModuleContextHeight && $InMethodContext;
modifies $Heap, $Tick;



implementation CheckWellformed$$_module.__default.Lemma(this: ref, m#3: Map BoxType BoxType, m2#4: Map BoxType BoxType)
{
var $_Frame: <beta>[ref,Field beta]bool;
var x#15: int;
var m#16: Map BoxType BoxType;
var m#17: Map BoxType BoxType;

$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
havoc x#15;
if (Map#Domain(m2#4)[$Box(x#15)])
{
}

assume (forall x#5: int :: true ==> Map#Domain(m2#4)[$Box(x#5)] ==> Map#Domain(m#3)[$Box(x#5)]);
havoc $Heap /* where $IsGoodHeap($Heap) */;
assume (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(old($Heap), $o, alloc) ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
assume $HeapSucc(old($Heap), $Heap);
m#16 := m2#4;
assume _module.__default.domain#canCall($Heap, this, m2#4);
m#17 := m#3;
assume _module.__default.domain#canCall($Heap, this, m#3);
assume Set#Subset(_module.__default.domain($Heap, this, m2#4), _module.__default.domain($Heap, this, m#3));
}



procedure _module.__default.Lemma(this: ref where this != null && read($Heap, this, alloc) && dtype(this) == class._module.__default, m#3: Map BoxType BoxType, m2#4: Map BoxType BoxType);
free requires 0 == $ModuleContextHeight && $InMethodContext;
requires (forall x#5: int :: true ==> Map#Domain(m2#4)[$Box(x#5)] ==> Map#Domain(m#3)[$Box(x#5)]);
modifies $Heap, $Tick;
ensures Set#Subset(_module.__default.domain#2($Heap, this, m2#4), _module.__default.domain#2($Heap, this, m#3));
// frame condition
free ensures (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(old($Heap), $o, alloc) ==> read($Heap, $o, $f) == read(old($Heap), $o, $f));
// boilerplate
free ensures $HeapSucc(old($Heap), $Heap);



implementation _module.__default.Lemma(this: ref, m#3: Map BoxType BoxType, m2#4: Map BoxType BoxType)
{
var $_Frame: <beta>[ref,Field beta]bool;
var $initHeapParallelStmt#4: HeapType;

$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && read($Heap, $o, alloc) ==> false);
$initHeapParallelStmt#4 := $Heap;
havoc $Tick;
assume (forall $ih#m2#21: Map BoxType BoxType, $ih#m23#22: Map BoxType BoxType :: (forall x#5: int :: true ==> Map#Domain($ih#m23#22)[$Box(x#5)] ==> Map#Domain($ih#m2#21)[$Box(x#5)]) && (($ih#m2#21 == null && m#3 != null) || (($ih#m2#21 != null <==> m#3 != null) && $ih#m23#22 == null && m2#4 != null)) ==> Set#Subset(_module.__default.domain($Heap, this, $ih#m23#22), _module.__default.domain($Heap, this, $ih#m2#21)));
}

Coordinator
Oct 17, 2012 at 2:01 AM

Thanks for the bug report.  I fixed it.  Until you get the fix, you can work around the problem by marking the ghost method with {:induction false}, like this: 

ghost method {:induction false} Lemma(m : map, m2 : map)

  Rustan

Oct 17, 2012 at 11:14 AM

Thank you, Rustan!