Dafny Triggers

It is possible to write tiggers for particular quantifiers in Dafny programs.

```predicate P(x:int) { true }   lemma ThereIsMoreThanOneInteger(x:int) ensures exists z:int :: z!=x; { // can't prove }   lemma NoReallyThereIsMoreThanOneInteger(x:int) ensures exists z:int {:trigger P(z)} :: z!=x; { assert P(x+1); // can prove }```

Dafny Function Lemmas

Sometimes it is hard to use a normal Dafny method lemma where you need it. For example, if you want to use a lemma inside a function or in a contract. There is a simple solution.

Given a method lemma:

```static lemma SomethingValid(s:S) requires P(s); ensures Q(s);```

We can produce a function lemma:

```static lemma SomethingValidFn(s:S) requires P(s); ensures Q(s); ensures SomethingValidFn(s); { SomethingValid(s); true }```

Dafny: Proving forall x :: P(x) ==> Q(x)

The general method in Dafny for proving something of the form `forall x :: P(x) ==> Q(x)` is:

```lemma X() ensures forall x :: P(x) ==> Q(x); { forall x | P(x) ensures Q(x); { // prove Q(x) } }```

Using {:verify false} in Dafny

Due to the nature of the underlying SMT used by Dafny for proof checking, Dafny sometimes takes a very long time to verify things. I find it useful to ask Dafny to work on a single lemma at a time. This can be achieved using the {:verify false} annotation. I set every function and method in my proof to {:verify false}, then change only the one I am working on back to {:verify true}. Occasionally I use find and replace to change all the {:verify false} annotations to {:verify true} and then run the whole proof through the Dafny command line.

I am using Opaque functions in Dafny quite heavily, and for three main reasons:

Opaque functions can improve performance

I have a very large predicate which judges partial isomorphism between two program states. This predicate appears in the requires, ensures and bodies of a large number of lemmas and functions in my proof. The number of facts that are introduce by Dafny automatically revealing these function definitions seems to substantially slow down the proof step, sometimes to the point where it no longer goes through in an amount of time I am willing to wait.

For example take a predicate like this

```prediate I(a:T,b:T) { P(a,b) && Q(a,b) && R(a,b) && S(a,b) } predicate P(a:T,b:T) { ... } predicate Q(a:T,b:T) { ... } ... static lemma IThenSomethingThatReliesOnQ(a:T,b:T) requires I(a,b); ensures SomethingThatReliesOnQ(a,b); { // Q automatically revealed, but so is P,R and S }```

```prediate I(a:T,b:T) { P(a,b) && Q(a,b) && R(a,b) && S(a,b) } predicate {:opaque true} P(a:T,b:T) { ... } predicate {:opaque true} Q(a:T,b:T) { ... } ... static lemma IThenSomethingThatReliesOnQ(a:T,b:T) requires I(a,b); ensures SomethingThatReliesOnQ(a,b); { reveal_Q(); // reveals Q only, not P,R and S }```

I initially really liked the automatic function definition revealing feature, but as my proof got larger I liked it less. Particularly in the presence of big predicates (like my isomorphism predicate), I found it can get quite hard to understand which parts of the proof rely on which facts. This made it harder for me to work out what I need to establish in other parts of the proof (in this case, that the isomorphism has certain properties and that those can be used to show it is preserved by some particular program execution steps).

The example above shows how using opaque and reveal makes the proof more self documenting, allows us to automatically check that documentation and provides (I think) more insight into the proof.

If you are using {:verify false} to restrict re-verification only to the elements you are working on, then having functions set to opaque helps you find all the places that depend on their definition. So, if you change the definition then you can easily find all the places that will need to be re-verified with the new definition.

Naming quantifiers in Dafny

It seems to help Dafny with instantiation of quantifiers during proofs if you give the quantified expression a name by encapsulating it in a predicate. If you don’t you can end up in a situation where you prove some quantified property, but are then unable to subsequently assert that quantified property, I think due to Dafny not understanding that the quantification is the same. Naming the property (or more likely, only writing it in one place rather than two places) fixes this.

For example rather than writing:

``` ... ensures forall c :: P(a, c) == P(b, c); ... assert forall c :: P(a, c) == P(b, c);```

Write this:

