×

Structural operational semantics through context-dependent behaviour. (English) Zbl 1223.68026

Summary: We present a new approach to providing a structural operational semantics for imperative programming languages with concurrency and procedures. The approach is novel because we expose the building block operations-variable assignment and condition checking-in the labels on the transitions; these form the context-dependent behaviour of a program. Using this style results in two main advantages over standard formalisms for imperative programming language semantics: firstly, our individual transition rules are more concise, and secondly, we are able to more abstractly and intuitively describe the semantics of procedures, including by-value and by-reference parameters. Standard techniques in the literature tend to result in complex and hard-to-read rules for even simple language constructs when procedures and parameters are dealt with.
Our semantics for procedures utilises the context-dependent behaviour in the transition label to handle variable name scoping, and defines the semantics of recursion without requiring additional rules. In contrast with Plotkin’s seminal structural operational semantics paper, we do not use locations to describe some of the more complex language constructs. Novel aspects of the abstract syntax include local states (in contrast to a single global store), which simplifies the reasoning about local variables, and a command for dynamically renaming variables (in contrast to mapping variables to locations), which simplifies the reasoning about the effect of procedures on by-reference parameters.

MSC:

68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

ALGOL 60
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Birrell, A.; Harris, T.; Isard, M., Semantics of transactional memory and automatic mutual exclusion, ACM Trans. Program. Lang. Syst., 33, 1, 2:1-2:50 (2011)
[2] Aceto, L.; Fokkink, W.; Verhoef, C., Structural operational semantics, (Bergstra, J.; Ponse, A.; Smolka, S., Handbook of Process Algebra (2001), Elsevier Science), 197-292 · Zbl 1062.68074
[3] Backus, J. W.; Bauer, F. L.; Green, J.; Katz, C.; McCarthy, J.; Perlis, A. J.; Rutishauser, H.; Samelson, K.; Vauquois, B.; Wegstein, J. H.; van Wijngaarden, A.; Woodger, M.; Naur, P., Revised report on the algorithm language ALGOL 60, Commun. ACM, 6, 1, 1-17 (1963) · Zbl 0108.30206
[4] Baeten, J. C.M.; Bergstra, J. A., Global renaming operators in concrete process algebra, Inform. Comput., 78, 3, 205-245 (1988) · Zbl 0651.68031
[5] Baeten, J. C.M.; Bergstra, J. A., Process algebra with propositional signals, Theor. Comput. Sci., 177, 2, 381-405 (1997) · Zbl 0901.68117
[6] Bergstra, J. A.; Klop, J. W., Process algebra for synchronous communication, Inform. Control, 60, 1-3, 109-137 (1984) · Zbl 0597.68027
[7] Colvin, R.; Hayes, I. J., CSP with hierarchical state, (Leuschel, M.; Wehrheim, H., Integrated Formal Methods. Integrated Formal Methods, Lecture Notes in Comp. Sci, vol. 5423 (2009), Springer), 118-135 · Zbl 1211.68266
[8] Colvin, R. J.; Hayes, I. J., A semantics for Behavior Trees using CSP with specification commands, Sci. Comput. Programming, 76, 10, 891-914 (2011) · Zbl 1220.68050
[9] Gadducci, F.; Montanari, U., The tile model, (Plotkin, G. D.; Stirling, C.; Tofte, M., Proof, Language, and Interaction, Essays in Honour of Robin Milner (2000), The MIT Press), 133-166
[10] (Gries, D., The Science of Programming (1981), Springer-Verlag) · Zbl 0472.68003
[11] Groote, J. F.; Mousavi, M. R.; Reniers, M. A., A hierarchy of SOS rule formats, Electron. Notes Theor. Comput. Sci., 156, 1, 3-25 (2006), (Proceedings of the Second Workshop on Structural Operational Semantics (SOS 2005)) · Zbl 1273.68206
[12] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall, Inc.: Prentice-Hall, Inc. Upper Saddle River, NJ, USA · Zbl 0637.68007
[13] Ishtiaq, S. S.; O’Hearn, P. W., BI as an assertion language for mutable data structures, (Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2001), ACM Press), 14-26 · Zbl 1323.68077
[14] Jaskelioff, M.; Ghani, N.; Hutton, G., Modularity and implementation of mathematical operational semantics, Electron. Notes Theor. Comput. Sci., 229, 5, 75-95 (2011), (Proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008)) · Zbl 1291.68123
[15] Jones, C. B., Operational semantics: concepts and their expression, Inform. Process. Lett., 88, 1-2, 27-32 (2003) · Zbl 1178.68329
[16] Jones, C. B., Understanding programming language concepts via operational semantics, (George, C.; Liu, Z.; Woodcock, J., Domain Modeling and the Duration Calculus. Domain Modeling and the Duration Calculus, International Training School, Advanced Lecture, Lecture Notes in Computer Science, vol. 4710 (2007), Springer), 177-235 · Zbl 1145.68374
[17] Kleymann, T., Hoare logic and auxiliary variables, Formal Asp. Comput., 11, 5, 541-566 (1999) · Zbl 0978.03026
[18] Klin, B., Bialgebras for structural operational semantics: an introduction, Theor. Comput. Sci. (2011), (Corrected Proof) · Zbl 1246.68150
[19] Leroy, X.; Grall, H., Coinductive big-step operational semantics, Inform. and Comput., 207, 2, 284-304 (2009) · Zbl 1165.68044
[20] Matthews, J.; Findler, R. B., Operational semantics for multi-language programs, ACM Trans. Program. Lang. Syst., 31, 3, 12:1-12:44 (2009)
[21] McCarthy, J., Recursive functions of symbolic expressions and their computation by machine, Part I, Commun. ACM, 3, 4, 184-195 (1960) · Zbl 0101.10413
[22] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[23] Milner, R.; Tofte, M.; MacQueen, D., The Definition of Standard ML (1997), MIT Press: MIT Press Cambridge, MA, USA
[24] Morgan, C., Programming from Specifications (1994), Prentice Hall · Zbl 0829.68083
[25] Mosses, P. D., Pragmatics of modular SOS, (Kirchner, H.; Ringeissen, C., Algebraic Methodology and Software Technology, 9th International Conference AMAST 2002, Proceedings. Algebraic Methodology and Software Technology, 9th International Conference AMAST 2002, Proceedings, Lecture Notes in Computer Science, vol. 2422 (2002), Springer), 21-40 · Zbl 1275.68086
[26] Mosses, P. D., Modular structural operational semantics, J. Log. Algebr. Program., 60-61, 195-228 (2004) · Zbl 1072.68061
[27] Mosses, P. D., Exploiting labels in structural operational semantics, Fundam. Inform., 60, 1-4, 17-31 (2004) · Zbl 1083.68066
[28] Mosses, P. D.; New, M. J., Implicit propagation in structural operational semantics, Electron. Notes Theor. Comput. Sci., 229, 4, 49-66 (2009) · Zbl 1339.68159
[29] Mousavi, M. R.; Reniers, M. A.; Groote, J. F., Notions of bisimulation and congruence formats for SOS with data, Inform. and Comput., 200, 1, 107-147 (2005) · Zbl 1082.68075
[30] Mousavi, M. R.; Reniers, M. A.; Groote, J. F., SOS formats and meta-theory: 20 years after, Theor. Comput. Sci., 373, 3, 238-272 (2007) · Zbl 1111.68069
[31] Owens, S., A sound semantics for OCaml light, (Drossopoulou, S., European Symposium on Programming (ESOP). European Symposium on Programming (ESOP), Lecture Notes in Computer Science, vol. 4960 (2008), Springer), 1-15 · Zbl 1133.68308
[32] G.D. Plotkin, A structural approach to operational semantics, Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, 1981.; G.D. Plotkin, A structural approach to operational semantics, Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
[33] Plotkin, G. D., A structural approach to operational semantics, J. Log. Algebr. Program., 60-61, 17-139 (2004) · Zbl 1082.68062
[34] Plotkin, G. D., The origins of structural operational semantics, J. Log. Algebr. Program., 60-61, 3-15 (2004) · Zbl 1072.68063
[35] Reynolds, J. C., Theories of Programming Languages (1998), Cambridge University Press · Zbl 0972.68507
[36] Reynolds, J. C., Separation logic: a logic for shared mutable data structures, (IEEE Symposium on Logic in Computer Science (LICS) (2002), IEEE Computer Society), 55-74
[37] Reynolds, J. C., An overview of separation logic, (Meyer, B.; Woodcock, J., Verified Software: Theories, Tools, Experiments (VSTTE). Verified Software: Theories, Tools, Experiments (VSTTE), Lecture Notes in Computer Science, vol. 4171 (2005), Springer), 460-469
[38] Roscoe, A., The Theory and Practice of Concurrency (1998), Prentice Hall
[39] Schneider, S., Concurrent and Real-time Systems: The CSP Approach (2000), Wiley
[40] Sebesta, R. W., Concepts of Programming Languages (2008), Addison-Wesley · Zbl 1130.68034
[41] Turi, D.; Plotkin, G. D., Towards a mathematical operational semantics, (IEEE Symposium on Logic in Computer Science (LICS) (1997), IEEE Computer Society), 280-291
[42] van Beek, D. A.; Man, K. L.; Reniers, M. A.; Rooda, J. E.; Schiffelers, R. R.H., Syntax and consistent equation semantics of hybrid \(\chi \), J. Log. Algebr. Program., 68, 1-2, 129-210 (2006) · Zbl 1088.68111
[43] von Oheimb, D., Hoare logic for mutual recursion and local variables, (Rangan, C. P.; Raman, V.; Ramanujam, R., Foundations of Software Technology and Theoretical Computer Science (FSTTCS). Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Lecture Notes in Computer, vol. 1738 (1999), Springer), 168-180 · Zbl 0956.68086
[44] Winskel, G., The Formal Semantics of Programming Languages: An Introduction (1993), MIT Press · Zbl 0919.68082
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.