Spec Sharp

From Wikipedia, the free encyclopedia

The correct title of this article is Spec#. The substitution or omission of a # sign is because of technical restrictions.

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 post-conditions. 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.

Microsoft Research developed both Spec# and C#; in turn, Spec# serves as the foundation of the Sing# programming language, which Microsoft Research also developed.

[edit] Sources

  • Barnett, M., K. R. M. Leino, W. Schulte, "The Spec# Programming System: An Overview." Proceedings of Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS), Marseilles. Springer-Verlag, 2004.

[edit] See also

[edit] External links

v • d • e
Microsoft Research (MSR)
Languages and compilers
Polyphonic C# · Cω · Spec# · Sing# · Bartok · Phoenix
Distributed / grid computing
Internet and networking
Other projects
Operating systems
APIs
Joins · Accelerator · Dryad  · SXM
Launched as products
Soft Eng logo This computer language-related article is a stub. You can help Wikipedia by expanding it.
Languages