Abstract
Just claiming the importance of formal methods is not enough, it is necessary to teach programming using formal methods. Also, we have to convince students to use them in their programming. To fill this goal, two points seem necessary: a no-fault approach combined with (apparently) affordable proofs and the use of automatic provers.
More than twenty years ago, David Gries and others said that the goal should be to forbid the construction of incorrect programs by teaching constructions of correct programs using a no-fault approach. This point of view appears to us to be both simple and challenging for students, because teaching correct program construction means teaching methodologies based on a process with well-defined steps which decomposes into sub-tasks, each of which is human in scope. Human scope means the sub-tasks are considered obvious or easy to prove by humans; for example, easy to prove sub-tasks preferably do not require inductive proof.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lévy, M., Trilling, L. (1999). A PVS-based approach for teaching constructing correct iterations. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_52
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_52
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive