Spec Sharp

Spec#

Paradigm	multi-paradigm: structured, imperative, object-oriented, event-driven, functional, contract
Appeared in	2004
Designed by	Microsoft Research
Developer	Microsoft Research
Stable release	1.0.21125
Typing discipline	static, strong, safe, nominative
Influenced by	C#, Eiffel
Influenced	Sing#
Website	Spec# website

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.

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

Example

This example shows two of the basic structures that are used when adding contracts to your code.

    static void Main(string![] args)
        requires args.Length > 0
    {
        foreach(string arg in args)
        {
            Console.WriteLine(arg);
        }
    }

• ! is used to make a reference type non-nullable, e.g. you cannot set the value to null. This in contrast of nullable types which allows value types to be set as null.

• requires indicates a condition that must be followed in the code. In this case the length of args is not allowed to be zero or less.

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.

See also

• Eiffel
• Singularity
• Sing#
• C#

External links

• Spec# website from Microsoft Research
• Spec# at Codeplex