User Tools

Site Tools


official:goals

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
official:goals [2012/04/25 11:19]
paddy [Exercise 1]
official:goals [2012/07/06 18:08] (current)
paddy
Line 15: Line 15:
        
 ==== Exercise 1 ====    ==== Exercise 1 ====   
-  ​ + 
- * Be able to write basic Isabelle/​HOL functions and recursive functions. ​   +  * Be able to write basic Isabelle/​HOL functions and recursive functions. ​   
- * Get familiar with functional programs, so you can at least read more complex programs. ​  +  * Get familiar with functional programs, so you can at least //read// more complex programs. ​  
        
 ==== Exercise 2 ====    ==== Exercise 2 ====   
-   +
   * Be able to specify properties of functions in Isabelle/​HOL.  ​   * Be able to specify properties of functions in Isabelle/​HOL.  ​
   * Be able to prove many of these properties with a simple proof pattern. ​     * Be able to prove many of these properties with a simple proof pattern. ​  
Line 26: Line 26:
        
 ==== Exercise 3 ====    ==== Exercise 3 ====   
-   +
   * More advanced example. ​     * More advanced example. ​  
-  * Be able to define the algorithm and specify its correctness. ​  ​ +  * Be able to define the algorithm and specify its correctness. 
-   ​+  * Doing the proof at this point can be challenging. 
 +    * It highly depends on your definitions and your knowledge of the proof system. 
 +    * You should be able to do it at the end of the semester the latest. 
 +===== Sheet 3 ===== 
 + 
 +==== Exercise 1 ==== 
 + 
 +  * Be able to define datatypes in Isabelle/​HOL. 
 +  * Be able to define primitive recursive functions on datatypes. 
 +  * Be able to specify properties on such functions. 
 +  * Be able to prove many of these properties with a simple proof pattern. 
 +  * Next steps in finding missing lemmas from proofs which are not working yet. 
 + 
 +==== Exercise 2 ==== 
 + 
 +  * Get used to the idea of using existing types to define new ones. 
 +  * Get used to the idea that sets and predicates are pretty much equivalent. 
 + 
 +==== Exercise 3 ==== 
 + 
 +  * More exercise in writing, understanding and modifying functional programs and datatypes. 
 +  * Get familiar with proofs, proof commands and proof states in a very simple setting. 
 +  * In general, understand how provers work and how one could implement one. 
 + 
 + 
 +===== Sheet 4 ===== 
 + 
 +  * Basic theory questions you should be able to answer about the HOL core, universes, models, conservative extensions, etc. 
 +  * Exercise 2 (d/e) More and more advanced questions where you can get more familiar with using Isabelle/​HOL,​ proofs, finding and applying theorems, etc. 
 + 
 +===== Sheet 5 ===== 
 + 
 + 
 +==== Exercise 1 ==== 
 + 
 +  * Be able to apply methods to rules and do proofs. 
 +  * Get to know the different methods. 
 +  * Get to know more and more rules. 
 +  * Be able to do arbitrary proofs on propositional and predicate logic theorems. 
 + 
 +==== Exercise 2 ==== 
 + 
 +  * Get familiar with designing and defining both syntax and semantics of languages. 
 +  * First steps towards formulating and proving properties relating models, in this case two language semantics and a compiler. 
 + 
 +===== Sheet 6 ===== 
 + 
 +  * First steps in finding needed theorems from the library, using the Find Theorems function. 
 +  * First steps in using different induction schemes. 
 +  * First case study about specifying models, properties and proving their consistency. 
 + 
 +===== Sheet 7 ===== 
 + 
 +  * Two more complex case studies for specifying models, properties and proving their consistency. 
 +  * Be able to define advanced models. 
 +  * Be able to specify properties for such models. 
 +  * Be able to prove those properties with regard to the models. 
 + 
 +  * Understand and proof properties on paper about lattices and fixpoints. 
 +  * Be able to specify inductive sets on paper and understand their semantics. 
 + 
 +===== Sheet 8 ===== 
 + 
 +  * Get familiar with LTL. 
 +  * Be able to specify properties about transition systems in LTL. 
 +  * Be able to do proofs of LTL properties, using the semantics. 
 +  * Get to know one possible definition of traces and transition systems and how to use it for proofs. 
 +  * First steps in defining a calculus for an embedded logic in Isabelle/​HOL and using the calculus to do proofs. 
 +  * Learn how the specification affects proofs and how changes in the specification can help the proofs. 
 + 
 +===== Sheet 9 ===== 
 + 
 +  * Understand the difference between different styles of semantics. 
 +  * Be able to prove properties about language semantics. 
 +  * Be able to do induction over inductive sets / predicates. 
 + 
 +===== Sheet 10 ===== 
 + 
 +  * Be able to do pen & paper proofs using the Hoare calculus. 
 +  * Be able to find simple loop invariants. 
 +  * Be able to translate proofs into the framework created in the lecture.
  
official/goals.1335345584.txt.gz · Last modified: 2012/04/25 11:19 by paddy