Spec Sharp
| Paradigm(s) | 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.
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.
Contents |
[edit] Features
- See also: Spec# in C Sharp syntax.
Spec# extends the core C# programming language with features such as:
- Non-nullable types
- Structures for code contract like preconditions and postconditions.
- Checked exceptions similar to those in Java.
- Convenient syntax
[edit] Example
This example shows two of the basic structures that are used when adding contracts to your code (try Spec# in your browser).
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.
[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
|
|||||||||||||||||||||||||||||||||||||||||
 |
This programming language-related article is a stub. You can help Wikipedia by expanding it. |
