You can edit almost every page by Creating an account. Otherwise, see the FAQ.

Spec Sharp

From EverybodyWiki Bios & Wiki


Spec#
Paradigmmulti-paradigm: structured, imperative, object-oriented, event-driven, functional, contract
Designed byMicrosoft Research
DeveloperMicrosoft Research
First appeared2004; 20 years ago (2004)
Stable release
SpecSharp 2011-10-03 / October 7, 2011; 13 years ago (2011-10-07)
Typing disciplinestatic, strong, safe, nominative
LicenseMicrosoft Research Shared Source license agreement (MSR-SSLA)
Websiteresearch.microsoft.com/specsharp/
Influenced by
C#, Eiffel
Influenced
Sing#

Search Spec Sharp on Amazon.

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.

Features[edit]

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

Example[edit]

This example shows two of the basic structures that are used when adding contracts to your code (try Spec# in your browser).

    static int Main(string![] args)
        requires args.Length > 0;
        ensures return == 0;
    {
        foreach(string arg in args)
        {
            Console.WriteLine(arg);
        }
        return 0;
    }
  • ! 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 precondition that must be followed in the code. In this case the length of args is not allowed to be zero or less.
  • ensures indicates a postcondition that must be followed in the code.

Sing#[edit]

Sing# is a superset of Spec#. Microsoft Research developed Spec#, and later extended it into Sing# in order to develop the Singularity operating system. Sing# augments the capabilities of Spec# with support for channels and low-level programming language constructs, which are necessary for implementing system software. Sing# is type-safe. The semantics of message-passing primitives in Sing# are defined by formal and written contracts.[citation needed]

Sources[edit]

  • 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[edit]

External links[edit]


This article "Spec Sharp" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Spec Sharp. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.