Sie befinden sich hier: Termine » Prüfungsfragen und Altklausuren » Hauptstudiumsprüfungen » Lehrstuhl 8 » semprog_ss16 (Übersicht)

Examiners: Tadeusz Litak, Christoph Rauch

The atmosphere was super relaxed and friendly, all of us had a few laughs. Several minor hickups and uncertainty of some details didn't matter at all.

Q: Does `contradiction` solve the following goal?

Theorem x : true = false -> False. Proof. intros.

Q: Which tactic does solve it?

Q: Another one?

Q: What is the difference between `induction` and `inversion`?

Q: What does `induction` do that `inversion` doesn't?

Q: Is the following code correct?

Inductive no_repeats : (l : list) -> Prop := | nor_once : forall x l, appears_not_in x l -> no_repeats l -> no_repeats (x::l) | nor_forgot : forall x l, no_repeats l -> no_repeats (x::l)

[The second constructor might have been different, I can't remember the details]

`appears_not_in` was also defined and did what it sounds like.

Q: What is a hoare triple, what does it assert?

Q: Write down some hoare rules.

Q: [after writing down the sequence rule] Something more interesting?

Q: [after writing down the assignment rule] How about the rule for `while`?

Q: We talked about the simply-typed lambda calculus. What is the difference between our notions of terms in normal form and values?

Q: Which theorem connects types, normal forms and stuckness?

Q: [after stating a form of the progress theorem] We had another theorem involving types and reduction.

Q: Alright, that's the preservation theorem. Next, I have some new reduction/typing rules, choose one and state if determinism, preservation and progress are preserved.

1.

---------------- (ST_Foo1) ------------- (ST_Foo2) (\x. x) => foo foo => true

2.

--------------------------------- (ST_IfTrue') if true then t0 else t1 => true

3. can't recall, something involving a typing rule

Q: [after elaborating on the first ruleset] Choose one more.

Q: Oh, I asked you about these additional rules, but I didn't even ask you about the basic ones. Show me the rules for abstraction and application.

Q: I'm not sure what more to ask you. Can you write down an annotated version of the swap program using only two variables?

We stopped after I backwards-reasoned one instance of the assignment rule (which took several attempts).

The text below has been written by a student from the future different from the author of the exam protocol above!

Here is some working Coq code for the no_repeats inductive question:

Fixpoint appears_not_in {X: Type} (x: X) (l: list X): Prop := match l with | nil => True | cons y ys => (x <> y) /\ (appears_not_in x ys) end. Inductive no_repeats {X: Type} : list X -> Prop := | nor_empty: no_repeats nil | nor_cons: forall x l, appears_not_in x l -> no_repeats l -> no_repeats (x::l).