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

no way to compare when less than two revisions

Unterschiede

Hier werden die Unterschiede zwischen zwei Versionen der Seite angezeigt.


—pruefungen:hauptstudium:ls8:semprog_ss13_b [29.07.2013 13:42] (aktuell) – angelegt dario
Zeile 1: Zeile 1:
 +=====Protokoll SemProg 29.7.2013=====
  
 +Prüfer: Daniel Gorín, Lutz Schröder
 +
 +====Fragen====
 +
 +==Was macht »omega«?===
 +
 +  löst pressburger-arithmetik
 +
 +
 +==Wie ist in coq der existenzquantor definiert?==
 +
 +antwort wäre gewesen:
 +  Inductive ex (X:Type) (P : X->Prop) : Prop :=
 +    ex_intro : forall (witness:X), P witness -> ex X P.
 +
 +hab mich bissi vertan, und
 +  Inductive ex {X : Type} (x : X) ...
 +
 +angefangen, so dass wir einen kleinen ausflug nach "welchen typ hat der ausdruck »X > 5«? (nat -> Prop) gemacht haben.
 +
 +==Was ist denn die »functional extensionality«?==
 +
 +Axiom, das sagt, dass wenn forall x. f x = g x, dann ist f = g. ist in coq so nicht beweisbar, weil nur dinge für die man einen beweis konstruieren kann beweisbar sind.
 +
 +
 +==Wir ham da mal so n programm, was sagst du so dazu==
 +
 +  Axiom funny: exists (X Y : Type) (x : X) (f g : X -> Y), f x = g x -> f = g.
 +
 +also functional extensionality, nur mit existenz- statt allquantor.
 +
 +==Was sind denn diese hoare-tripel?==
 +
 +tripel aus vorbedingung, codestück und nachbedingung. wenns gültig ist, dann sagts, dass falls vorbedingung gilt, und codestück terminiert, dannach nachbedingung gilt.
 +
 +==schreib doch mal eine der hoare-regeln hin==
 +
 +  (hoare_asgn) ---------------------------
 +                {{[X/s]P}} X := s {{P}}
 +
 +==wenn man jetzt eine hoare-regel für eine for-schleife wie in C-ähnlichen sprachen haben wollen würde..==
 +
 +for-schleife allgemein
 +  FOR (C1; guard; C2) { C3 }
 +
 +hoare-tripel
 +  {{P'}}C1{{P}}     {{P}} WHILE guard DO C3; C2 END {{P ∧ ¬guard}}
 +  ----------------------------------------------------------------
 +    {{P'}} FOR (C1; guard; C2) { C3 } {{P ∧ ¬guard}}
 +
 +
 +===Ergebnis===
 +damit war die zeit auch schon rum, leider (auch etwas zu daniels überraschung), und die ganzen coolen dinge, wie typ-foo (progress, typerhaltung) und lambda-zeugs kamen garned dran :-/
 +
 +zusammen mit meinem übungsabgabenergebnis von umgerechnet 2.4 wars am ende ne 2.0