The idea of this page is to collect questions which might be asked in the exams. Whenever you review the slides or work on exercises, just put anything here which might be asked.

I guess it will be most easy for the moderating group to put questions about the topic they present here, too.

Please try to maintain categories of useful size, so each gets its own edit button.

If there are any answers on this page, they are given by students; Feel free to discuss the answers and/or add additional ones!

Please give a short overview over the lecture.

• Intorduction: What is Verification and Specification? What is a Logic? –> Propositional logic
• Functional programming and specification (ML & Isabelle/HOL)
• HOL: language and semantic aspects (e.g. types, terms, theory, cons. ext., …)
• Proofs in HOL
• Specific things in HOL: sets, functions, relations, and fixpoints
• Verifying functions
• Inductively defined sets
• Specifiaction of PL semantics (operational-, denotational- & axiomatical semantics)
• –> programm verification and programm logic (Hoare Logic)

What is Verification?

• argument for building the system right (NOT building the right system –> validation)

What is Specification?

• defining all possible behaviours of the specified system

What is the difference between model- and property-oriented specifications?

• Model-oriented is based on well-defined mathematical objects like sets and functions, which are used to construct a representation of the system state, as well as the operations on these states. Thus, such specifications reason about a transition system.
• Property-oriented is purely declarative. It uses some logic language to express the properties of the functions in the system.

What is a Model?

What's the most important thing that needs to be proven when defining types in a HOL theory $T = (\chi, \Sigma, A)$?

• Proof that the newly introduced term $S$ of type $r \Rightarrow bool$ has at least one element inside. Formally $T \vdash \exists x.\; S\; x$

Why is it important that the new types defined in HOL are non-empty?

• (see FAQ for hints)

How are the elements True and False introduced in HOL?

• Since there should always be a distinguished infinite set in U whose elements and subsets are also fully contained in U, there's a guarantee that there will be a set with two elements (say the subset {0,1} of the infinite set) and that one is going to be mapped further on to the values True and False ¹⁾

Why must all functions be total in Isabelle/HOL?

How does the automatic proof of termination work for definition, primrec, and fun?

What is the general procedure for proving termination manually in function?

Why do we need calculi.

• Basically, calculi are the tools we use to derive (and prove) theorems. Given a set of valid formulas and a sound calculus, new valid formulas (tautologies) can be derived. As far as I know, the semantic notion of “validity” corresponds to “provability” in the calculus, since it does not consider any notion of “truth”.

Please explain the following properties: Soundness (Correctness), Completeness, …

• A deductive system is sound if all provable formulas are valid. It is complete if all valid formulas are provable.
• Validity is a semantic property ($A \models B$), while provability a syntactic one ($A \vdash B$). So, in other words we have:
  • Soundness: $A \vdash B \longrightarrow A \models B$
  • Completeness: $A \models B \longrightarrow A \vdash B$

What are the advantages/disadvantages of the Hilbert calculus compared to the Gentzen calculus.

How can we prove formulas without a calculus?

• Calculi are based purely on syntax. We can always rely on semantic proofs, e.g. truth table or tableaux methods.