BT
x Your opinion matters! Please fill in the InfoQ Survey about your reading habits!

Spec# and Boogie Released on CodePlex

by Jonathan Allen on Aug 05, 2009 |

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.

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Educational Content

General Feedback
Bugs
Advertising
Editorial
InfoQ.com and all content copyright © 2006-2014 C4Media Inc. InfoQ.com hosted at Contegix, the best ISP we've ever worked with.
Privacy policy
BT