Sie befinden sich hier: Termine » 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