Spec-Sharp
Spec # is a technology developed by Microsoft Research, object-oriented programming language that is an extension to the established C #. It is free and, inter alia, 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.
Concept
Spec # is an extension of C # to preconditions, postconditions, non -zero type and Objektinvarianzen. The methods and conditions are represented by contracts and thus extend the meta description of an object. In addition Checked exceptions are implemented. The extensions are made possible by the Spec # compiler. To hedge a theorem prover, codenamed Boogie has been implemented.
Programming Example
The following lines give a little insight into the structure and use of Spec #. This is the start code that is generated by Visual Studio 2005 through 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 in example. requires forall {int i in ( 0: args.Length ); args [ i] = null}! ; { Console.WriteLine (" Spec # says hello! "); } } see also