Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Protokoll (Übersicht)
Inhaltsverzeichnis
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: 0 = 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
Was ist functional extensionality
- forall x, f x = g x → f = g
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.
Was ist ein Hoare-Triple
- { P } c { Q }
- P, Q sind Assertions
- P gilt auf st, c / st || st', Q gilt für st'
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! }
- 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. ec terminiertinzelne Evaluationsschritte
Was ist zB ein Vorteil von Small-Step
- Implementierung von Parallel-Imp