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 [2012/05/10 09:50] paddy [Exercise 3] |
official:goals [2012/07/06 18:08] (current) paddy |
||
|---|---|---|---|
| Line 29: | Line 29: | ||
| * 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. | + | * 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. | ||
| + | |||
| + | ===== 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.1336636242.txt.gz · Last modified: 2012/05/10 09:50 by paddy
Page Tools