``` predicate Q(a:S,b:S) { forall c :: P(a, c) == P(b, c) } ... ensures Q(a, b); ... assert Q(a, b);```

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

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)); { injectiveMapHasInverse(m);   var m' :| mapsAreInverse(m,m'); m' }```

Incremental software projects can be less risky

Inability to proceed incrementally is risk factor for project failure. If you have to wait until the end of the project for delivery, then you get (or don’t get) all your features at that point. What if an unexpected event occurs? Then you may reach the project end date still with all features in progress and none finished!

How does this problem manifest? You have a big list of features that are partially working, or “in progress”, and few features that are “finished” or “not started”. Perhaps you have even lost track of which features are finished or not, or how completed the features are, or how completed the project is?

What I prefer to see in a de-risked project is: a list of completed features; one in-progress item that is currently being worked on; and a bunch of not-started-at-all items. It can be risky to have a process of “filling-in” the code from a sort of sketch implementation across all of the features – I generally prefer an incremental process of adding features one-by-one to a known finished and working base. If you need to check on features to inform the design process then implement simple, but complete, minimal versions of the key features. But do them one at a time.

The three main problem with lots of started-but-not-finished items are:

1. that it can be difficult to understand how much work actually needs to be done before you get any further completed features, there is a /risk/ that big surprises can come up late on.
2. that it is difficult for testers to give you early feedback on the quality of your implementation – they end up having to test all the features at the end. And at the end is when you have no time left to fix any problems they may discover. Of course they may not discover any problems, but I am talking about risk management and predictability.
3. and if you do get your testers going early then they don’t know if something they don’t like about the product is caused by an incomplete feature, or is a genuine problem. You can end up with lots of wasted time for testers and developers as they try and sort this communication problem out. And I think it can lead to testers getting used to a lower quality of half-finished software.

There are more problems actually, but those are the most serious ones in the short term. Maybe I will write more about this later.

Blog Review: Should I comment code?

I want to try to get a sense of the set of reasons that people have for commenting or not commenting code. What follows is a table of blog posts (and similar) with an assesment of if they are generally for or against comments in code, and extracts which (I think) give an overview of their key points.

If you have any more links (perhaps something you have written) then please feel free to add them in a similar format in the comments on this post.

