Title :
Use of a specification construction and animation tool to teach formal methods
Author :
Morrey, Ian ; Siddiqi, Jawed ; Buckberry, Graham ; Hibberd, Richard
Author_Institution :
Sheffield Hallam Univ., UK
Abstract :
ZAL (Z Animation in LISP) is a package which allows a Z specification to be incrementally designed and validated in an interactive environment built on Common LISP. A Z specification is transformed into an equivalent ZAL program which can be executed in order to demonstrate the functionality of the intended implementation. ZED is a full screen editor and syntax analyser for Z. Using these two tools as an integrated package encourages and facilitates an exploratory approach to formal specification which reflects the way in which many users of Z (particularly beginners) prefer to approach the specification task. The package has also been used to support the teaching of students following courses in discrete mathematics, formal specification and software development
Keywords :
computer animation; computer science education; courseware; formal specification; software tools; specification languages; Common LISP; Z Animation in LISP; Z specification; ZAL package; ZAL program; animation tool; beginners; courses; discrete mathematics; formal method teaching; formal specification; full screen editor; functionality; interactive environment; software development; specification construction; students; syntax analyser; teaching; tools; Animation; Education; Formal specifications; Mathematics; Packaging; Programming; Prototypes; Software packages; Specification languages; Vehicles;
Conference_Titel :
Computer Software and Applications Conference, 1993. COMPSAC 93. Proceedings., Seventeenth Annual International
Conference_Location :
Phoenix, AZ
Print_ISBN :
0-8186-4440-0
DOI :
10.1109/CMPSAC.1993.404236