Boolean Expression

5.1 Zustandsbasierte Spezifikationen

Zustandsbasierte Spezifikationen beschreiben Softwaresysteme in Form von Zuständen und Auswirkungen von Operationen auf Zustände. Solche Spezifikationen werden von mehreren Spezifikationssprachen unterstützt, die wir in zwei Gruppen einteilen: klassische Spezifikationssprachen, wie Z , B und VDM , und Assertionssprachen, wie Eiffel , JML (Java Modeling Language) und Peters und Parnas‘ Tabellen . Während klassische Spezifikationssprachen Zustände und Übergänge unabhängig von der Implementierung definieren, spezifizieren Assertionssprachen Zustände und Übergänge als Anweisungen oder Annotationen des Quellprogramms.

Zustandsbasierte Spezifikationen werden als Testorakel verwendet, indem die Übereinstimmung der Testausführungen mit den Spezifikationen überprüft wird. Das Hauptproblem bei der Generierung von Testorakeln aus zustandsbasierten Spezifikationen ergibt sich aus den unterschiedlichen Abstraktionsebenen zwischen den Spezifikationen und den während der Testausführung überwachten Operationen; daher werden die Spezifikationen der Operationen in eine überprüfbare Form übersetzt. Die Spezifikationssprachen sind in der Regel ausdrucksstark genug, um verschiedene Datenstrukturen und zustandsbasierte Eigenschaften darzustellen, aber ihre Ausdruckskraft erschwert die Übersetzung in eine ausführbare Form. Oft werden bei der Übersetzung einige vereinfachende Annahmen getroffen, wie z.B. die Begrenzung unendlicher Mengen, z.B. die unendliche Menge der natürlichen Zahlen, und die Behandlung nicht ausführbarer Elemente, die nur teilweise und manchmal nur durch menschliches Eingreifen erfolgen kann.

Hier werden die wichtigsten Ansätze zur Übersetzung zustandsbasierter Spezifikationen in eine ausführbare Form diskutiert. Die Übersetzung von Z-, B- und VDM-Spezifikationen weist die gleichen Probleme auf, die mit unendlichen Datenstrukturen, teilweise definierten Ausdrücken und objektorientierten Strukturen zusammenhängen. Die Übersetzung von Eiffel, JML und anderen Assertion-Sprachen in eine überprüfbare Form stellt ähnliche Probleme dar, allerdings auf einer anderen Abstraktionsebene. Im Folgenden stellen wir die wichtigsten Ansätze zur Übersetzung zustandsbasierter Spezifikationen in überprüfbare Form in Bezug auf Z vor; die Ansätze für andere Sprachen sind ähnlich. Anschließend diskutieren wir die Probleme der Kompilierung von Assertions in ausführbare Checks mit Bezug auf Eiffel, JML und Peters und Parnas‘ Tabellen.

Objektorientierte Erweiterungen von Z, wie Object-Z, verschärfen die Probleme. McDonald et al. übersetzen Ojbect-Z-Spezifikationen von Containerklassen in drei Schritten in C++-Code: Optimierung, strukturelles Mapping und Prädikatsübersetzung. In der Optimierungsphase ordnen sie die Spezifikation neu an, um die anschließende Übersetzung durch mehrere Schritte zu vereinfachen, einschließlich des Ersetzens konstanter Variablen durch ihre Werte und des Entfernens sekundärer Variablen und Schemaanreicherungen. In der Phase des strukturellen Mappings werden die Strukturen der Object-Z-Spezifikation auf die entsprechenden Codeelemente abgebildet: Spezifikationskonstanten und -variablen auf Variablen mit geeigneten Initialisierungen und Variablentypen auf primitive C++-Typen oder entsprechende Klassen in der von der Technik verwendeten Z-Toolkit-Bibliothek. So werden zum Beispiel die Typen integer und boolean auf int und der Typ von integer sets auf z_set<int > abgebildet. Sie bilden das Initialisierungsschema auf einen Konstruktor und die Operationsschemata auf Mitgliedsfunktionen ab, erstellen eine spezielle Mitgliedsfunktion inv(), um die Klasseninvariante zu prüfen, und generieren eine Ausnahmeklasse für jedes Ausnahmeschema.

