Prüfungsprotokoll zu "Formale Methoden der Softwareentwicklung"

• Prüfer: Lutz Schröder
• Beisitzer: Daniel Gorín
• Ergebnis: 1.7

Fragen des Prüfers Antworten meinerseits

In der VL definierte imperative Sprache, dazu denotationelle Semantik
aufm schlauch gestanden

Was ist denn ein Modell Zustand, d.h. Belegung aller Variablen im Programm

Hoare-Kalkül, zunächst mal Syntax Hoare-Tripel, geschweifte klammern für partielle, eckige für totale Korrektheit

ok, Semantik d. Hoare-Kalküls Hoare-Tripel {A} C {B} sagt „wenn vorher A gilt und C terminiert, gilt danach B“. bei totalen Tripeln [A] C [B] „wenn vorher A gilt terminiert C auf jeden fall und hinterher gilt B“

herleitungsregel für schleifen-korrektheit im hoare-kalkül
{A && E} C {A}
——————— (while)
{A} while(E) {C}; {A && not E}

wieso darf ich da „&& E“ bzw. am ende „&& not E“ hinschreiben? wenn am anfang nicht E gilt, wird C eh ned ausgeführt und es is egal, am ende muss „not E“ gelten weil die schleife solange läuft, wie E gilt, falls sie terminiert gilt dannach not E, falls nicht is eh egal was dannach steht

ok, wie macht man den Schritt auf totale korrektheit man fügt zur vorbedingung ein V = x und zur nachbedingung ein V < x hinzu, so dass V nach 0 gehen muss. wir ham noch bissl rum was V sein muss, weil ich zuerst nur ganzzahl gesagt hab, aber wenn man ne schon negative zahl runterzählt bis sie 0 is, zählt man ziemlich lang..

dann ham wir uns ja noch mit dem wp-kalkül beschäftigt, wie geht des so? quasi rückwärtseinsetzen des codes, um aus einer gegebenen nachbedingung eine schwächste vorbedingung zu erhalten, so dass die nachbedingung gilt

was ham wir mit dem wp-kalkül fürs hoare-kalkül bewiesen wusst ich ned, antwort wäre relative vollständigkeit gewesen

ok, dann hatten wir ja noch model-checking und temporallogiken, welche gabs da so? LTL, CTL, CTL*

ja, wie sieht die syntax von LTL aus? logische operatoren: not, oder
temporal-operatoren: X(next) und U(until)
und dadraus halt G(generally) und F(finally)

machen sie mal so formeln mit X und U nagut, X phi und phi U psi, erklärt was des jew. heißt

ok, wenn sie jetz ein modell (malt hin: p mit self-loop, pfeil nach not p welches auch self-loop hat) und die formel GF(not p) haben, is die dann erfüllt? nein, weil nicht garantiert ist dass irgendwann mal der pfad zu not p genommen wird
in LTL is ja eine formel implizit über alle pfade allquantifiziert, d.h. ein nicht-erfüllender pfad macht die ganze aussage halt falsch.

genau, wie kann man des besser machen? CTL hat pfadquantoren A und E, angelehnt an die all- und existenzquantoren aus der klassischen logik, mit denen man dan sagen kann EGF(not p), was erfüllt wäre.

kann ich die pfad-quantoren beliebig irgendwohin schreiben? in CTL nicht, immer nur gepaart mit einem temporaloperator. in CTL* egal wo.

wie war das denn mit der fixpunktiteration? kurz skizziert, dass man halt mit nix anfängt, und induktiv quasi immer was in einem schritt vom bisherigen aus erreichbar ist dazu nimmt und irgendwann keine änderung mehr hat ⇒ fixpunkt

joa, dann können sie mal kurz rausgehn..

insgesamt sehr faire prüfung, hab mich zwei, drei mal verhaspelt, schröder meinte aber dannach „sie wussten schon an einigen stellen genau genug, dass es auf jeden fall besser als 2.0 werden musste “