• IT-Karriere:
  • Services:

... und was ist jetzt Spark?

Spark ist eine Teilmenge von Ada, jedes Spark-Programm ist auch ein gültiges Ada-Programm. Spark ist also im Wesentlichen die gleiche Sprache wie Ada, die Werkzeuge wie IDE und Compiler sind auch identisch.

Stellenmarkt
  1. Transdev Vertrieb GmbH, Leipzig
  2. Radeberger Gruppe KG, Frankfurt am Main

Es gibt jedoch in Spark einige zusätzliche Regeln, die befolgt werden müssen. Das Ziel von Spark ist dabei, Ada so zu beschränken, dass Spark-Programme mehr Garantien bieten können, als es für normale Ada-Programme möglich wäre.

Als Belohnung für die Einhaltung dieser strikten Regeln gibt es beim Programmieren in Spark ein neues Werkzeug: die Möglichkeit der formalen Verifikation. Sie kommt in Form eines zusätzlichen Menüs in der Entwicklungsumgebung. Wird mithilfe dieses Menüs die Verifikation durchgeführt, kann Spark automatisch potenzielle Programmierfehler wie arithmetische Überläufe und Pufferüberläufe signalisieren. Meldet Spark keine Fehler, dann können die von Spark überprüften Fehlersituationen nicht auftreten - und das gilt für alle möglichen Eingaben des Programms.

Spark ermöglicht auch das Hinzufügen sogenannter Verträge. Das sind Bedingungen, die vor beziehungsweise nach der Ausführung einer Funktion gültig sein sollen. Im Idealfall kann man hier direkt Anforderungen an die Software ausdrücken.

Wurden Verträge hinzugefügt, werden diese in den Verifikationsprozess einbezogen und möglicherweise inkorrekte Verträge signalisiert. Wieder gilt: Wenn Spark keine Fehler findet, dann sind diese Bedingungen korrekt, und zwar für alle möglichen Eingaben des Programms.

C, Ada und Spark kombinieren

C, Ada und Spark schließen sich gegenseitig nicht aus. Im Gegenteil: Es kann viel Sinn ergeben, Ada, Spark und C zusammen einzusetzen.

Zum Beispiel könnte Ada als Basis ausgewählt werden, denn es bietet einen guten Kompromiss zwischen Sicherheit und Komfort. Spark wäre für hochkritische Teile des Produkts am besten geeignet.

Mancher Code muss ohnehin in C sein, um zum Beispiel gewisse Systemaufrufe oder Bibliotheken benutzen zu können. Ein ähnliches Konzept wurde zum Beispiel im Wookey-Projekt umgesetzt, das auch Rust für einige Komponenten verwendet.

Programming in Ada 2012

Fazit

Zu oft steht die Wahl der Programmiersprache entweder schon vor Projektstart fest oder es wird sehr zeitig im Projekt nach externen Faktoren entschieden. Zu selten werden jedoch die Anforderungen der Software selbst zur Entscheidung hinzugezogen. In sicherheitsrelevanten Bereichen ist das fatal, denn gerade die oft gewählte Programmiersprache C ist dafür nicht so gut geeignet, es gibt bessere Lösungen.

Moderne Programmiersprachen können durch Vermeidung ganzer Klassen von Fehlern direkt zur Erfüllung von Software-Anforderungen beitragen. Nämlich genau dann, wenn die Vermeidung von solchen Fehlern Teil der Anforderungen ist. Mit fortgeschrittenen Technologien wie Spark können sogar funktionale Anforderungen für alle Eingaben garantiert werden.

Johannes Kanig ist Experte für statische Analysen und Formale Verifikation. Seit 2011 ist er Senior Software Engineer bei AdaCore und entwickelt dort die Spark-Software zur formalen Verifikation von Ada- und Spark-Programmen. Er schreibt regelmäßig Artikel über Ada und Spark auf Basis seiner umfangreichen Erfahrung.

Bitte aktivieren Sie Javascript.
Oder nutzen Sie das Golem-pur-Angebot
und lesen Golem.de
  • ohne Werbung
  • mit ausgeschaltetem Javascript
  • mit RSS-Volltext-Feed
 Warum nicht einfach C?
  1.  
  2. 1
  3. 2
  4. 3


Anzeige
Top-Angebote
  1. 299,99€ (Release 10.11.)
  2. 299,99€ (Release 10.11.)
  3. 299,99€ (Release 10.11.)
  4. 299,99€ (Release 10.11.)

amagol 03. Sep 2020 / Themenstart

Eine C/C++ library kann man in den meisten Faellen auch von anderen Sprachen aus...

TheNX 02. Sep 2020 / Themenstart

Ich habe mich mal für Ada im kommerziellen Bereich interessiert. Kurzum, die Situation...

igor37 02. Sep 2020 / Themenstart

Jede gefundene Lücke basierend auf ungültigen Pointerzugriffen, data races...

captain_spaulding 02. Sep 2020 / Themenstart

Dann eben neu. Von Pascal hab ich schon lang nichts mehr gelesen und hab es im Job oder...

captain_spaulding 02. Sep 2020 / Themenstart

Ist aus Safety/Security-Sicht quatsch. Es kommt auf die Fehlerhäufigkeit an. Fehler in...

Kommentieren


Folgen Sie uns
       


Zwischenzertifikate: Zertifikatswechsel bei Let's Encrypt steht an
Zwischenzertifikate
Zertifikatswechsel bei Let's Encrypt steht an

Bisher war das Let's-Encrypt-Zwischenzertifikat von Identrust signiert. Das wird sich bald ändern.
Von Hanno Böck

  1. CAA-Fehler Let's-Encrypt-Zertifikate werden nicht sofort zurückgezogen
  2. TLS Let's Encrypt muss drei Millionen Zertifikate zurückziehen
  3. Zertifizierung Let's Encrypt validiert Domains mehrfach

MX 10.0 im Test: Cherrys kompakte, flache, tolle RGB-Tastatur
MX 10.0 im Test
Cherrys kompakte, flache, tolle RGB-Tastatur

Die Cherry MX 10.0 kommt mit besonders flachen MX-Schaltern, ist hervorragend verarbeitet und umfangreich programmierbar. Warum Nutzer in Deutschland noch auf sie warten müssen, ist nach unserem Test unverständlich.
Ein Test von Tobias Költzsch

  1. Argand Partners Cherry wird verkauft

Probefahrt mit Citroën Ami: Das Palindrom auf vier Rädern
Probefahrt mit Citroën Ami
Das Palindrom auf vier Rädern

Wie fährt sich ein Elektroauto, das von vorne und hinten gleich aussieht und nur 7.000 Euro kostet?
Ein Hands-on von Friedhelm Greis

  1. Umweltschutz Großbritannien will Verbrenner ab 2030 verbieten
  2. Elektroautos Förderung privater Ladestellen noch für 2020 geplant
  3. Zulassungsrekord Jeder achte neue Pkw fährt elektrisch

    •  /