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 12:00 - 14:00 MZH 4194,
Tuesday 12:00 - 14:00 MZH 1450

Start: Monday, April 12th

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