On choosing a good notation for a formal methods course: Making the concepts explicit

In a first undergraduate course in formal methods, it is important that the key concepts be made explicit to the students and that they be supported by the specification language. In this paper, we examine what those key concepts are and show how they are supported by the Spec specification language. We briefly describe a syntax- and type-checker we developed for this language and a new CLASS construct we added to Spec in order for it to better support OO concepts. Finally, through a short example, we also illustrate what we consider to be some of the weaknesses of two common specification languages, VDM and Z.

Pour obtenir la version postscript

Cliquez ici pour obtenir la version postscript.