Differences

This shows you the differences between two versions of the page.

--- exam [2011/05/27 14:19] – [Core HOL] paddy
+++ exam [2011/08/02 15:29] (current) – [Core HOL] 188.107.127.174
@@ Line 7: / Line 7: @@
 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 =====
 :?: 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?
 ===== Core HOL =====
@@ Line 20: / Line 41: @@
 :?: 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 =====
 :?: 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.