Bei der Übersetzung des Prädikats DeepL konzentriert sich die Technik auf die Generierung von Code zur Überprüfung des Programmzustands anstelle der Auswertung von Prädikaten. Die Übersetzung verhindert zum Beispiel, dass die Funktion inv() eine andere Mitgliedsfunktion aufruft, um eine unendliche Rekursion zu vermeiden. In einem Konstruktor wird die Klasseninvariante bei dessen Beendigung geprüft.

Richardson et al. konzentrieren sich auf zeitkritische Systeme, behandeln eine Kombination aus Z- und temporaler Intervalllogik und schlagen eine Übersetzung von Spezifikationen in Testorakel mittels symbolischer Interpretation vor. Die symbolische Interpretation ordnet die symbolischen Namen in den Spezifikationen den Stimuluseingängen und den anfänglichen Zustandsvariablen zu, indem sie sich auf die Daten- und Kontrollmappings bezieht. Dann interpretiert die symbolische Interpretation jeden Kontrollpfad in den Spezifikationen, d. h. sie erstellt eine Behauptung, die die Bedingung für die Spezifikationsdaten auf der Grundlage des symbolischen Zustands an jedem Spezifikationskontrollpunkt ausdrückt. Ein Spezifikationskontrollpunkt ist ein relevantes Element, wie z.B. ein parametrisiertes Ereignis, eine Transition und eine Operation. Nach der symbolischen Interpretation der Z-Spezifikation wird die Orakelinformation als eine Liste relevanter Z-Schemata und ihrer entsprechenden Assertionen dargestellt, die geprüft werden, wenn das Schema aufgerufen wird. Die Ausführung eines Testfalls bezieht sich auf eine konkrete Testeingabe, aus der konkrete Variablen und Ereignisse an ihre Entsprechungen in der Testklasse gebunden werden (jede Testklasse ist eine Partition der Testeingabe). Die Ausführung des Testfalls erzeugt ein Ausführungsprofil, und die im Ausführungsprofil enthaltenen konkreten Ereignisse und Werte von Variablen werden auf die Orakel-Ebene abgebildet, um ihre Konsistenz mit den Orakel-Informationen zu überprüfen.

Assertion-Sprachen verschmelzen Spezifikationen mit dem Quellcode, wodurch das Übersetzungsproblem zwar vereinfacht, aber nicht beseitigt wird. Assertions werden von verschiedenen Sprachen und Methodiken unterstützt. Design by contract ist ein Softwareentwurfsparadigma, das den gemeinsamen Entwurf von Code und Assertions postuliert. Design by contract wurde von Meyer vorgeschlagen und wird von der Programmiersprache Eiffel vollständig unterstützt. Im Gegensatz zu allgemeinen Spezifikationssprachen wie Z werden die Spezifikationen in Eiffel, die Verträge genannt werden, in den Quellcode integriert und definieren die Verpflichtungen und Vorteile der Softwarekomponenten, die über gut gestaltete Schnittstellen kommunizieren. In Sprachen, die Verträge unterstützen, werden die Verpflichtungen und Vorteile der Kunden als Vor- und Nachbedingungen der Dienstanbieter ausgedrückt. Der Quellcode wird mit Invarianten angereichert, die Zustandseigenschaften darstellen, die bei jeder Interaktion gegeben sein müssen.

Verträge wurden auf viele Sprachen ausgeweitet. iContract war das erste Werkzeug, das Verträge in Java unterstützte. In iContract werden Verträge als Code-Kommentare mit speziellen Tags geschrieben. Bei den von iContract unterstützten Verträgen handelt es sich um boolesche Ausdrücke, die der Java-Syntax entsprechen, mit Ausnahme einiger syntaktischer Erweiterungen, zu denen die universelle Quantifizierung (∀), die Existenzquantifizierung (∃) und die Implikation (→) gehören. Diese Erweiterungen wurden entwickelt, um die Übersetzung in Java-Code zu vereinfachen. Ein Beispiel, the syntax of ∀ is forall < Class >< var > in < Enum >< Exp_var >, where < Class > is the type of the variable < var >, which represents an element of < Enum >. A reasonable translation of the ∀ expression is to use a Java loop to iterate over the enumeration < Enum > and evaluate the boolean expression < Exp_var > in each iteration. The existential quantification is translated similarly. An implication expression C implies I can be simply translated into an if statement: „if C then check I.“

