This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
official:goals [2012/06/20 10:54] paddy |
official:goals [2012/07/06 18:08] (current) paddy |
||
---|---|---|---|
Line 92: | Line 92: | ||
===== Sheet 8 ===== | ===== Sheet 8 ===== | ||
- | * Get familiar with LTL. | + | * Get familiar with LTL. |
- | * Be able to specify properties about transition systems in LTL. | + | * Be able to specify properties about transition systems in LTL. |
- | * Be able to do proofs of LTL properties, using the semantics. | + | * 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. | + | * 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. | + | * 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. | + | * 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. | ||