Top-Fragen
Zeitleiste
Chat
Kontext
Spec-Sharp
Programmiersprache Aus Wikipedia, der freien Enzyklopädie
Remove ads
Spec# ist eine von Microsoft Research entwickelte objektorientierte Programmiersprache, die eine Erweiterung zum etablierten C# ist[1]. Sie ist kostenlos und u. a. für die Entwicklungsumgebungen Microsoft Visual Studio 2003, 2005 und 2008 verfügbar und bildet zusätzlich den Grundstock für Sing#. Diese Sprache wurde für das Projekt Singularity entwickelt. Die Konzepte sind zum Teil als Code Contracts in Visual Studio 2010 eingeflossen.
Remove ads
Remove ads
Konzept
Spec# ist eine Erweiterung von C# um Vorbedingungen, Nachbedingungen, Non-Null-Types und Objektinvarianzen. Die Methodenbedingungen werden durch Kontrakte abgebildet und erweitern damit die Metabeschreibung eines Objekts. Zusätzlich werden Checked Exceptions implementiert. Die Erweiterungen sind durch den Spec#-Compiler möglich. Für die Absicherung wurde ein Theorembeweiser mit dem Codenamen Boogie implementiert.
Remove ads
Programmierbeispiel
Die folgenden Zeilen geben einen kleinen Einblick in den Aufbau und die Verwendung von Spec#. Hierbei handelt es sich um den Start-Quelltext, der von Visual Studio 2005 über den Projekt-Wizard für eine Konsolenanwendung generiert wird:
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!");
}
}
Remove ads
Siehe auch
Weblinks
Einzelnachweise
Wikiwand - on
Seamless Wikipedia browsing. On steroids.
Remove ads