I work on
Spec# (pronounced "speck-sharp"), an experimental extension to
C# that adds design-by-contract
features. Contracts include method
preconditions, postconditions, and
object invariants. Contracts capture
programmer intentions about how methods
and data are to be used. The Spec#
compiler emits run-time checks that
enforce the contracts and the Spec#
program verifier uses theorem-proving
technology to statically check the
consistency between a program and its
contracts. Spec# helps programmers write
correct software and makes explicit the
correct usage of APIs for clients. It is
integrated into Visual Studio .NET.
The other members of the Spec# team are:
Manuel Fähndrich,
Rustan Leino,
Francesco Logozzo,
Peter Müller,
Wolfram Schulte, and Herman Venter.
