Years ago, Dr. Dobb's columnist Al Stevens launched a C-library project that implemented a subset of the IBM SAA Common User Access (CUA) interface. Being a C programmer, he wanted to call it "C-Sharp," but being a realist, he figured that someone else had already latched on to that name. So being a musician and knowing that C-sharp is the same as D-flat, he christened the library D-Flat.

Eventually, of course, Microsoft snagged "C#" (pronounced "C-Sharp") and proceeded to sharpen one language after another. Let's see, there's A#, F#, J#, Sing#, and X#, and probably others. The one I recently ran across is Spec#. Admittedly, it has been around for a number of years, but I just ran across it when reading about program verifiers.

Developed by Microsoft Research's Programming Languages and Methods group, Spec# is an C# extension that extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and post-conditions as well as object invariants. The Spec# compiler, which has been integrated into Visual Studio, statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools. The Spec# static program verifier -- Boogie -- generates logical verification conditions from a Spec# program. Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it. A unique Spec# feature is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads, and inter-object relationships.

Boogie is a program verification system that produces verification conditions for programs written in an intermediate language (also named Boogie). The intermediate language is easy to target from source languages such as Spec#, C#, or even C. Boogie accepts the Boogie language as input and generates verification conditions that are passed to a solver.

Both Spec# and Boogie have been released under the Microsoft Research Shared Source License Agreement (MSR-SSLA) for non-commercial uses.