Designed by Microsoft Research | Developer Microsoft Research | |
Paradigm multi-paradigm: structured, imperative, object-oriented, event-driven, functional, contract First appeared 2004; 13 years ago (2004) Stable release SpecSharp 2011-10-03 / October 7, 2011; 5 years ago (2011-10-07) Typing discipline static, strong, safe, nominative |
Spec# is a programming language with specification language features that extends the capabilities of the C# programming language with Eiffel-like contracts, including object invariants, preconditions and postconditions. Like ESC/Java, it includes a static checking tool based on a theorem prover that is able to statically verify many of these invariants. It also includes a variety of other minor extensions to the language, such as non-null reference types.
Contents
The code contracts API in the .NET Framework 4.0 has evolved with Spec#.
Microsoft Research developed both Spec# and C#; in turn, Spec# serves as the foundation of the Sing# programming language, which Microsoft Research also developed.
Features
See also: Spec# in C Sharp syntax.Spec# extends the core C# programming language with features such as:
Example
This example shows two of the basic structures that are used when adding contracts to your code (try Spec# in your browser).
Sing Sharp
Sing Sharp (or Sing#) is a superset of Spec Sharp. Microsoft Research developed Spec#, and later extended it into Sing# in order to develop the Singularity operating system. Sing# augments the capabilities of Spec# with support for channels and low-level programming language constructs, which are necessary for implementing system software. Sing# is type-safe. The semantics of message-passing primitives in Sing# are defined by formal and written contracts.