(Bergen)

Algebraic specifications is a very useful technology for domain analysis and engineering, as well as being valuable for verification and validation of the resulting software. One problem with the traditional specification methods is their inability to deal flexibly with error situations, such as non-termination and exceptions.Guarded algebras allow the specification of algebras where the presence of errors, both recoverable (exceptions) and irrecoverable (partiality) can be handled smoothly, i.e., without cluttering the axioms.

This presentation will be in two parts. First we will give an intuition of the ideas involved, showing how we specify several algebras with quite involved errors. We also show how we independently may specify error handlers.

Then we use the concepts of institutions and generalised logics to show that guarded specifications are insensitive to whether the underlying models are total or partial, and that we hence may use the simpler total logics when reasoning about guarded specifications.

This work is done in cooperation with Eric Wagner.

Robert Recorde Room

Department of Computer Science