• 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. Deutsche Gesellschaft für Qualität - DGQ Service GmbH, Frankfurt am Main
  2. ALDI International Services GmbH & Co. oHG, Mülheim an der Ruhr, Düsseldorf, Dortmund, Duisburg

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.

Golem Akademie
  1. OpenShift Installation & Administration
    14.-16. Juni 2021, online
  2. PostgreSQL Fundamentals
    15.-18. Juni 2021, online
Weitere IT-Trainings

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
Spiele-Angebote
  1. 4,49€
  2. 7,49€
  3. 8,29€
  4. 5,99€

amagol 03. Sep 2020

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

TheNX 02. Sep 2020

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

igor37 02. Sep 2020

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

captain_spaulding 02. Sep 2020

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

captain_spaulding 02. Sep 2020

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


Folgen Sie uns
       


Mercedes EQA Probe gefahren

Wir sind mit dem EQA von Mercedes-Benz für ein paar Stunden unterwegs gewesen.

Mercedes EQA Probe gefahren Video aufrufen
Programm für IT-Jobeinstieg: Hoffen auf den Klebeeffekt
Programm für IT-Jobeinstieg
Hoffen auf den Klebeeffekt

Aktuell ist der Jobeinstieg für junge Ingenieure und Informatiker schwer. Um ihnen zu helfen, hat das Land Baden-Württemberg eine interessante Idee: Es macht sich selbst zur Zeitarbeitsfirma.
Ein Bericht von Peter Ilg

  1. Arbeitszeit Das Sechs-Stunden-Experiment bei Sipgate
  2. Neuorientierung im IT-Job Endlich mal machen!
  3. IT-Unternehmen Die richtige Software für ein Projekt finden

Weclapp-CTO Ertan Özdil: Wir dürfen nicht in Schönheit und Perfektion untergehen!
Weclapp-CTO Ertan Özdil
"Wir dürfen nicht in Schönheit und Perfektion untergehen!"

Der CTO von Weclapp träumt von smarter Software, die menschliches Eingreifen in der nächsten ERP-Generation reduziert. Deutschen Perfektionismus hält Ertan Özdil aber für gefährlich.
Ein Interview von Maja Hoock


    Fiat 500 als E-Auto im Test: Kleinstwagen mit großem Potenzial
    Fiat 500 als E-Auto im Test
    Kleinstwagen mit großem Potenzial

    Fiat hat einen neuen 500er entwickelt. Der Kleine fährt elektrisch - und zwar richtig gut.
    Ein Test von Peter Ilg

    1. Vierradlenkung Elektrischer GMC Hummer SUV fährt im Krabbengang seitwärts
    2. MG Cyberster MG B Roadster mit Lasergürtel und Union Jack
    3. Elektroauto E-Auto-Prämie übersteigt in 2021 schon Vorjahressumme

      •  /