FSI Informatik/pruefungen/hauptstudium/ls8/fm

Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Prüfungsprotokoll zu "Formale Methoden der Softwareentwicklung" (Übersicht)

Diese Seite ist nicht editierbar. Du kannst den Quelltext sehen, jedoch nicht verändern. Kontaktiere den Administrator, wenn du glaubst, dass hier ein Fehler vorliegt.

====== 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 ;-)"