Local Reasoning and Dynamic Frames for the Composite Pattern

Local Reasoning and Dynamic Frames for the Composite Pattern

Typ: Seminarthema Betreuer: P. H. Schmitt

Links: Paper

Einer der Fortschritte, welche die formale Programmverifikation in den letzten Jahren gemacht hat, besteht darin nicht nur Vor- und Nachbedingungen für Prozeduren (Methoden) zu betrachten, sondern auch die Spezifikation von Objekten, oder feinkörniger von "locations", die von einer Prozedur verändert werden und/oder von denen ihr Ergebniss abhängt. In der betrachteten Arbeit benutzen die Autoren dafür den Begriff "read-write-effects". Analog kann man auch, meist automatisch, ermitteln von welchen "locations" die Gültigkeit einer Formel der Spezifikationssprache abhängt. Damit lassen sich dann logische Schlüsse der folgenden Art ziehen:

• vor Ausführung der Prozedur P ist die Invariantenformel I wahr
• die Prozedur verändert nur die "locations" R1
• die Gültigkeit von I hängt höchstens von den "locations" R2 ab
• R1 und R2 sind disjunkt

dann gilt I auch nach Ausführung von P. Das erklärt das Konzept "local reasoning" im Titel der Arbeit. Der Text selbst beschreibt die Einzelheiten anhand eines durchgängigen Beispiels, der Spezifikation des "composite pattern".