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/24 11:36] paddy |
official:goals [2012/07/06 18:08] (current) paddy |
||
|---|---|---|---|
| Line 77: | Line 77: | ||
| * First steps in finding needed theorems from the library, using the Find Theorems function. | * 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. | * 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.1337852168.txt.gz ยท Last modified: 2012/05/24 11:36 by paddy
Page Tools
