Teaching formal methods is notoriously difficult and is linked to motivation problems among the students; we think that formal methods need to be supported by adequate tools to get better acceptance from the students. One of the goals of the thesis is to build a practical tool to help students to deeply understand the classical programming methodology based on specifications, loop invariants, and decomposition into subproblems advocated by Dijkstra, Gries, and Hoare to name only a few famous computer scientists. Our motivation to build this tool is twofold. On the one hand, we demonstrate that existing verification tools (e.g., ESC/Java, Spark, SMV) are too complex to be used in a pedagogical context; moreover they often lack completeness, (and sometimes, even soundness). On the other hand teaching formal (i.e., rigorous) program construction with pen and paper does not motivate students at all. Thus, since students love to use tools, providing them with a tool that checks not only their programs but also their specifications and the structure of their reasoning seemed appealing to us.
Obviously, building such a system is far from an easy task. It may even be thought completely unfeasible to experts in the field. Our approach is to restrict our ambition to a very simple programming language with simple types (limited to finite domains) and arrays. In this context, it is possible to specify problems and subproblems, both clearly and formally, using a specific assertion language based on mathematical logic. It appears that constraint programming over finite domains is especially convenient to check the kind of verification conditions that are needed to express the correctness of imperative programs. However, to conveniently generate the constraint problems equivalent to a given verification condition, we wish to have at hand a powerful language that allows us to interleave constraints generation, constraints solving, and to specify a distribution strategy to overcome the incompleteness of the usual consistency techniques used by finite domain
constraint programming. We show in this thesis that the Oz language includes all programming mechanisms needed to reach our goals.
Such a tool has been fully implemented and is intended to provide interesting feedback to students learning the programming method: it detects programming and/or reasoning errors and it provides typical counter-examples. We argue that our system is adapted to our pedagogical context and we report on experiments of using the tool with students in a third year programming course.
| Identifer | oai:union.ndltd.org:BICfB/oai:ucl.ac.be:ETDUCL:BelnUcetd-09262007-143230 |
| Date | 14 September 2007 |
| Creators | Dony, Isabelle |
| Publisher | Universite catholique de Louvain |
| Source Sets | Bibliothèque interuniversitaire de la Communauté française de Belgique |
| Language | English |
| Detected Language | English |
| Type | text |
| Format | application/pdf |
| Source | http://edoc.bib.ucl.ac.be:81/ETD-db/collection/available/BelnUcetd-09262007-143230/ |
| Rights | unrestricted, J'accepte que le texte de la thèse (ci-après l'oeuvre), sous réserve des parties couvertes par la confidentialité, soit publié dans le recueil électronique des thèses UCL. A cette fin, je donne licence à l'UCL : - le droit de fixer et de reproduire l'oeuvre sur support électronique : logiciel ETD/db - le droit de communiquer l'oeuvre au public Cette licence, gratuite et non exclusive, est valable pour toute la durée de la propriété littéraire et artistique, y compris ses éventuelles prolongations, et pour le monde entier. Je conserve tous les autres droits pour la reproduction et la communication de la thèse, ainsi que le droit de l'utiliser dans de futurs travaux. Je certifie avoir obtenu, conformément à la législation sur le droit d'auteur et aux exigences du droit à l'image, toutes les autorisations nécessaires à la reproduction dans ma thèse d'images, de textes, et/ou de toute oeuvre protégés par le droit d'auteur, et avoir obtenu les autorisations nécessaires à leur communication à des tiers. Au cas où un tiers est titulaire d'un droit de propriété intellectuelle sur tout ou partie de ma thèse, je certifie avoir obtenu son autorisation écrite pour l'exercice des droits mentionnés ci-dessus. |
Page generated in 0.0028 seconds