Benutzer:Mr magic223325/SPARK (Programmiersprache)
| SPARK | |
|---|---|
| Paradigmen: | Multiparadigmatisch |
| Designer: | Altran, AdaCore |
| Aktuelle Version: | Community 2021 (1. Juni 2021) |
| Typisierung: | statisch, stark, sicher, nominal |
| Wichtige Implementierungen: | SPARK Pro, SPARK GPL Edition, SPARK Community |
| Beeinflusst von: | Ada, Eiffel |
| Betriebssystem: | Plattformübergreifend: Linux, Microsoft Windows, Mac OS X |
| Lizenz: | GPLv3 |
| About SPARK | |
SPARK ist eine formal definierte Programmiersprache, die auf der Programmiersprache Ada basiert und für die Entwicklung von sicherheitskritischer Software bestimmt ist, die in Systemen eingesetzt wird, bei denen ein vorhersehbarer und äußerst zuverlässiger Betrieb unerlässlich ist. Sie erleichtert die Entwicklung von Anwendungen, die Sicherheit, Schutz oder Integrität erfordern. Anwendungsgebiete für SPARK beinhalten sowohl zivile als auch militärische Avionik, Eisenbahnsignaltechnik und Satelliten.[1][2]
Ursprünglich gab es drei Versionen der Sprache (SPARK83, SPARK95, SPARK2005), die auf Ada 83, Ada 95 beziehungsweise Ada 2005 basierten.
Eine vierte Version, SPARK 2014, basierend auf Ada 2012, wurde am 30. April 2014 veröffentlicht. SPARK 2014 ist eine vollständige Neugestaltung der Sprache und der unterstützenden Verifikationswerkzeuge.
In SPARK83/95/2005 sind die Contracts in Ada-Kommentaren kodiert und werden daher von jedem Standard-Ada-Compiler ignoriert, aber vom SPARK-"Examiner" und seinen zugehörigen Werkzeugen verarbeitet.
SPARK 2014 verwendet dagegen die in Ada 2012 eingebaute "Aspekt"-Syntax, um Contracts auszudrücken, und bringt sie in den Kern der Sprache. Das Hauptwerkzeug für SPARK 2014 (GNATprove) basiert auf der GNAT/GCC-Infrastruktur und verwendet fast das gesamte GNAT Ada 2012 Front-End.
Technischer Überblick
[Bearbeiten | Quelltext bearbeiten]SPARK nutzt die Stärken von Ada und versucht gleichzeitig, alle potenziellen Mehrdeutigkeiten und unsicheren Konstrukte zu beseitigen. SPARK-Programme sind so konzipiert, dass sie eindeutig sind und ihr Verhalten von der Wahl des Ada-Compilers unbeeinflusst bleibt. Diese Ziele werden zum Teil durch den Verzicht auf einige der problematischeren Merkmale von Ada (wie zum Beispiel uneingeschränktes paralleles Tasking) und zum Teil durch die Einführung von Contracts erreicht, die die Absichten und Anforderungen des Anwendungsentwicklers für bestimmte Komponenten eines Programms kodieren.
Durch die Kombination dieser Ansätze kann SPARK seine Ziele erreichen, die da lauten:
- logische Korrektheit
- strenge formale Definition
- einfache Semantik
- Sicherheit
- Ausdruckskraft
- Überprüfbarkeit
- Laufzeit.
Contract Beispiele
[Bearbeiten | Quelltext bearbeiten]Gegeben sei die folgende Ada-Unterprogrammspezifikation:
procedure Erhöhe (X : in out Zähler_Typ);
In Standard-Ada könnte diese Prozedur die Variable X um eins oder tausend erhöhen; oder sie könnte eine globale Variable auf den Wert von X setzen und den ursprünglichen Wert der Variable zurückgeben; oder sie könnte überhaupt nichts mit X machen.
Mit SPARK 2014 wurden der Sprache Contracts hinzugefügt, die zusätzliche Informationen darüber liefern, was ein Unterprogramm tatsächlich tut. Zum Beispiel kann die obige Spezifikation wie folgt geändert werden:
procedure Erhöhe (X : in out Zähler_Typ)
with Global => null,
Depends => (X => X);
Dies legt fest, dass die Erhöhe-Prozedur keine globalen Variablen verwendet (weder aktualisiert noch liest) und dass der einzige Wert, der bei der Berechnung des neuen Wertes von X verwendet wird, X selbst ist.
Alternativ könnte der Entwickler auch angeben:
procedure Erhöhe (X : in out Zähler_Typ)
with Global => (In_Out => Zähler),
Depends => (Zähler => (Zähler, X),
X => null);
Dies legt fest, dass Erhöhe die globale Variable Zähler verwendet, die im gleichen Paket wie Erhöhe definiert ist, dass der exportierte Wert von Zähler von importierten Werten von Zähler und X überhaupt nicht von Variablen abhängt und nur von konstanten Daten abgeleitet wird.
Wenn GNATprove dann auf die Spezifikation und der entsprechenden Implementation eines Unterprogramms angewendet wird, analysiert es die Implementation des Unterprogramms, um ein Modell des Informationsflusses zu erstellen. Dieses Modell wird dann mit demjenigen verglichen, das durch die Anmerkungen spezifiziert wurde, und etwaige Diskrepanzen werden dem Benutzer mitgeteilt.
Diese Spezifikationen lassen sich weiter ausbauen, indem man verschiedene Eigenschaften festlegt, die entweder beim Aufruf des Unterprogramms erfüllt sein müssen (Preconditions) oder nach Abschluss der Ausführung erfüllt sein müssen (Postcondition). Folgendes Beispiel erweitert die vorherige Prozedur:
<syntaxhighlighting lang="ada"> procedure Erhöhe (X : in out Zähler_Typ)
with Global => null,
Depends => (X => X),
Pre => X < Zähler_Typ'Last,
Post => X = X'Old + 1;
</syntaxhighlighting>
Damit wird nicht nur festgelegt, dass X nur von sich selbst abgeleitet wird, sondern auch, dass X vor dem Aufruf von Erhöhe unbedingt kleiner als der letzte mögliche Wert des Types Zähler_Typ sein muss, damit ein Zählerüberlauf ausgeschlossen werden kann. Weiterhin muss der Wert von X nach dem Aufruf der Prozedur genau eins größer als der Wert vor Aufruf der Prozedur sein.
Überprüfungsbedingungen
[Bearbeiten | Quelltext bearbeiten]GNATprove kann auch einen Satz von Verifikationsbedingungen oder VCs erzeugen. Diese Bedingungen werden verwendet, um festzustellen, ob bestimmte Eigenschaften für ein bestimmtes Unterprogramm zutreffen. Mindestens erzeugt GNATprove VCs, um festzustellen, dass alle Laufzeitfehler in einem Unterprogramm nicht auftreten können, wie zum Beispiel:
- Array-Index außerhalb der Grenzen
- Verstoß gegen den Typenbereich
- Division durch Null
- Zählerüberlauf.
Wenn eine Postcondition oder eine andere Assertion zu einem Unterprogramm hinzugefügt wird, generiert GNATprove auch VCs, die vom Benutzer verlangen, dass er zeigt, dass diese Eigenschaften für alle möglichen Pfade durch das Unterprogramm gelten.
Intern verwendet GNATprove die Why3-Zwischensprache und den VC-Generator, sowie die CVC4-, Z3- und Alt-Ergo-Theorembeweiser, um VCs auszuführen. Die Verwendung anderer Beweiser (einschließlich interaktiver Theorembeweiser) ist auch durch andere Komponenten des Why3-Toolkits möglich.
Geschichte
[Bearbeiten | Quelltext bearbeiten]Die erste Version von SPARK (basierend auf Ada 83) wurde an der Universität von Southampton (mit Unterstützung des britischen Verteidigungsministeriums) von Bernard Carré und Trevor Jennings entwickelt. Der Name SPARK wurde von SPADE Ada Kernel abgeleitet, in Anlehnung an die SPADE-Untermenge der Programmiersprache Pascal.[3]
In der Folge wurde die Sprache schrittweise erweitert und verfeinert, zunächst von Program Validation Limited und dann von Praxis Critical Systems Limited. Im Jahr 2004 änderte Praxis Critical Systems Limited seinen Namen in Praxis High Integrity Systems Limited. Im Januar 2010 wurde das Unternehmen zu Altran-Praxis.
Anfang 2009 ging Praxis eine Partnerschaft mit AdaCore ein und veröffentlichte "SPARK Pro" unter den Bedingungen der GPL. Im Juni 2009 folgte die SPARK GPL Edition 2009, die sich an die FOSS- und akademische Gemeinschaft richtet.
Im Juni 2010 gab Altran-Praxis bekannt, dass SPARK in der Software des US-Mondprojekts CubeSat, das voraussichtlich 2015 abgeschlossen sein wird.
Im Januar 2013 änderte Altran-Praxis ihren Namen in Altran und wurde im April 2021 zu Capgemini Engineering (nach der Fusion von Altran mit Capgemini).
Die erste Pro-Version von SPARK 2014 wurde am 30. April 2014 angekündigt, und kurz darauf folgte die SPARK 2014 GPL Edition.
Industrielle Anwendungen
[Bearbeiten | Quelltext bearbeiten]Sicherheitsrelevante Systeme
[Bearbeiten | Quelltext bearbeiten]SPARK wurde in mehreren hochkarätigen sicherheitskritischen Systemen eingesetzt, darunter in der militärischen Luftfahrt (Eurofighter Typhoon, Lockheed Martin C130J) und in der Raumfahrt (CubeSat-Projekt des Vermont Technical College).[2][4]
Kategorie:Prozedurale Programmiersprache Kategorie:Imperative Programmiersprache Kategorie:Programmiersprache mit einem ISO-Standard Kategorie:Programmiersprache für besondere Aufgaben
- ↑ About SPARK. Abgerufen am 4. Dezember 2024 (englisch).
- ↑ a b A SPARK/Ada CubeSat Control Program. Abgerufen am 4. Dezember 2024 (englisch).
- ↑ SPARK - The SPADE Ada Kernel (including RavenSPARK). AdaCore, abgerufen am 5. Dezember 2024 (englisch).
- ↑ Roderick Chapman: Industrial Experience with SPARK. In: Ada Letters. 2000. Jahrgang, Nr. 4, S. 64 (englisch, sigada.org [PDF]).