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

Nächste Überarbeitung		Vorherige Überarbeitung
pruefungen:hauptstudium:ls8:semprog_ss13 [29.07.2013 12:13] – angelegt rootzlevelpruefungen:hauptstudium:ls8:semprog_ss13 [29.07.2013 13:05] (aktuell) – rootzlevel
Zeile 1: Zeile 1:
-* Protokoll+====== Protokoll ======
  
-  Prüfer: Daniel, Lutz. Fragen nur von Daniel+Prüfer: Daniel, Lutz. Fragen nur von Daniel
  
-** Was macht contradiction+ 
 +===== Was macht contradiction =====
  
    - Antwort: Solved das Goal, wenn False im Kontext    - Antwort: Solved das Goal, wenn False im Kontext
Zeile 9: Zeile 10:
    - Nachfrage: Was ist mit:    - Nachfrage: Was ist mit:
            
-     H: x = 1+     H: 0 = 1
      ----------------------      ----------------------
  
-   - 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+===== 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?    - Frage: Wie prooft man es?
Zeile 24: Zeile 23:
    - Antwort: split oder apply vom Konstructor    - Antwort: split oder apply vom Konstructor
  
-** Wie haben wir Program-Equivalence definiert+===== Was ist functional extensionality ==== 
 + 
 +   - forall x, f x = g x -> f = g 
 + 
 +===== Wie haben wir Program-Equivalence definiert =====
  
    - Antwort:    - Antwort:
            
      - Für expressions: Evaluieren auf das Gleiche      - 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+===== Schreibe die Hoare-Kalkül-Regeln hin =====
  
    - Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon    - Hab skip, seq, if und while hingeschreiben, dann hat er gesagt, es passt schon
  
-** Beweisen sie ein Fakultätsprogramm in Hoare+===== Beweisen sie ein Fakultätsprogramm in Hoare =====
  
-   Habe hingeschreben:+   - Habe hingeschreben:
  
    #+BEGIN_EXAMPLE    #+BEGIN_EXAMPLE
Zeile 47: Zeile 55:
    end    end
    { x = n! }    { 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+===== 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+===== Was ist zB ein Vorteil von Small-Step =====
  
-   Implementierung von Parallel-Imp+   - Implementierung von Parallel-Imp