Spec# and Boogie Released on CodePlex

Posted by Jonathan Allen on Aug 05, 2009

Sections

Process & Practices,

Architecture & Design,

Development

Topics

.NET ,

Code Analysis ,

Language Design

Tags

Static Analysis ,

Spec#

Spec# is a research language based on C#. It is based contract-first principals where the pre- and post-conditions for functions can be defined declaratively. Other features include class invariants, non-nullable reference types, and enhanced static analysis capabilities.

While key features like Code Contracts have found their way into .NET 4, Spec# itself has languished in research status. Recently Microsoft has announced that it is finally loosening the reins on it, but only by a little bit. The source code for Spec# is now available on CodePlex under the Microsoft Research Shared Source License Agreement. This license restricts its use to non-commercial purposes.

Hand in hand with Spec# is Boogie, an intermediate language for code verification. Boogie isn’t .NET specific, other languages it supports include “the HAVOC and vcc verifiers for C, the Dafny language and verifier, and the concurrent language Chalice”.

Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.

Boogie has been released under the Microsoft Public License, which conforms to Free/Open Source standards.

Currently Microsoft is positioning Code Contracts as the way forward, meaning Spec# probably won’t see much in the way of future development.

• Older >