Post Position  Comment
The Hows and Whys of Commenting C and C++ Code Pro Comments should reveal the underlying structure of the code, not the surface details. A more meaningful comment would be “int callCount = 0; //holds number of calls to [function].”
Why comments in code are largely pointless Anti as we do the standard stuff we comment the code frequently and with confidence […] when it comes to something a bit more difficult we maybe have to try a few different options before we get it right […] there is little imperative to go back and document your work […] you get a large amount of commentary on the pedestrian every day part of your application and very little in the more interesting areas
Commenting Code Effectively: The How AND The Why Pro “why was it done that way in the first place?” […] Much like a math teacher asks you to show your work so that they can see how you arrived at the answer, a developer must comment their code as they are writing it to document (1) how the code works, and (2) why it was written that way. The developers thoughts and decisions are just as important in the comments as an explanation of how the code works. […] Make sure all methods and parameters are documented, explaining what is the purpose of each method and what are the expected parameters and results
The Problem With Comments Pro Comments should be displayed in the UI by editors as more important than the code (e.g. in bright colors)
Why would company develop an atmosphere which discourage code comments? forum
Comments are a code smell forum on balance probably pro
Eliminating Comments: the Road to Clarity Anti It is not that comments in and of themselves are bad. It’s more that having comments in your code indicates that your code itself is not clear enough to express its intent.
Common Excuses Used To Comment Code and What To Do About Them Anti (extensive extracts as post is no-longer available) Just two years ago, I was beyond skeptical towards the forces telling me that comments are worse-than-useless, self-injuring blocks of unexecutable text in a program. I thought the idea was downright ludicrous. But as I’ve made an effort towards reaching this nirvana called “self-documenting code,” I’ve noticed it’s far more than a pipe dream. […] you can choose better variable names and keep all code in a method at the same level of abstraction to make is easy to read without comments. […] want to keep track of who changed what and when it was changed. Version control does this quite well […] The code too complex to understand without comments. I used to think this case was a lot more common than it really is. But truthfully, it is extremely rare. Your code is probably just bad, and hard to understand. […] Natural language is easier to read than code. But it’s not as precise.
Don’t Comment Your Code Anti In the vast majority of cases, a comment indicates that something is wrong. If you have to add a comment to explain what a block of code is doing, that means that the code is too complicated or is using poor variable names or function calls.
Not Commenting And The Tipping Point Of Poor Programming Not Sure It’s one thing for a person, such as Brian, that writes very high quality code, to keep his comments to a minimum. But what about the majority of people who are not at his level? These are people who are not writing great code to begin with – are they going to view these blog posts as the excuse and justification to stop commenting their code? What happens then? We have an epidemic (as Gladwell would put it) of poorly written and poorly commented code. […] I am merely trying to play devil’s advocate to keep things in perspective.
Code Tells You How, Comments Tell You Why Anti/Caveat If you write your code to be consumed by other programmers first, and by the compiler second, you may find the need for additional comments to be greatly reduced. […] [code] can’t explain why the program is being written, and the rationale for choosing this or that method. [code] cannot discuss the reasons certain alternative approaches were taken.
Why programmers don’t comment their code Pro That’s probably not true unless you wrote it in COBOL. You may very well know that
\$string = join(”,reverse(split(”,\$string)));
just reverses your string, but how hard is it to insert
# Reverse the string
Why not to comment code Anti Every time you’re tempted to comment, take the time to think if you can make the code tell its own story, e.g., instead of some branching condition, extract the condition into a method to emphasize the story of why over how.
Developers comment to explain a confusing part of their code rather than take the time to refactor it by extracting a method or naming a variable properly. Inevitably the code gets modified and the comment rots.
On Commenting Source Code – Why Commenting is Not Bad Practice Pro Maybe I’m missing something, but that’s not how I see the purpose of refactoring. When I refactor code I don’t arbitrarily break out larger functions into smaller functions that are only ever called once. Instead, I look for patterns that are repeated across the code base and try to create new functions that encapsulate those patterns.
Portrait of a N00b Unknown (couldn’t understand this post, a bit TL;DR combined with it somehow being a long missive on static types and if they are like comments or not) Should a team write for the least common denominator? And if so, exactly how compressed should they make the code? I think the question may be unanswerable […] I think the general answer to this is: when in doubt, don’t model it. Just get the code written, make forward progress. Don’t let yourself get bogged down with the details of modeling a helper class that you’re creating for documentation purposes.
comments are a sign of bad code and I am not sorry for saying it Anti Comments are not bad, the code is – I’m not suggesting to forgo the use of comments, but that they are only band-aids. […] Code should not be written to the level of the dumbest developer, the dumbest developer should be brought to the level of the code (though I want to reiterate good code should be easily readable).
How bad comments are born in your code Pro I don’t think going to the extreme and having comments replaced with just relevant class/method naming is a good idea because you cannot express full intent in a class/method name. This is actually why you have to write some code inside the class or the method, isn’t it? […] To summarize with only one word the reason for commenting code is maintenance!
Code commenting? Try Business Commenting. Pro one thing I rarely hear mentioned is that it’s often more interesting to comment the business justification than it is to comment the code. Jeff goes some way towards suggesting this when he says to comment the “why”, but for many people that translates to “Why did I write the code this way?”. I often find that code I’m maintaining is missing comments regarding the business logic. Rather than “Why is the code designed like this?”, something like “Why is the business process designed like this?”
Once Again: Comments In Code Aren’t Necessarily Bad Pro/Caveat I generally agree that you should strive to avoid comments in code. That is, you should write your code in a way that doesn’t require comments for the reader to easily understand and grasp what the code is doing. However… there are situations where comments are helpful (or even required) […] That code applies a certain pattern which isn’t well known, but there is a very specific reason why the pattern is needed. And I still believe that most developers need comments to understand it properly. […] if you need to write some code in a very non-obvious way, then you could really make things easier for those who need to maintain it […] by including some comments to explain why a certain solution/pattern was chosen.
Cleaning bad code Anti Even when comments are correct and useful, remember that you will be doing a lot of refactoring of the code. The comments may no longer be correct when you are done. And there is no unit test in world that can tell you if you have “broken the comments”. Good code needs few comments because the code itself is clearly written and easy to understand. Variables with good names do not need comments explaining their purpose. Functions with clear inputs and outputs and no special cases or gotchas require little explanation. Simple, well written algorithms can be understood without comments. Asserts document expectations and preconditions.
Don’t comment bad code—rewrite it. Forum