Using domain-independent problems for introducing formal methods

Abstract

The key to the integration of formal methods into engineering practice is education. In teaching, domain-independent problems i.e., not requiring prior engineering background-offer many advantages. Such problems are widely available, but this paper adds two dimensions that are lacking in typical solutions yet are crucial to formal methods: (i) the translation of informal statements into formal expressions; (ii) the role of formal calculation (including proofs) in exposing risks or misunderstandings and in discovering pathways to solutions. A few example problems illustrate this: (a) a small logical one showing the importance of fully capturing informal statements; (b) a combinatorial one showing how, in going from "real-world" formulations to mathematical ones, formal methods can cover more aspects than classical mathematics, and a half-page formal program semantics suitable for beginners is presented as a support; (c) a larger one showing how a single problem can contain enough elements to serve as a Leitmotiv for all notational and reasoning issues in a complete introductory course. An important final observation is that, in teaching formal methods, no approach can be a substitute for an open mind, as extreme mathphobia appears resistant to any motivation. © Springer-Varlag Berlin Heidelberg 2006.