Building Dafny Visual Studio Extension

You will need the Visual Studio 2012 SDK installed you can tell this because Visual Studio tells you the project is incompatible and refuses to open it. But if you use a text editor to look at the associated .csproj file, that file has the GUID “82b43b9b-a64c-4715-b499-d71e9ca2bd60” in the “project types” section. And this GUID means “needs the visual studio SDK”.

You probably need to build boogie first. You may find that you need to enable nuget restore (right click the Boogie Solution in the Solution Explorer and click Enable NuGet Package Restore) for the boogie solution, in order to get visual studio to download the correct version of nunit.

Then you need to open the solution Dafny.sln in the source directory, and build it with visual studio. Then build the visual studio extension DafnyExtension.sln. Then in “Extensions and Updates” you can uninstall the DafnyLanguageMode if you already have it. Then you can install Binaries\DafnyLanguageService.vsix to get the VS extension.

Also, on the Dafny VS extension color codes. I think perhaps: yellow means “line changed since last save”; orange means “line changed since the last verify run”; pink means “line currently being verified”; and green means line verified.

Build Boogie

  1. Get the latest code (its now on github)
  2. Open Source/Boogie.sln in visual studio
  3. Build -> Build

Build Dafny

  1. Get the latest code (hg pull the hg update)
  2. Open Source/Dafny.sln in visual studio
  3. Build -> Build
  4. Open Source/DafnyExtension.sln in visual studio
  5. Build -> Build


  1. Dafny type system documentation

Inverting Maps in Dafny

I had cause to need to prove some things about injective maps and inverses.

// union on maps does not seem to be defined in Dafny
function union<U, V>(m: map<U,V>, m': map<U,V>): map<U,V>
	requires m !! m'; // disjoint
	ensures forall i :: i in union(m, m') <==> i in m || i in m';
	ensures forall i :: i in m ==> union(m, m')[i] == m[i];
	ensures forall i :: i in m' ==> union(m, m')[i] == m'[i];
	map i | i in (domain(m) + domain(m')) :: if i in m then m[i] else m'[i]
// the domain of a map is the set of its keys  
function domain<U,V>(m: map<U,V>) : set<U>
	ensures domain(m) == set u : U | u in m :: u;
	ensures forall u :: u in domain(m) ==> u in m;
		set u : U | u in m :: u
// the domain of a map is the set of its values
function range<U,V>(m: map<U,V>) : set<V>
	ensures range(m) == set u : U | u in m :: m[u];
	ensures forall v :: v in range(m) ==> exists u :: u in m && m[u] == v;
	set u : U | u in m :: m[u]
// here a map m is smaller than m' if the domain of m is smaller than 
// the domain of m', and every key mapped in m' is mapped to the same 
// value that it is in m.   
predicate mapSmaller<U,V>(m: map<U,V>, m': map<U,V>)
	ensures mapSmaller(m,m') ==> 
		(forall u :: u in domain(m) ==> u in domain(m'));
	forall a :: a in m ==> a in m' && m[a] == m'[a]
// map m is the inverse of m' if for every key->value in m
// there is value->key in m', and vice versa
predicate mapsAreInverse<U,V>(m: map<U,V>, m': map<V,U>)
	(forall a :: a in m ==> m[a] in m' && m'[m[a]] == a) &&
	(forall a :: a in m' ==> m'[a] in m && m[m'[a]] == a) 
// map m is injective if no two keys map to the same value	
predicate mapInjective<U,V>(m: map<U,V>)
	forall a,b :: a in m && b in m ==> a != b ==> m[a] != m[b]
// here we prove that injective map m has an inverse, we prove
// this by calculating the inverse for an arbitrary injective map.
// maps are finite in Dafny so we have no termination problem
lemma invertMap<U,V>(m: map<U,V>) returns (m': map<V,U>)
	requires mapInjective(m);
	ensures mapsAreInverse(m,m');
	var R := m;     // part of m left to invert
	var S := map[]; // part of m already inverted
	var I := map[]; // inverted S
	while R != map[]       // while something left to invert
		decreases R;   // each loop iteration makes R smaller
		invariant mapSmaller(R, m);
		invariant mapSmaller(S, m);
		invariant R !! S; // disjoint
		invariant m == union(R, S);
		invariant mapsAreInverse(S,I);
		var a :| a in R;   // take something arbitrary in R
		var v := R[a];
		var r := map i | i in R && i != a :: R[i];  // remove a from R
		I := I[v:=a];
		S := S[a:=v];
		R := r;
	m' := I;  // R is empty, S == m, I inverts S
// here we prove that every injective map has an inverse  
lemma injectiveMapHasInverse<U,V>(m: map<U,V>)
	requires mapInjective(m);
	ensures exists m' :: mapsAreInverse(m, m'); 
    var m' := invertMap(m);
// here we prove that no non-injective map has an inverse  
lemma nonInjectiveMapHasNoInverse<U,V>(m: map<U,V>)
	requires !mapInjective(m);
	ensures !(exists m' :: mapsAreInverse(m, m')); 
{ }
// here we prove that if m' is the inverse of m, then the domain of m
// is the range of m', and vice versa  
lemma invertingMapSwapsDomainAndRange<U,V>(m: map<U,V>, m': map<V,U>)
	requires mapsAreInverse(m, m');
	ensures domain(m) == range(m') && domain(m') == range(m);
{ }
// a map m strictly smaller than map m' has fewer elements in its domain 
lemma strictlySmallerMapHasFewerElementsInItsDomain<U,V>(m: map<U,V>, m': map<U,V>)
	requires mapSmaller(m,m') && m != m';
	ensures domain(m') - domain(m) != {};
	var R,R' := m,m';
	while R != map[]
		decreases R;
		invariant mapSmaller(R,R');
		invariant R != R';
		var a :| a in R && a in R';
		var v := R[a];
		var r := map i | i in R && i != a :: R[i];
		var r' := map i | i in R' && i != a :: R'[i];
		R := r;
		R' := r';
	assert R == map[];
	assert R' != map[];
	assert domain(R) == {};
	assert domain(R') != {};
function invert<U,V>(m:map<U,V>) : map<V,U>
	requires mapInjective(m); 
	ensures mapsAreInverse(m,invert(m));
	var m' :| mapsAreInverse(m,m');