This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
exam [2011/06/09 10:47] 91.45.33.35 |
exam [2011/08/02 15:29] (current) 188.107.127.174 [Core HOL] |
||
---|---|---|---|
Line 7: | Line 7: | ||
Please try to maintain categories of useful size, so each gets its own edit button. | 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! | ||
===== General ===== | ===== General ===== | ||
:?: Please give a short overview over the lecture. | :?: Please give a short overview over the lecture. | ||
* Intorduction: What is Verification and Specification? What is a Logic? --> Propositional logic | * 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? | :?: What is Verification? | ||
Line 16: | Line 25: | ||
:?: What is Specification? | :?: What is Specification? | ||
- | * defining all possible behaviours of the specified syetsm | + | * 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 is a Model? | ||
===== Core HOL ===== | ===== Core HOL ===== | ||
Line 27: | Line 41: | ||
:?: How are the elements //True// and //False// introduced in HOL? | :?: How are the elements //True// and //False// introduced in HOL? | ||
- | * Since there should always be an infinite set in **U** whose elements and power sets are also fully contained in **U**, there's a guarantee that there will be a set with two elements and that set is going to represent the values //True// and //False// ((Did I miss something?)) | + | * 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// ((Did I miss something?)) |
+ | |||
+ | :?: 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//? | ||
===== Calculi ===== | ===== Calculi ===== | ||
:?: Why do we need calculi. | :?: 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, ... | :?: 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. | :?: 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. |