Seminar work about Dafny

Oct 19, 2015 at 11:34 AM
Hi, in order to present Dafny in a Course I take this semester, I need some "background" information about when Dafny was released and so on. Unfortunately, I was not able to find much about that.
From what I found now, I suppose it was joint work from K. Rustan M. Leino with Jason Koenig, Michał Moskal, Nadia Polikarpova, Valentin Wüstholz and it was released in 2008. Is that correct?
Oct 29, 2015 at 4:01 PM
Nice to hear about your presentation. What you stated is correct, but incomplete. Other people who have worked on the Dafny implementation include Reza Ahmadi, Nada Amin, Maria Christakis, Chris Hawblitzel, Jay Lorch, Qunyan Mangus, Bryan Parno, Clément Pit--Claudel, Michael L. Roberts, and Dan Rosén.

Dafny started as a little language and verifier to experiment with a certain style of specifications (known as "dynamic frames") for programs that operate on a mutable heap. Since then, Dafny has become a full program verifier with both imperative (assignments, loops, classes, etc.) and functional (datatypes, co-datatypes, higher-order functions, etc.) programming constructs as well as proof authoring facilities (lemmas, proof calculations, refinement, etc.). It has been used for some systems projects, including ExpressOS [ASPLOS 2013], Ironclad Apps [OSDI 2014], and IronFleet [SOSP 2015], and it has been used in various forms of teaching at more than 30 universities.

Rustan
Nov 1, 2015 at 11:56 AM
Thank you very much!

I am experiencing some difficulties while playing with maps. Is map union (+) possible (as shown in the tutorial @rise4fun)?
For example should

var m1:=map[0:=1];
var m2:=map[2:=3];
var m:=m1+m2;


work? Because VS gives me an error, that the arguments to + must be numeric or collection type.
Nov 16, 2015 at 10:01 PM
Good catch. That's a bug in the tutorial. The + operator is not supported on maps. If you want the union of two maps, use your own map comprehension:
method M() {
  var m1:=map[0:=1]; 
  var m2:=map[2:=3]; 
  var m1Domain := set x | x in m1;
  var m2Domain := set x | x in m2;
  var m := map x | x in m1Domain + m2Domain :: if x in m1 then m1[x] else m2[x];
}
(Admittedly, this is a lot more complicated than the +. I imagine we'll support + on maps in the future.)

I removed the sentence about map union from the tutorial.

Thanks,
Rustan