Using Domain-Independent Problems for Introducing Formal Methods Export

@inbook{Boute06:domain-indep-probs, 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. Index Terms: Domain-independent problems, Formal methods, Functional Predicate Calculus, Funmath, Generic functionals, Teaching, Specification, Word problems.}, address = {Berlin/Heidelberg}, author = {Boute, Raymond}, booktitle = {Lecture Notes in Computer Science}, chapter = {Chapter 22}, citeulike-article-id = {5321724}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11813040_22}, citeulike-linkout-1 = {http://www.springerlink.com/content/884587x16247342w}, doi = {10.1007/11813040_22}, editor = {Misra, Jayadev and Nipkow, Tobias and Sekerinski, Emil}, isbn = {3-540-37215-6}, journal = {FM 2006: Formal Methods}, keywords = {boute, fm, formal, general-bib, mathematical-methodology, mathis}, pages = {316--331}, posted-at = {2009-08-01 16:43:54}, priority = {2}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Using Domain-Independent Problems for Introducing Formal Methods}, url = {http://dx.doi.org/10.1007/11813040_22}, volume = {4085}, year = {2006} }

TY - CHAP ID - Boute06:domain-indep-probs L3 - citeulike-article-id:5321724 N2 - 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. Index Terms: Domain-independent problems, Formal methods, Functional Predicate Calculus, Funmath, Generic functionals, Teaching, Specification, Word problems. JF - FM 2006: Formal Methods SE - LNCS SN - 3-540-37215-6 AD - Berlin/Heidelberg EP - 331 TI - Using Domain-Independent Problems for Introducing Formal Methods PB - Springer-Verlag VL - 4085 T2 - Lecture Notes in Computer Science SP - 316 KW - boute KW - fm KW - formal KW - general-bib KW - mathematical-methodology KW - mathis AU - Boute, Raymond A2 - Misra, Jayadev A2 - Nipkow, Tobias A2 - Sekerinski, Emil PY - 2006/// UR - http://dx.doi.org/10.1007/11813040_22 ER -