Proofs & Programs 1995
LEGO-Summerschool in Hetzelsdorf
Exercises and Solutions
The Exercises covered the following topics:
- Basic proofs in Lego (Thomas Schreiber)
- Data refinement (Zhaohui Luo)
- Concurrency (Zhaohui Luo)
- Imperative Programs (Thomas Schreiber)
- Exercises on inductive relations (Randy Pollack)
- Object-oriented proving (Wolfgang Naraschewski)
- Bonus exercise: type of "printf" in LEGO (Eike Ritter and Thomas Schreiber)
The
exercises and solutions
can be accessed via ftp together with documentation as tar-files.
steffen@informatik.uni-erlangen.de
Mon Aug 21 11:35:08 MET DST 1995