Lecture
Section outline
-
- Introduction (4 on 1).
- Abstract Datatypes (4 on 1).
- CafeOBJ (4 on 1).
- Logic (4 on 1).
- Specifications: Formal and Informal - A Case Study (restricted)
- Loose Specifications (4 on 1).
- Model-based Specifications in Larch/C++ (4 on 1).
- Proof of Correctness of Data Representations (restricted).
- An Overview of Larch/C++: Behavioral Specifications for C++ Modules (original site).
- Formal Specification as a Design Tool (restricted)
- Term Algebras (4 on 1).
- Initial Specifications (4 on 1).
- Executing Specifications (4 on 1).
- Specifying in the Large (4 on 1).
- Case Study - A Multiple Window Environment (restricted)
- A Case Study - A Lexical Analyzer (restricted)
- A Gentle Introduction to CASL (original site).
Password is handed out in class.Literature
Jacques Loeckx, Hans-Dieter Ehrich, Markus Wolf: Specification of Abstract Datatypes, John Wiley & Teubner, Chichester, 1996. Amazon.at Page.Donald Sannella, Andrzej Tarlecki: Foundations of Algebraic Specification and Formal Software Development, Springer, Berlin, 2012. Amazon.at Page.