This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
official:goals [2012/05/10 09:49] paddy |
official:goals [2012/07/06 18:05] paddy |
||
---|---|---|---|
Line 28: | Line 28: | ||
* 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 ===== | ||
Line 71: | Line 73: | ||
* Get familiar with designing and defining both syntax and semantics of languages. | * 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. | * 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. | ||