Du befindest dich hier: FSI Informatik » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » Protokoll SemProg 29.7.2013 (Übersicht)
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