At the Lang.NET Symposium, I met up a member of the Spec# research team, Mike Barnett, shared with him information about the tool I was working on, and gave him my contact information.As I suspected earlier, Rustan Leino, who previously worked at HP/Compaq on ESC/Java, joined Microsoft to work on the Spec# programming system. I watched an impressivepresentation on the tool that included real-time IDE integration and syntax highlighting. Spec# works off of IL with the implication that eventually all the .NET languages will eventually support specifications. Indeed, the presentation was called Why Every Language Should (Will) have Specifications. Spec# requires that all calls to functions with specifications be provably true either through existing conditions within code or by using...
Previous Topic
