Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Protokoll (Übersicht)

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.

Link zu der Vergleichsansicht

--- pruefungen:hauptstudium:ls8:semprog_ss13 [29.07.2013 12:34] – rootzlevel
+++ pruefungen:hauptstudium:ls8:semprog_ss13 [29.07.2013 13:05] (aktuell) – rootzlevel
@@ Zeile 1: / Zeile 1: @@
 ====== Protokoll ======
-  Prüfer: Daniel, Lutz. Fragen nur von Daniel
+Prüfer: Daniel, Lutz. Fragen nur von Daniel
@@ Zeile 10: / Zeile 10: @@
    - Nachfrage: Was ist mit:
-     <code>
+     H: 0 = 1
-     H: x = 1
      ----------------------
-     </code>
-   - Antwort: Geht net, nur mit inversion. contradiction will tatsächlich
+   - Antwort: Geht net, nur mit inversion. contradiction will tatsächlich False (oder (A ∧ ¬A))
-     False (oder (A ∧ ¬A))
 ===== Wie implementiert man conjunction =====
-   - Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen
+   - Antwort: Induktiver Datentyp mit einem Konstruktor, der zwei Prämissen nimmt.
-     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 =====
@@ Zeile 32: / Zeile 32: @@
      - Für expressions: Evaluieren auf das Gleiche
-     - Für statements: Genau dann wenn das Eine mit state x terminiert, tuts
+     - Für statements: Genau dann wenn das Eine mit state x terminiert, tuts das andere auch.
-       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 =====
@@ Zeile 41: / Zeile 46: @@
 ===== Beweisen sie ein Fakultätsprogramm in Hoare =====
-   Habe hingeschreben:
+   - Habe hingeschreben:
    #+BEGIN_EXAMPLE
@@ Zeile 50: / Zeile 55: @@
    end
    { x = n! }
-   #+END_EXAMPLE
-   Anwenden: Seq, Assign, Consequence, While
+   - Anwenden: Seq, Assign, Consequence, While
-   Nachdem ich mit consequence die invariante hatte, hat er abgebrochen.
+   - 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
+   - Programm auf einmal komplett evaluieren vs. ec terminiertinzelne Evaluationsschritte
 ===== Was ist zB ein Vorteil von Small-Step =====
-   Implementierung von Parallel-Imp
+   - Implementierung von Parallel-Imp