Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Prüfungsprotokoll zu "Formale Methoden der Softwareentwicklung" (Übersicht)
no way to compare when less than two revisions
Unterschiede
Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.
— | pruefungen:hauptstudium:ls8:fm_ws1213_2 [27.03.2013 10:34] (aktuell) – angelegt iridium | ||
---|---|---|---|
Zeile 1: | Zeile 1: | ||
+ | ====== Prüfungsprotokoll zu " | ||
+ | * Prüfer: Lutz Schröder | ||
+ | * Beisitzer: Daniel Gorín | ||
+ | * Ergebnis: 1,0 (Gesamtnote, | ||
+ | * Sprache: Deutsch | ||
+ | |||
+ | Sehr angenehme Atmosphäre, | ||
+ | |||
+ | **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, | ||
+ | |||
+ | **Mit dem WP-Kalkül haben wir die relative Vollständigkeit von Hoare bewiesen. Warum relativ?** | ||
+ | Rumgestottert, | ||
+ | |||
+ | **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/ | ||
+ | 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, | ||
+ | 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, | ||
+ | |||
+ | **Wie kann ich jetzt da Model Checking für das EG\phi machen?** | ||
+ | Kurze Hänger, dennoch: Modell auf [[\phi]] einschränken, | ||
+ | |||
+ | **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, | ||
+ | |||
+ | 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). |