Du befindest dich hier: FSI Informatik » 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).