... 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. JavaScript-Entwickler (m/w/d)
    tangro software components GmbH, Heidelberg
  2. IT Consultant / Projektleiter Warenwirtschaft (m/w/d) Anwendungs- und Organisationsberatung ... (m/w/d)
    Infokom GmbH, deutschlandweit
Detailsuche

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. ITIL 4® Foundation: virtueller Zwei-Tage-Workshop
    16.–17. Dezember 2021, virtuell
  2. AZ-104 Microsoft Azure Administrator: virtueller Vier-Tage-Workshop
    13.–16. Dezember 2021, virtuell
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


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...



Aktuell auf der Startseite von Golem.de
Pornhub, Youporn, Mydirtyhobby
Gericht bestätigt Zugangsverbot für Pornoportale

Die Landesmedienanstalt NRW hat zu Recht gegen drei Pornoportale mit Sitz in Zypern ein Zugangsverbot verhängt.

Pornhub, Youporn, Mydirtyhobby: Gericht bestätigt Zugangsverbot für Pornoportale
Artikel
  1. Zip: Ratenzahlung in Microsoft Edge empört die Community
    Zip
    Ratenzahlung in Microsoft Edge empört die Community

    Die App Zip wird seit Microsoft Edge 96 standardmäßig aktiviert. Diese bietet Ratenzahlung an, schürt aber nur Hass in der Community.

  2. Kompakter Einstieg in die Netzwerktechnik
     
    Kompakter Einstieg in die Netzwerktechnik

    Die Golem Akademie bietet Admins und IT-Sicherheitsbeauftragten in einem Fünf-Tage-Workshop einen umfassenden Überblick über Netzwerktechnologien und -konzepte.
    Sponsored Post von Golem Akademie

  3. Razer Zephyr im Test: Gesichtsmaske mit Stil bringt nicht viel
    Razer Zephyr im Test
    Gesichtsmaske mit Stil bringt nicht viel

    Einmal Cyberpunk mit Beleuchtung bitte: Tragen wir Razers Zephyr in der U-Bahn, fallen wir auf. Allerdings ist das Produkt nicht ausgereift.
    Ein Test von Oliver Nickel

Du willst dich mit Golem.de beruflich verändern oder weiterbilden?
Zum Stellenmarkt
Zur Akademie
Zum Coaching
  • Schnäppchen, Rabatte und Top-Angebote
    Die besten Deals des Tages
    Daily Deals • Last Minute Angebote bei Amazon • Crucial-RAM zu Bestpreisen (u. a. 16GB Kit DDR4-3600 73,99€) • HP 27" FHD 165Hz 199,90€ • Razer Iskur X Gaming-Stuhl 239,99€ • Adventskalender bei MM/Saturn (u. a. Surface Pro 7+ 849€) • Alternate (u. a. Adata 1TB PCIe-4.0-SSD für 129,90€) [Werbung]
    •  /