Simple gedanken experiments in leveraging applications of formal methods

Abstract

As experience in established engineering disciplines shows, the most (maybe only) effective way for leveraging formal methods (FM) into daily practice is by developing mathematical modeling abilities. Laying a solid theoretical basis early is best assisted by simple example problems with minimal technical content. It is shown how simplicity still allows covering all practical aspects of FM and even finding new insights because, as in basic science, simple problems lead to a variety of gedanken experiments. Of the wide realm of opportunities, three are illustrated: (a) microsemantics in algorithmic problem solving and reasoning about invariants, (b) experimenting with data abstractions to capture informal statements faithfully, (c) expressing puzzles involving procedures, possibly with nondeterminism and multiple loops, by simple mathematics. The proper rôle of software tools in leveraging FM is discussed alongside. © 2008 Springer-Verlag.