 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | ||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
Formale Sprachen und Programmiersprachen |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| Programmiersprachen sind keine formalen Sprachen im engeren Sinne, da sie in der Regel keine exakt definierte Semantik haben. Probleme bereiten insbesondere C, C++ und Java.
Erfolgreiche Versuche werden hier unternommen, Ausschnitte von Programmiersprachen mit einer exakten Semantik zu versehen und diese sicherer zu gestalten. Beispiele hierfür sind MISRA-C. MISRA-C verbietet beispielsweise einige problematische Konstrukte wie unbegrenzte Pointer-Arithmetik. SPARK ist ein weiteres Beispiel, es basiert auf ADA. Beide Sprachen werden vor allem im militärischen Bereich verwendet. (Siehe hierzu auch den Artikel von Amey. ) Statische Analyse Statische Analyse ist ein einfaches Verfahren um Programmcode in C, ADA, Java oder anderen Sprachen auf bestimmte Eigenschaften hin zu untersuchen. Gefunden werden über die statische Analyse unter anderem nicht verwendete Variablen, nicht erreichbarer Code oder unpassende Typkonvertierungen. Werkzeuge zur statischen Analyse haben den Vorteil, dass sie ohne besonderen Aufwand in Einarbeitung und Anwendung auch von Laien verwendet werden können. Auf dem OpenSource Markt ist PMD ein Beispiel für ein frei verfügbares Werkzeug zur statischen Analyse. PMD überprüft üblichen Java-Code auf nicht benutzte lokale Variablen, leere Catch-Blöcke, leere If-Befehle, doppelte Import-Befehle, nicht verwendete Parameter usw. Lint erlaubt die statische Analyse von C-Programmen. Lint findet nicht verwendete Variable, nicht verwendeten Code, nicht erlaubte Typ-Konvertierungen usw. . Verschiedene Varianten von Lint sind kommerziell verfügbar. Eine Übersicht zu statischen Analysewerkzeugen findet sich im Internet auf den Seiten der Testingfaqs. Anreicherungen von Programmiersprachen mit zusätzlichen Konstrukten erlauben mehr Sicherheit vor Fehlern und weitere Verifikationsmöglichkeiten. Ansätze sind hier beispielsweise Java-Programme mit Invarianten, Vor- und Nachbedingungen anzureichern. Auf den so erweiterten Programmen arbeiten Werkzeuge zur statischen Analyse, die Eigenschaften des Codes überprüfen und übliche Programmierfehler und Verletzungen von Invarianten zur Compile-Zeit finden. Die Analyse des Codes kann über automatische Model Checker oder Theorem-Beweiser geschehen. ESC-Java von Compaq-Researach ist ein Beispiel. Abstrakte Interpretationen Abstrakte Interpretationen sind (automatisch erzeugte) mathematische Modelle des Verhaltens von Quelltexten. Das Modell beschreibt das Verhalten angenähert und erlaubt Aussagen über das Verhalten des späteren Systems. Laufzeitfehler werden über diesen Ansatz identifiziert, Code-Optimierung ist möglich, in Einzelfällen sind auch Korrektheitsbeweise durchführbar. Abstrakte Interpretationen sind ein Mittel zur statischen Analyse. Polyspace bietet beispielsweise ein Werkzeug an, das auf Abstrakten Interpretationen basiert und bei mehreren Kunden zur Qualitätsverbesserung von Embedded-Software verwendet wird. Das Werkzeug ist für die Programmiersprachen C und ADA verfügbar. | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| Formale Sprachen und... | ||||
| ||||
| ||||
| ||||
| ||||
| Ansprechpartner | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| Weitere Themen | | ||
| ||||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
