Sie befinden sich hier: Termine » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Protokoll   (Übersicht)

Protokoll

Prüfer: Daniel, Lutz. Fragen nur von Daniel

Was macht contradiction

  1. Antwort: Solved das Goal, wenn False im Kontext
  1. Nachfrage: Was ist mit:

H: 0 = 1

  1. ———————
  1. Antwort: Geht net, nur mit inversion. contradiction will tatsächlich False (oder (A ∧ ¬A))

Wie implementiert man conjunction

  1. Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen nimmt.
  1. Frage: Wie prooft man es?
  1. Antwort: split oder apply vom Konstructor

Was ist functional extensionality

  1. forall x, f x = g x → f = g

Wie haben wir Program-Equivalence definiert

  1. Antwort:
  1. Für expressions: Evaluieren auf das Gleiche
  2. Für statements: Genau dann wenn das Eine mit state x terminiert, tuts das andere auch.

Was ist ein Hoare-Triple

  1. { P } c { Q }
  2. P, Q sind Assertions
  3. P gilt auf st, c / st || st', Q gilt für st'

Schreibe die Hoare-Kalkül-Regeln hin

  1. Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon

Beweisen sie ein Fakultätsprogramm in Hoare

  1. Habe hingeschreben:
 #+BEGIN_EXAMPLE
 { y = n }
 X := 1;
 while (y > 0) then
   x := y * x; y := y - 1
 end
 { x = n! }
  1. Anwenden: Seq, Assign, Consequence, While
  1. Nachdem ich mit consequence die invariante hatte, hat er abgebrochen.

Was ist Big-Step vs Small-Step

  1. Programm auf einmal komplett evaluieren vs. ec terminiertinzelne Evaluationsschritte

Was ist zB ein Vorteil von Small-Step

  1. Implementierung von Parallel-Imp