Tom Naughton, Computer Science, NUIM.

Course Outline

• Creating abstract (implementation-independent) solutions which can be proved free of ambiguity and contradition.

• Validation: is the resulting specification what the customer wanted?

• Transformation of the specification into a program.

• By understanding the semantics of our programming language, verify that the program indeed implements the specification.

Detailed Outline

Section 0 Introduction

Section 1 Formal specification

Model-based, process-based, and axiomatic specification styles; VDM, B, LOTOS

Section 2 Concurrency and real-time computing

Semiformal modelling methods; Timed automaton model

Section 3 Formal semantics

Operational, denotational, translational and axiomatic semantics; The Dijkstra-Gries guarded command language

URL: http://www.cs.may.ie/~tnaughton
Revised: July 1998
Contact: webmaster@cs.may.ie