Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » FMSoft WS14/15 (Übersicht)
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?