Prüfungsprotokoll zu "Formale Methoden der Softwareentwicklung"

• Prüfer: Lutz Schröder
• Beisitzer: Daniel Gorín
• Ergebnis: 1,0 (Gesamtnote, zu 75% beeinflusst durch Übungsabgaben)
• Sprache: Deutsch

Sehr angenehme Atmosphäre, Stift und Papier lagen bereit und waren auch notwendig. Fragen hat alle Prof. Schröder gestellt.

Frage des Prüfers / Antworten und Kommentare

Wir haben Hoare-Kalkül besprochen, können Sie dazu was sagen? Hoare-Tripel hingemalt, partiell und total.

Erklären Sie doch mal die Semantik davon Wenn A gilt und C terminiert, …

Gut, es gab da nun mal einige Regeln, schreiben Sie doch mal die Regeln für Schleifen hin Erstmal im Partiellen: (while-Regel hingeschrieben)

Aus der Aussage, mal nur im Partiellen schließe ich, Sie können das auch im Totalen (Hingeschrieben). War keine weitere Erklärung verlangt.

Es gibt da noch das WP-Kalkül, was ist das denn so? Rückwärtseinsetzen, schwächste Vorbedingung zu gegebener Nachbedingung herleiten.

Mit dem WP-Kalkül haben wir die relative Vollständigkeit von Hoare bewiesen. Warum relativ? Rumgestottert, mit Schröders Hilfe: {Top} C {Bottom} ist Tripel für nicht-terminierendes Programm, wenn ich das herleiten kann, habe ich die Terminierung bewiesen. (In diesem Kontext auch gefragt gewesen: Weakening-Regel hinschreiben. Weiterhin wichtig: Programmzustand ist Abbildung von Variablen auf natürliche Zahlen. Natürliche Zahlen sind in Prädikatenlogik 1. Stufe nicht vollständig beschreibbar, wir nutzen sie aber in unseren Aussagen). (Der Teil hat viel Zeit in Anspruch genommen, dabei auch einige Teilfragen wie „was haben wir sonst noch bewiesen (Korrektheit natürlich).)

Bis auf Schleifen ist das ja recht angenehm, schreiben Sie mal die rekursive Ersetzungsregel dafür hin wp(C1; C2, B) = wp(C1, wp(C2, B))

Gut. Wir haben uns mit Boogie beschäftigt. Es gibt da ja einige interessante Statements, was ist z.B. das assume? Können Sie die genaue Semantik davon hinschreiben? wp(assume A, B) = A ⇒ B

Warum ist das seltsam/kein richtiges, deterministisches Statement, wie man es von einem wohlgeformten Programm erwarten würde? wp(assume \bottom, \bottom) = \top, was ja so nicht geht. Annahmen entgegen meiner Nachbedingung möglich, Erfüllung der unmöglichen Nachbedingung.

Beweise funktionieren in Boogie ja mit einigen Tricks und Umschreibungen. Können Sie notieren, wie das mit Schleifen funktioniert? Ersetzungsregel für Schleifen hingeschrieben und relativ ausführlich erklärt (Nichtdeterminismus durch havoc, …)

Wir hatten uns noch mit Model Checking beschäftigt, insbesondere mit Temporallogiken. Welche kennen Sie denn da so? LTL, CTL, CTL*

Beginnen wir mit LTL, schreiben Sie doch mal hin, was da so die Syntax ist \phi UND \psi | p | X\phi | \phi U \psi Daraus per Abkürzung den Rest.

Wie unterscheidet sich das jetzt von CTL*? In CTL* gibts noch A[\phi] und E[\phi] (All- und Existenzquantor). A[\phi] mit \phi \in LTL ist die Entsprechung von \phi in CTL*, deshalb LTL Teilmenge CTL*.

Und was ist die Einschränkung für CTL? All- und Existenzquantor immer abwechselnd.

Sagt Ihnen die Fixpunktcharakterisierung von CTL noch etwas? EG\phi = .. und E \phi U \psi = … hingeschrieben, kurz erklärt.

Wie kann ich jetzt da Model Checking für das EG\phi machen? Kurze Hänger, dennoch: Modell auf \phi einschränken, SCCs berechnen, schauen, ob ich einen Pfad zu einer SCC habe.

Was ist Fairness? Menge von Formeln, jede muss unendlich oft gelten.

Und wie funktioniert das Model Checking mit Fairness? Mit Hilfe: Ich muss auf die SCCs einschränken, die jede Formel mindestens einmal erfüllt.

Insgesamt extrem faire Prüfung, habe ein paar Hänger gehabt, aber mit Schröders Hilfe eigentlich immer die Kurve gekriegt. In Anbetracht dessen zuvorkommende Benotung (wie oben bereits erwähnt allerdings ggf. auch durch Übungsabgaben beeinflusst).