Spec-Sharp – Wikipedia

Spec#
Paradigmen: Objektorientierte Programmiersprache
Erscheinungsjahr: 2004
Entwickler: Microsoft Research
Aktuelle Version: SpecSharp 2011-10-03  (7. Oktober 2011)
Typisierung: stark
Beeinflusst von: C#
Betriebssystem: alle mit CLR
research.microsoft.com/SpecSharp

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.

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 | Quelltext 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:

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!");     } } 

Einzelnachweise

[Bearbeiten | Quelltext bearbeiten]
  1. Spec#. In: Microsoft Research. Abgerufen am 16. Dezember 2018 (amerikanisches Englisch).