imported>SchlurcherBot: Bot: http → https

2025-09-27T09:20:22Z

Bot: http → https

Neue Seite

{{Korrekter Titel|Spec#}}

{{Infobox Programmiersprache
|Name=Spec#
|Logo =
|Beschreibung= Objektorientierte Programmiersprache
|Paradigma = [[Objektorientierte Programmiersprache]]
|Erscheinungsjahr = 2004
|Entwickler = [[Microsoft Research]]
|AktuelleVersion = SpecSharp 2011-10-03
|AktuelleVersionFreigabeDatum = 7. Oktober 2011
|Typisierung = [[Starke Typisierung|stark]]
|Implementierung =
|Dialekte =
|Beeinflusst_von =[[C-Sharp|C#]]
|Beeinflusste =
|Betriebssystem = alle mit [[Common Language Runtime|CLR]]
|Lizenz =
|Website = [https://research.microsoft.com/SpecSharp/ research.microsoft.com/SpecSharp]
}}

'''Spec#''' ist eine von [[Microsoft Research]] entwickelte [[Objektorientierte Programmierung|objektorientierte Programmiersprache]], die eine Erweiterung zum etablierten [[C-Sharp|C#]] ist<ref>{{Internetquelle |url=https://www.microsoft.com/en-us/research/project/spec/ |titel=Spec# |werk=Microsoft Research |zugriff=2018-12-16 |sprache=en-US}}</ref>.
Sie ist kostenlos und u. a. für die [[Integrierte Entwicklungsumgebung|Entwicklungsumgebungen]] [[Microsoft Visual Studio]] 2003, 2005 und 2008 verfügbar und bildet zusätzlich den Grundstock für [[Sing-Sharp|Sing#]]. Diese Sprache wurde für das Projekt [[Singularity (Microsoft)|Singularity]] entwickelt. Die Konzepte sind zum Teil als [[Code Contracts]] in Visual Studio 2010 eingeflossen.

== 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 [[Ausnahmebehandlung#Checked Exceptions|Checked Exceptions]] implementiert. Die Erweiterungen sind durch den Spec#-Compiler möglich. Für die Absicherung wurde ein [[Maschinengestütztes Beweisen|Theorembeweiser]] mit dem Codenamen Boogie implementiert.

== 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-[[Assistent (Datenverarbeitung)|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 ==
* [[Eiffel (Programmiersprache)]]

== Weblinks ==
* [https://research.microsoft.com/SpecSharp/ Offizielle Webseite] (englisch)
* [http://channel9.msdn.com/shows/Going+Deep/Expert-to-Expert-Contract-Oriented-Programming-and-Spec/ Expert to Expert: Contract Oriented Programming and Spec# (Erik Meijer im Gespräch mit den Spec#-Designern auf Channel9)] (englisch)
* [https://visualstudiomagazine.com/articles/2010/06/23/code-contracts.aspx Code Contracts in .NET 4] (englisch)

== Einzelnachweise ==
<references />

[[Kategorie:Objektorientierte Programmiersprache]]
[[Kategorie:.NET]]
[[Kategorie:Microsoft]]
[[Kategorie:Qualitätsmanagement (Softwaretechnik)]]

Spec-Sharp - Versionsgeschichte

imported>SchlurcherBot: Bot: http → https