User Tools

Site Tools


official:goals

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
official:goals [2012/06/13 10:23]
paddy
official:goals [2012/07/06 18:08] (current)
paddy
Line 89: Line 89:
   * Understand and proof properties on paper about lattices and fixpoints.   * Understand and proof properties on paper about lattices and fixpoints.
   * Be able to specify inductive sets on paper and understand their semantics.   * 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.1339575813.txt.gz ยท Last modified: 2012/06/13 10:23 by paddy