Spec-Sharp
| Spec# | |
|---|---|
| [[Datei:Skriptfehler: Ein solches Modul „Wikidata“ ist nicht vorhanden.|150px]] | |
| Basisdaten | |
| Paradigmen: | Objektorientierte Programmiersprache |
| Erscheinungsjahr: | 2004 |
| Designer: | Skriptfehler: Ein solches Modul „Wikidata“ ist nicht vorhanden. |
| Entwickler: | Microsoft Research |
| Aktuelle Version: | SpecSharp 2011-10-03 (7. Oktober 2011) |
| Typisierung: | stark |
| Beeinflusst von: | C# |
| Betriebssystem: | alle mit CLR |
| Lizenz: | Skriptfehler: Ein solches Modul „Wikidata“ ist nicht vorhanden. |
| research.microsoft.com/SpecSharp | |
Spec# ist eine von Microsoft Research entwickelte objektorientierte Programmiersprache, die eine Erweiterung zum etablierten C# ist<ref>Skriptfehler: Ein solches Modul „Vorlage:Internetquelle“ ist nicht vorhanden. In: Skriptfehler: Ein solches Modul „Vorlage:Internetquelle“ ist nicht vorhanden. Ehemals im Vorlage:Referrer (nicht mehr online verfügbar) (Skriptfehler: Ein solches Modul „Multilingual“ ist nicht vorhanden.).Vorlage:Toter Link/Core (Seite nicht mehr abrufbar. Suche im Internet Archive)Skriptfehler: Ein solches Modul „TemplatePar“ ist nicht vorhanden.Skriptfehler: Ein solches Modul „TemplatePar“ ist nicht vorhanden.</ref>. 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.
Konzept[Bearbeiten]
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.
Programmierbeispiel[Bearbeiten]
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:
<syntaxhighlight lang="csharp"> 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!");
}
} </syntaxhighlight>
Siehe auch[Bearbeiten]
Weblinks[Bearbeiten]
- Offizielle Webseite (englisch)
- Expert to Expert: Contract Oriented Programming and Spec# (Erik Meijer im Gespräch mit den Spec#-Designern auf Channel9) (englisch)
- Code Contracts in .NET 4 (englisch)
Einzelnachweise[Bearbeiten]
<references />