User Tools
official:goals
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
official:goals [2011/07/18 11:40] paddy [Sheet 8] |
official:goals [2012/07/06 18:08] (current) paddy |
||
|---|---|---|---|
| Line 12: | Line 12: | ||
| * Make first steps with the tool/editor Isabelle/HOL/Emacs. | * Make first steps with the tool/editor Isabelle/HOL/Emacs. | ||
| + | ===== Sheet 2 ===== | ||
| + | |||
| + | ==== Exercise 1 ==== | ||
| - | ===== Sheet 2 ===== | + | * 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. | ||
| + | |||
| + | ==== Exercise 2 ==== | ||
| - | ==== Exercise 1 ==== | + | * 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 write basic Isabelle/HOL functions and recursive functions. | + | * First steps in finding missing lemmas from proofs which are not working yet. |
| - | * Get familiar with functional programs, so you can at least read more complex programs. | + | |
| - | + | ==== Exercise 3 ==== | |
| - | ==== Exercise 2 ==== | + | |
| - | + | ||
| - | * Be able to specify properties of functions in Isabelle/HOL. | + | |
| - | * Be able to prove many of these properties with a simple proof pattern. | + | |
| - | * First steps in finding missing lemmas from proofs which are not working yet. | + | |
| - | + | ||
| - | ==== 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 ===== | ===== Sheet 3 ===== | ||
| ==== Exercise 1 ==== | ==== Exercise 1 ==== | ||
| - | * Basic theory questions you should be able to answer. | + | * 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 ==== | ==== Exercise 2 ==== | ||
| * Get used to the idea of using existing types to define new ones. | * Get used to the idea of using existing types to define new ones. | ||
| - | * The actual definitions are very easy once you get the idea. | + | * Get used to the idea that sets and predicates are pretty much equivalent. |
| ==== Exercise 3 ==== | ==== Exercise 3 ==== | ||
| - | * Be able to define datatypes in Isabelle/HOL. | + | * More exercise in writing, understanding and modifying functional programs and datatypes. |
| - | * Be able to define primitive recursive functions on datatypes. | + | * Get familiar with proofs, proof commands and proof states in a very simple setting. |
| - | * Be able to specify properties on such functions. | + | * In general, understand how provers work and how one could implement one. |
| - | * 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 4 ==== | ||
| - | |||
| - | * More exercise in writing functional programs and using datatypes. | ||
| - | * Can be used to check the own skills in basic functional programming. | ||
| - | * Get familiar with proofs, proof commands and proof states in a very simple setting. | ||
| ===== Sheet 4 ===== | ===== Sheet 4 ===== | ||
| - | ==== Exercise 1 ==== | + | * 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. | ||
| - | * (a/b/c) Basic theory questions you should be able to answer. | + | ===== Sheet 5 ===== |
| - | * (d/e) More and more advanced questions where you can get more familiar with using Isabelle/HOL, proofs, finding and applying theorems, etc. | + | |
| - | ==== Exercise 2 ==== | + | |
| + | ==== Exercise 1 ==== | ||
| * Be able to apply methods to rules and do proofs. | * Be able to apply methods to rules and do proofs. | ||
| Line 71: | Line 69: | ||
| * Be able to do arbitrary proofs on propositional and predicate logic theorems. | * Be able to do arbitrary proofs on propositional and predicate logic theorems. | ||
| - | ===== Sheet 5 ===== | + | ==== Exercise 2 ==== |
| * Get familiar with designing and defining both syntax and semantics of languages. | * Get familiar with designing and defining both syntax and semantics of languages. | ||
| Line 78: | Line 76: | ||
| ===== Sheet 6 ===== | ===== Sheet 6 ===== | ||
| - | * Understand and proof properties on paper about lattices and fixpoints. | + | * First steps in finding needed theorems from the library, using the Find Theorems function. |
| - | * Be able to specify inductive sets both on paper and in Isabelle/HOL. | + | * First steps in using different induction schemes. |
| - | * Be able to do simple proofs on elements of inductive sets in Isabelle/HOL. | + | |
| - | * First steps in finding needed theorems from the library, using the //Find Theorems// function. | + | |
| * First case study about specifying models, properties and proving their consistency. | * First case study about specifying models, properties and proving their consistency. | ||
| Line 90: | Line 86: | ||
| * Be able to specify properties for such models. | * Be able to specify properties for such models. | ||
| * Be able to prove those properties with regard to the 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 ===== | ===== Sheet 8 ===== | ||
| Line 105: | Line 104: | ||
| * Be able to prove properties about language semantics. | * Be able to prove properties about language semantics. | ||
| * Be able to do induction over inductive sets / predicates. | * 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.1310982056.txt.gz · Last modified: 2011/07/18 11:40 by paddy
Page Tools
