Spec-Sharp
| Spec # | |
|---|---|
| Paradigms : | Object-oriented programming language |
| Publishing year: | 2004 |
| Developer: | Microsoft Research |
| Current version : | SpecSharp 2011-10-03 (October 7, 2011) |
| Typing : | strong |
| Influenced by: | C # |
| Operating system : | all with CLR |
| research.microsoft.com/SpecSharp | |
Spec # is an object-oriented programming language developed by Microsoft Research that is an extension of the established C # . It is free and including for the development environment Microsoft Visual Studio 2003, 2005 and 2008 available and also forms the basis for Sing # . This language was developed for the Singularity project. Some of the concepts were incorporated into Visual Studio 2010 as code contracts .
concept
Spec # is an extension of C # to include preconditions, postconditions, non-zero types and object invariants. The method conditions are mapped by contracts and thus expand the meta description of an object. In addition, Checked Exceptions implemented. The extensions are possible through the Spec # compiler. A theorem prover with the code name Boogie was implemented for protection.
Programming example
The following lines give a little insight into the structure and use of Spec #. This is the start source code that is generated by Visual Studio 2005 via the project wizard for a console application :
using System;
public class Program
{
static void Main(string![]! args)
// The following precondition is redundant with the type
// signature for the parameter, but shown here as an example.
requires forall{int i in (0:args.Length); args[i] != null};
{
Console.WriteLine("Spec# says hello!");
}
}
See also
Web links
- Official website (English)
- Expert to Expert: Contract Oriented Programming and Spec # (Erik Meijer in conversation with the Spec # designers on Channel9) (English)
- Code Contracts in .NET 4 (English)