Lecture

The lecture will be based on a not yet published manuscript "Thinking Programs" that covers in Chapter 6 the topic of "Abstract Data Types"; in the course we will walk through parts of this chapter.

• Chapter 6: Abstract Datatypes (teaser excerpt only)
  
• Thinking Programs (draft manuscript, password will be handed out in class)
  

Variously we will also use slides and other material from previous instances of this course (not aligned with above chapter):

• 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).

Restricted Area (password handed out in class)

Literature