Protokoll

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

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))

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

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

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.

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

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

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.

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

1. Implementierung von Parallel-Imp