Abstract
The transition from basic ASMs to Turbo ASMs reminds at the earlier transition from programming languages like FORTRAN and ALGOL58 to ALGOL60. Essential new features are on the ASM-side naming, parameterizing, local states and possible return values of rules and were on the ALGOL60-side procedures, block concept and function procedures with return values. Turbo ASM–theory and ALGOL60 have two central phenomena in common: Operational style of specifying and semantics definition and named rules and procedures with their potential of recursion. There are quite a few connections between Turbo ASM and ALGOL60. The close coupling of operational style and recursion becomes especially evident in Apt’s and Olderog’s proof of soundness of Hoare’s deduction rule for recursive ASM–rule resp. procedure calls.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Apt, K.R.: Ten years of Hoare’s logic, a survey, part I. ACM Transactions on Programming Languages and Systems 3, 431–483 (1981); Tech. Report, Fac. of Economics, Erasmus Univ. Rotterdam (April 1979)
Backus, J.W., et al.: The FORTRAN Automatic Coding System. In: Proc. Western Joint Computing Conf., vol. 11, pp. 188–198 (1957)
de Bakker, J.: Mathematical Theory of Program Correctness. Prentice Hall, Englewood Cliffs (1980)
Börger, E., Bolognesi, T.: Remarks on Turbo ASMs for Functional Equations and Recursion Schemes. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 218–228. Springer, Heidelberg (2003)
Börger, E., Stärk, R.: Abstract State Machines. Springer, Berlin (2003)
Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare–like axioms. J. Assoc. Comp. Mach. 26, 129–147 (1979)
Curry, H.B., Feys, R.: Combinatory Logic, vol. I. North– Holland, Amsterdam (1968)
Dijkstra, E.W.: Recursive Programming. Num. Math. 2, 312–318 (1960)
Floyd, R.W.: Assigning Meaning to Programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proc. Symp. in Applied Math., vol. 19, pp. 19–32. American Math. Soc., Providence (1967)
Fruja, N.G., Stärk, R.F.: The Hidden Computation Steps of Turbo Abstract State Machines. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 244–262. Springer, Heidelberg (2003)
Harel, D. (ed.): First-Order Dynamic Logic. LNCS, vol. 68. Springer, Heidelberg (1979)
Grau, A.A., Hill, U., Langmaack, H.: Translation of ALGOL60. In: Samelson, K. (chief ed.) Handbook for Automatic Computation Ib, Springer, Berlin (1967)
Hermes, H.: Aufzählbarkeit, Entscheidbarkeit, Berechenbarkeit. Springer, Berlin (1961)
Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580, 583 (1969)
Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.) Symposium on semantics of algorithmic languages. Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer, Berlin (1971)
Jensen, K., Wirth, N.: PASCAL User Manual and Report. Springer, Berlin (1975)
Kandzia, P.: On the “most recent” property of ALGOL–like programs. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 97–111. Springer, Heidelberg (1974)
Langmaack, H.: On Correct Procedure Parameter Transmission in Higher Programming Languages. Acta Informatica 2(2), 110–142 (1973)
Langmaack, H.: On procedures as open subroutines I, II. Acta Informatica 2, 311–333 (1973); Acta Informatica 3, 227–241 (1974)
Langmaack, H., Olderog, E.R.: Present–day Hoare–like systems for programming languages with procedures: power, limits and most likely extensions. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 363–373. Springer, Heidelberg (1980)
Langmaack, H.: On Termination Problems for Finitely Interpreted ALGOL– like Programs. Acta Informatica 18, 79–108 (1982)
Langmaack, H.: A new transformational approach to partial correctness proof calculi for ALGOL68–like programs with finite modes and simple side– effects. Annals of Discrete Mathematics 24, 73–102 (1985)
Langmaack, H.: Klaus Samelsons frühe Beiträge zur Informatikentwicklung. Informatik Spektrum 18, 132–137 (2002)
Lipton, R.J.: A necessary and sufficient condition for the existence of Hoare logics. In: 18th IEEE Symposium on Foundations of Comp. Sc.,, Providence, Rhode Island, pp. 1–6. IEEE, New York (1977)
Lippe, W.M., Simon, F.: A Formal Notion for Equivalence of ALGOL–like Programs. In: Robinet, B. (ed.) Transformationes de Programmes, 3e coll. int. sur la programmation, Paris, pp. 141–156. Dunod, Paris (1978)
McCarthy, J., et al.: Lisp 1.5 Programmer’s Manual. The M.I.T. Press, Cambridge (1965)
McGrowan, C.L.: The “most recent” error: its causes and correction. SIGPLAN Notices 7, 191–202 (1972)
Milne, R., Strachay, C.: A Theory of Programming Language Semantics, parts a, b. Chapman and Hall, Boca Raton (1976)
Mirkowska, G., Salwicki, A.: Algorithmic Logic. D.Reidel Publ. Comp./PWN–Polish Scient. Publ., Dordrecht/Warsaw (1987)
Naur, P., et al. (eds.): Report on the Algorithmic Language ALGOL60. Num. Math. 2, 106–136 (1960)
Nygaard, K.: Private communicaton. Oslo (2002)
Olderog, E.R.: Korrektheits- und Vollständigkeitsaussagen über Hoarsche Ableitungskalküle. Diplomarbeit, Christian-Albrechts-Univ. Kiel (1979)
Olderog, E.R.: Sound and Complete Hoare–like Calculi Based on Copy Rules. Acta Informatica 16, 161–197 (1981)
Olderog, E.R.: Chatacterisierung Hoarescher Systeme für ALGOL–ähnliche Programmiersprachen. Dissertation, Inst. f. Informatik u. Prakt. Math., Univ. Kiel, Bericht 5/81 (1981)
Olderog, E.R.: Correctness of Programs with Pascal–like Procedures without Global Variables. Theoretical Computer Science 30, 49–90 (1984)
Perlis, A.J., Samelson, K. (eds.): ACM Comunittee on Programming Languages and GAMM Comittee on Programming. Report on the Algorithmic Language ALGOL. Num.Math. 1, 41–60 (1959)
Poetzsch-Heffter, A., Müller, P.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (Hrsg.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Comp. Sc. Dept., Aarhus, Denmark (September 1981)
Salwicki, A.: Formalized Algorithmic Logic. Bull.PAS 18, 227–332 (1970)
Samelson, K.: Probleme der Programmierungstechnik. In: Int. Koll. ü. Probleme d. Rechentechnik, Dresden 1955, pp. 61–68. VEB Deutscher Verlag der Wissenschaften, Berlin (1957)
Samelson, K., Bauer, F.L.: Sequentielle Formelübersetzung. Elektr. Rechenanl. 1(4), 176–182 (1959)
Scott, D.S.: Outline of a Mathematical Theory of Computation. In: Proc. 4th Annual Princeton Conference on Information Sciences and Systems, Princeton, pp. 169–176 (1970)
Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer, Berlin (2001)
Stärk, R.F., Nanchen, S.: A logic for Abstract State Machines. J.UCS 7(11), 980–1005 (2001)
Turing, A.: Checking a Large Routine. In: Rep. Conf. High Speed Automatic Calculating Machines. Inst. of Comp. Sci. Univ. of Toronto, Ontario, Can. (January 1950)
van Wijngaarden, A., et al. (ed.) : Report on the Algorithmic Language ALGOL68. Num. Math. 14, 79–218 (1969)
Wilhelm, R., Maurer, D.: Übersetzerbau. Theorie, Konstruktion, Generierung. Springer, Berlin (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Langmaack, H. (2004). An ALGOL-View on Turbo ASM. In: Zimmermann, W., Thalheim, B. (eds) Abstract State Machines 2004. Advances in Theory and Practice. ASM 2004. Lecture Notes in Computer Science, vol 3052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24773-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-24773-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22094-7
Online ISBN: 978-3-540-24773-9
eBook Packages: Springer Book Archive