Teaching formal methods lite via testing

A new style of formal methods course is described, based on a pragmatic app roach that emphasizes testing. The course introduces students to formal spe cification using Z, and shows how formal specification and testing can bene fit each other, in both the validation and verification phases. It uses a t ools-based approach, with practical work that reinforces formal specificati on techniques as well as traditional software engineering skills, such as u nit and system testing, inspection and defensive programming with assertion s. The two main results are to identify several practical uses of formal sp ecifications that are not widely practised or taught, and to demonstrate th at teaching them results in a more interesting and relevant formal methods course. Copyright (C) 2001 John Wiley & Sons, Ltd.