128Accesses
3Citations
Abstract
Although formal programming is considered a recognised programming model, many avoid teaching it because of its very high mental cost. For that reason we developed a “microscopic” environment based on Emil Post's theoretical machine as an introduction to formal methods of programming and in the framework of an introductory computer science course.
In this paper, we present a small formal system for the development and simultaneous verification of algorithms; we give an example of problem solving in this environment; we present a small existing software simulating Post's machine; we propose two modules to facilitate the work in this environment; and finally, we present the didactic uses of Post's machine as an introduction to formal methods.
This is a preview of subscription content,log in via an institution to check access.
Access this article
Subscribe and save
- Get 10 units per month
- Download Article/Chapter or eBook
- 1 Unit = 1 Article or 1 Chapter
- Cancel anytime
Buy Now
Price includes VAT (Japan)
Instant access to the full article PDF.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Böhm, C. and Jacopini, G. (1966) Flow diagrams, tuning machines and languages with only two formation rules.Communications of the ACM,9(5), 366–371.
Bourbaki, N. (1948) L'architecture des mathe´matiques, InLe Lionnais: Les grands courants de la pensée mathématique, Edition des cahiers du sud.
Brusilovski, P., Calabrese, E., Hvorecky, J., Kouchnirenko, A. and Miller, P. (1997) Mini-languages: a way to learn programming principles.Education and Information Technologies,2, 65–83.
Dagdilelis, V. and Satratzemi, M. (1998) Post's machine picoworld as a bridge between programming and mathematics: didactic considerations.International Conference on the Teaching of Mathematics, July 3-6, Samos, Greece.
Dagdilelis, V. (1996) Teaching of programming: students' conceptions for development and verification of programs and didactic situations for their configuration.Ph.D. thesis, University of Macedonia, Dept. of Applied Informatics.
de Millo, R. A., Lipton, R. J., Perlis, A. J. (1979) Social processes and proofs of theorems and programs.Communications of the ACM,22(5), 271–280.
Dijkstra, E. W. (1972) The Humble programmer.Communications of the ACM,15(15), 859–866.
Floyd, R. W. (1968) Assigning meaning to Programs. InProceedings of Symposia in Applied Mathematics, XIX, 19–33.
Gries, D. (1981)The Science of Programming. Springer-Verlag, New York.
Hoare, C. A. R. (1969) An axiomatic basis for computer programming.Communications of the ACM,12(10), 576–580.
Hoare, C. A. R., Hayes, I. J., He Jifeng, Morgan, C. C., Roscoe, A. W., Sanders, J. W., Sorensen, I. H., Spivey, J. M. and Sufrin, B. A. (1987) Laws of programming.Communications of the ACM,30(8), 672–686.
Hoffstadter, D. R. (1989)Godel, Escher, Bach: An Eternal Golden Braid. Vintage Books, New York.
Knuth, D. E. (1973) Structured programming with GO TO statements.Computing Surveys,6, 4.
Knuth, D. E. (1974) Computer programming as an art.Communications of the ACM,17(12), 667–673.
Kuhn, T. S. (1983)La structure des revolutions scientifiques, Flammarion, Paris, (translation from English).
Post, E. (1939) Finite Combinatory process-formulation 1.The Journal of Symbolic Logic.
Stanford Verification Group: 1979,Stanford Pascal Verifier User Manual, Group Report 11.
Turing, A. (1939) On computational numbers with an application of the Entscheidungsproblem.Proceedings of London Mathematical Society.
Uspensky, V. A. (1983)Post's Machine. MIR Publishers, Moscow.
Wirth, N. (1975)Introduction à la programmation systématique. Masson, Paris, translation from German.
Author information
Authors and Affiliations
Department of Educational and Social Policy, University of Macedonia, 156 Egnatia Str., P.O. Box 1591, 54006, Thessaloniki, Greece
V. Dagdilelis
Department of Applied Informatics, University of Macedonia, 156 Egnatia str, P. O. Box 1591, 54006, Thessaloniki, Greece
M. Satratzemi
- V. Dagdilelis
You can also search for this author inPubMed Google Scholar
- M. Satratzemi
You can also search for this author inPubMed Google Scholar
Rights and permissions
About this article
Cite this article
Dagdilelis, V., Satratzemi, M. Post's Machine: A Didactic Microworld as an Introduction to Formal Programming.Education and Information Technologies6, 123–141 (2001). https://doi.org/10.1023/A:1012319900191
Issue Date:
Share this article
Anyone you share the following link with will be able to read this content:
Sorry, a shareable link is not currently available for this article.
Provided by the Springer Nature SharedIt content-sharing initiative