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 ca...

• Type: Conference
• Year: 2006
• Where: FM
• Authors: Raymond T. Boute
• Keywords: FM 2006, Formal Calculation, Formal Methods, Informal Statements