User Tools

Site Tools


exam

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
exam [2011/05/24 13:54]
131.246.84.190 [Core HOL]
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
 +  * 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 ===== ===== Core HOL =====
  
 :?: What's the most important thing that needs to be proven when defining types in a HOL theory $T = (\chi, \Sigma, A)$? :?: 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 \<Rightarrowbool$ has at least one element inside. Formally $T \vdash \exists x.\; S\; x$+  * 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? :?: Why is it important that the new types defined in HOL are non-empty?
Line 20: 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.
exam.1306238088.txt.gz · Last modified: 2011/05/24 13:54 by 131.246.84.190