JML ist eine populäre Sprache zur Spezifikation von Verhaltensweisen, die Design by Contract in Java unterstützt. JML-Verträge haben in Java die Form von speziellen Kommentaren. JML drückt Vorbedingungen, Nachbedingungen und Invarianten als boolesche Ausdrücke aus, denen die Schlüsselwörter requires, ensures bzw. invariant vorangestellt sind, und verwendet die eingebaute Methode \ old(x), um den Wert von x vor einer Operation darzustellen. Ähnlich wie die ▵-Notation in Z bietet JML das Schlüsselwort modifies, um die Variablen anzugeben, die in einem Methodenkörper geändert werden. Darüber hinaus befasst sich JML mit mehreren objektorientierten Merkmalen, wie Sichtbarkeit und Vererbung.

JML ist die Grundlage vieler Ansätze zur Testorakelgenerierung. Bhorkar schlug eine Technik zur Übersetzung von JML-Verträgen in Java-Assertions vor. Obwohl diese Technik nur Vorbedingungen unterstützt, behandelt sie Probleme im Zusammenhang mit reinen Spezifikationsvariablen, Verfeinerung, Spezifikationsvererbung und Privatsphäre. Ähnlich wie iContract behandelt die Technik die Vererbung von Verträgen, indem sie die Verträge entsprechend ihrer Typen verbindet und trennt. Die Technik verwendet außerdem eine Hashtabelle (pro Thread), um Rekursionen bei der Laufzeitüberprüfung zu vermeiden. Ausdrücke, die Quantoren verwenden, werden von der Technik als nicht ausführbar betrachtet, und es wird kein Java-Code für solche Ausdrücke generiert.

Korat hat eine Technik vorgeschlagen, um sowohl Testfälle als auch Orakel aus JML-Spezifikationen zu generieren. Korats Technik generiert Testfälle aus Vorbedingungen und Invarianten und Orakel aus Nachbedingungen und Invarianten. Araujo et al. erweiterten JML um nebenläufige Verträge und schlugen eine Laufzeitunterstützung vor, um die Überprüfung von Behauptungen, die nebenläufige Eigenschaften spezifizieren, zur Laufzeit zu ermöglichen.

Peters und Parnas stellten einen Ansatz vor, um Testorakel aus formaler Dokumentation zu generieren. Die Dokumentation ist in einer tabellarischen Form gegeben, die aus Relationen besteht, die die Schnittstellen von Prozeduren spezifizieren und in Orakel in C und C++ Code übersetzt werden. Das Kernelement der formalen Dokumentation besteht aus Prädikatenausdrücken, die in einer Variante der Prädikatenlogik mit speziellen Konstrukten zur Behandlung von Teilfunktionen geschrieben sind. Ähnlich wie andere spezifikationsbasierte Orakeltechniken behandelt diese Technik Quantoren, indem sie sie auf endliche Mengen einschränkt.

I, G und Q müssen so definiert werden, dass sie eine spezielle Bedingung erfüllen, die sicherstellt, dass die konstruierte Menge S endlich ist.

Peters und Parnas schlagen einen Ansatz zur Übersetzung der tabellarischen Dokumentationen in C-Code vor. Da die Form der in den Dokumentationen verwendeten Ausdrücke gut definiert ist, erfolgt die Übersetzung systematisch.

Auch andere zustandsbasierte Spezifikationen werden zur Ableitung von Testorakeln verwendet. UML-Modelle sind im Allgemeinen informell; dennoch haben Bouquet et al. eine Untermenge der UML 2.1, genannt UML-MBT, definiert, die präzise genug für die automatische Generierung von Testfällen ist. UML-MBT enthält Klassendiagramme, Zustandsautomaten und eine Teilmenge von OCL 2.0. Bouquet et al. verwenden in VDM-SL geschriebene Spezifikationen, um Testorakel zu generieren.