Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » FMSoft WS14/15   (Übersicht)

no way to compare when less than two revisions

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.


pruefungen:hauptstudium:ls8:fmsoft_ws14 [14.04.2015 09:24] (aktuell) – angelegt ouler
Zeile 1: Zeile 1:
 +==== FMSoft WS14/15 ====
  
 +  * Was ist ein Hoare-Triple und wofuer ist es gut?
 +  * Welche Sprache haben wir in der Vorlesung betrachtet?
 +      * Wie ist die Syntax und Semantik davon?
 +      * Welche Probleme gab es bei der Definition der Semantik und wie haben wir sie geloest? (Fixpunktsatz von Kleene)
 +  * Wie sind die Beweisregeln fuer das Hoare-Kalkuel?
 +  * Was ist Korrektheit und was ist Vollstaendigkeit?
 +  * Und dann haben wir also Korrektheit und Vollstaendigkeit von dem Beweiskalkuel gezeigt, oder? (Antwort: Nein! Nur relative Vollstaendigkeit)
 +  * Warum nur relative Vollstaendigkeit und was war das wichtige Werkzeug dabei?
 +  * Wofuer braucht man Boogie? Wie uebersetzt man IMP zu Boogie? 
 +  * Was ist das Frameproblem und wie loest man es?
 +
 +
 +  * Wie ist die Syntax und die Semantik von LTL?
 +  * Erklaeren Sie grob das Model-Checking fuer LTL?
 +  * Was ist ein NBA? Was ist der Unterschied zum GNBA?
 +  * Wie uebersetzt man einen GNBA in einen NBA? 
 +  * Wie uebersetzt man eine Formel in einen GNBA?
 +  * Wie konstruiert man den Automaten fuer M x A_{\neg \phi}?
 +  * Wie prueft man jetzt, ob die Formel im Modell erfuellt ist?
 +
 +