Software specification in CASL

03-05-H-706.54
Category A
Prerequisites: content of 600.01, 600.02, 601.01, 601.02, 604.02
ECTS: 6
Monday 10:00 - 12:00 MZH 7210,
Tuesday 13:00 - 15:00 MZH 4194

Start: Tuesday, October 24th

CASL, the Common Algebraic Specification Language, is an expressive language for the specification of software systems and other formal entities.

The most fundamental assumption is that programs are modelled as algebraic structures that include a collection of sets of data values together with functions over those sets. This level of abstraction is commensurate with the view that the correctness of the input/output behaviour of a program takes precedence over all its other properties. Another common element is that specifications of programs consist mainly of logical axioms, describing the properties that the functions are required to satisfy---often just by their interrelationship.

CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications; the latter are used to prescribe the modular structure of implementations.

The course will give an introduction to CASL, discuss sample case studies and will also explain how to use analysis and verification tools (like the heterogeneous tool set and the automatic theorem prover SPASS) for CASL specifications. These can be used for finding errors (like inconsistencies) at an early phase, as well as for proving intended consequences of a specification. Finally, it is also possible to derive executable programs from (algorithmic) specifications.

Literature

• CASL user manual
• CASL reference manual
• Language, proof and logic, a gentle introduction to first-order logic, with training software

Software

• The heterogeneous tool set
  Local installation: /home/linux-bkb/bin/hets
• The automatic theorem prover SPASS
  Local installation: /home/linux-bkb/bin/SPASS

Slides

• 24. Oct 06
• 30. Oct 06  Logelei (hint: use nullary predicates = propositional letters)
• 31. Oct 06  Slides for CASL user manual
• Problem sheet 1
• 06.Nov 06
• Problem sheet 2
• Semantics of basic specifications
• Semantics of structured specifications
• Development graphs   test file for Hide-Theorem-Shift   test file for Theorem-Hide-Shift   sorting example
• Problem sheet 3  ordering example  invoice example