Formal Specification of Abstract Datatypes (SS 2008)

Section outline

• Select section General

  General

  Collapse all Expand all

  Formal Specification of Abstract Datatypes (326.063, SS 2008)
  Time: Friday, 8:30-10:00.
  Room: T 911
  Start: March 7, 2008.
  
  The goal of this course is to teach students of computer science and mathematics methods for the formal specification of abstract data types and their application in practical software engineering examples. No prerequisites apart from basic set theory and logic are required.

  We concentrate on the approach of algebraic/axiomatic program specification where concepts from universal algebra are used to formalize the semantics of specifications. For rapid prototyping, we use the software system CafeOBJ in which specifications can be directly executed. We also sketch the object-oriented specification languages Larch/C++ and JML which are based on similar principles and finally introduce the Common Algebraic Specification Language CASL.
  

  Presentations of various case studies are interspersed. Course grades will be based on exercises which are both theoretical (paper and pencil) and practical (CafeOBJ).

  ---

  To take part in the course, you have to enrol in the KUSSS system. Since the exercises will be submitted via Moodle, you also have to login in Moodle and register as a course participant. You will then also receive per email all messages posted in the News forum.
  

  • Select activity News forum

    

    News forum
• Select section Topic 1

  Topic 1

  Presentations
  

  • 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 (local PDF copy).
  • 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 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.
  

  
  
• Select section Topic 2

  Topic 2

  CafeOBJ
  
  The CafeOBJ system is freely available for Linux and Windows from the CafeOBJ home page.
  
  Local copies:
  

  • CafeOBJ 1.4.7 (Linux executable)
  • CafeOBJ manual Ver.1.4 (PDF)

  If necessary, you may also use the CafeOBJ installation in the RISC environment (see the Formal Methods Course Software at RISC).
  
• Select section Topic 3

  Topic 3

  Exercises
  
  Five exercises are handed out of which at least four have to be positively elaborated; the best four exercises are used for grading.
  
  

  • Select activity Exercise 1 (April 21)

    

    Exercise 1 (April 21) Assignment
  • Select activity Exercise 2 (May 12)

    

    Exercise 2 (May 12) Assignment
  • Select activity Exercise 3 (May 26)

    

    Exercise 3 (May 26) Assignment
  • Select activity Exercise 4 (June 16)

    

    Exercise 4 (June 16) Assignment
  • Select activity Exercise 5 (July 7)

    

    Exercise 5 (July 7) Assignment