Understanding and exploring formal specifications

Formal methods is seen as a means of applying scientific knowledge to software construction, thereby legitimating the use of mathematics within software engineering. However, the software engineering community faces numerous challenges before an effective transfer of this formal methods technology can take place because of the level of skill, expertise and effort required in their application. It is argued that at present the use of formal notations for system specification is a mature technology offering the greatest leverage. The relative benefits of a declarative approach with a getting it right the first time maxim versus an imperative approach coupled with an exploratory trial and error flavour are explored. Detailed characteristics of a teaching and learning environment developed to support the latter approach are provided. Its varied uses in the context of teaching and learning within undergraduate and postgraduate courses in software engineering are discussed. Exemplars from these uses show how users of the environment explore formal specifications to improve their understanding of specification and thereby illustrate the effectiveness of the environment. Implications of our approach on technology transfer and training are briefly explored.