An undergraduate course in formal methods

摘要

We present a new undergraduate course in formal methods which emphasizes software specification and description instead of formal program correctness or program derivation.This course is motivated by the idea that specifications play a key role in the software development process and that precise and clear descriptions of software systems and artifacts are important. It wants to show students that some simple notions from logic and mathematics (predicates and quantifiers, set theory, maps), together with appropriate constructs for defining software components and systems, can be useful for this purpose.The course is taught using the Spec notation [1] and we first discuss why we did not choose the ubiquitous Z notation. The content of the course is then presented, followed with a brief description of an on-line WWW system that was developed to help the students do the exercices presented in the course notes.