Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Protokoll (Übersicht)
Dies ist eine alte Version des Dokuments!
* Protokoll
Prüfer: Daniel, Lutz. Fragen nur von Daniel
Was macht contradiction - Antwort: Solved das Goal, wenn False im Kontext - Nachfrage: Was ist mit: H: x = 1 ———————- - Antwort: Geht net, nur mit inversion. contradiction will tatsächlich False (oder (A ∧ ¬A)) Wie implementiert man conjunction
- Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen
nimmt.
- Frage: Wie prooft man es?
- Antwort: split oder apply vom Konstructor
Wie haben wir Program-Equivalence definiert - Antwort: - Für expressions: Evaluieren auf das Gleiche - Für statements: Genau dann wenn das Eine mit state x terminiert, tuts das andere auch. Schreibe die Hoare-Kalkül-Regeln hin
- Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon
Beweisen sie ein Fakultätsprogramm in Hoare Habe hingeschreben: #+BEGIN_EXAMPLE { y = n } X := 1; while (y > 0) then x := y * x; y := y - 1 end { x = n! } #+END_EXAMPLE Anwenden: Seq, Assign, Consequence, While Nachdem ich mit consequence die invariante hatte, hat er abgebrochen. Was ist Big-Step vs Small-Step
- Programm auf einmal komplett evaluieren vs. einzelne Evaluationsschritte
** Was ist zB ein Vorteil von Small-Step
Implementierung von Parallel-Imp