Grammar semantics, analysis and parsing by abstract interpretation. (English) Zbl 1248.68316
Grammar flow problems consist in computing a function of the proto language generated by the grammar for each nonterminal. In the paper under review, abstract interpretations of a fixpoint protoderivation semantics are studied, defining the maximal derivations of a transitional semantics of context-free grammars akin to pushdown automata. The result is a hierarchy of bottom-up or top-down semantics refining the classical equational and derivational language semantics and including Knuth grammar problems, classical grammar flow analysis algorithms and parsing algorithms. The paper is absolutely self-contained, providing also the mathematical background and the necessary elements of abstract interpretation.
Reviewer: Anna Labella (Roma)
MSC:
| 68Q55 | Semantics in the theory of computing |
| 68Q45 | Formal languages and automata |
| 68Q42 | Grammars and rewriting systems |
Keywords:
abstract interpretation; context-free grammar; bottom-up semantics; top-down semantics; abstract semantics; grammar flow analysis; grammar problemSoftware:
ALGOL 60References:
| [1] | Knuth, D., A generalization of Dijkstra’s algorithm, Information Processing Letters, 6, 1, 1-5 (1977) · Zbl 0363.68056 |
| [2] | Ramalingam, G.; Reps, T., An incremental algorithm for a generalization of the shortest-path problem, Journal of Algorithms, 21, 2, 267-305 (1996) · Zbl 0861.68035 |
| [3] | Bar-Hillel, J.; Perles, M.; Shamir, E., On formal properties of simple phrase structure grammars, Zeitschrift für Phonetik, Sprachwissenschaft und Kommunikationforschung, 14, 143-172 (1961) · Zbl 0106.34501 |
| [4] | Aho, A.; Ullman, J.; Parsing, The Theory of Parsing, Translation and Compiling, vol. 1 (1972), Prentice-Hall, Inc.: Prentice-Hall, Inc. Englewood Cliffs |
| [5] | Möncke, U.; Wilhelm, R., Iterative algorithms on grammar graphs, (Schneider, H.; Gottler, H., Proceedings of the Eight Conference on Graphtheoretic Concepts in Computer Science, WG’82 (1982), Hanser Verlag: Hanser Verlag Munchen), 177-194 · Zbl 0532.68080 |
| [6] | U. Möncke, Generierung von systemen zur transformation attributierter operatorbäume; komponenten des systems und mechanismen der generierung, Diplomarbeit, Universität des Saarlandes, Saarbrücken, 1985.; U. Möncke, Generierung von systemen zur transformation attributierter operatorbäume; komponenten des systems und mechanismen der generierung, Diplomarbeit, Universität des Saarlandes, Saarbrücken, 1985. |
| [7] | Möncke, U.; Wilhelm, R., Grammar flow analysis, (Alblas, H.; Melichar, B., Proceedings of the Attribute Grammars, Applications and Systems, International Summer School SAGA, Prague, 4-13 June, 1991. Proceedings of the Attribute Grammars, Applications and Systems, International Summer School SAGA, Prague, 4-13 June, 1991, Lecture Notes in Computer Science, vol. 545 (1991), Springer: Springer Heidelberg), 151-186 |
| [8] | Wilhelm, R.; Maurer, D., Übersetzerbau. Theorie, Konstruktion, Generierung (1992), Springer: Springer Heidelberg · Zbl 0757.68032 |
| [9] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1977), ACM Press: ACM Press New York, Los Angeles), 238-252 |
| [10] | Chomsky, N., Three models for the description of language, IEEE Transactions on Information Theory, 2, 3, 113-124 (1956) · Zbl 0156.25401 |
| [11] | Chomsky, N. (1957), de Gruyter: de Gruyter Mouton |
| [12] | A. Oettinger, Automatic syntactic analysis and the pushdown store, in: Proceedings of Symposia in Applied Math. 12.; A. Oettinger, Automatic syntactic analysis and the pushdown store, in: Proceedings of Symposia in Applied Math. 12. |
| [13] | Rutishauser, H., Automatische Rechenplanfertigung bei programmgesteuerten Rechenmaschinen, Zeitschrift für Angewandte Mathematik und, 32, 312-313 (1952), mitt. Nr. 3 aus dem Inst. f. Angew. Math. der ETH Zürich, 45 p., 1952, Birkhäuser, Basel · Zbl 0049.21203 |
| [14] | Boehm, C., Calculatrices digitales. du déchiffrage de formules logico-mathématiques par la machine même dans la conception du programme. dissertation eth zürich (1952), Annali di Matematica Pura ed Applicata, 4, 37, 5-47 (1954) |
| [15] | F. Bauer, K. Samuelson, Verfahren zur automatischen Verarbeitung von kodierten Daten und Rechenmaschine zur Ausübung des Verfahrens, deutsches Patentamt, Auslegeschrift 1094019, B441221X/42m. Anmeldetag: 30. März 1957. Bekanntmachung der Anmeldung und Ausgabe der Auslegeschrift: 1.Dezember 1960. Dr. Friedrich Ludwig Bauer und Dr. Klaus Samuelson, München, sind als Erfinder genannt worden. Erteilt 12.8.1971, DE-PS 1094019, 1957.; F. Bauer, K. Samuelson, Verfahren zur automatischen Verarbeitung von kodierten Daten und Rechenmaschine zur Ausübung des Verfahrens, deutsches Patentamt, Auslegeschrift 1094019, B441221X/42m. Anmeldetag: 30. März 1957. Bekanntmachung der Anmeldung und Ausgabe der Auslegeschrift: 1.Dezember 1960. Dr. Friedrich Ludwig Bauer und Dr. Klaus Samuelson, München, sind als Erfinder genannt worden. Erteilt 12.8.1971, DE-PS 1094019, 1957. |
| [16] | Samuelson, K.; Bauer, F., Sequentielle formelübersetzung, Elektronische Rechenanlagen, 1, 4, 176-182 (1959) · Zbl 0094.31406 |
| [17] | Bauer, F., From the stack principle to ALGOL, (Broy, M.; Denert, E., Software Pioneers: Contributions to Software Engineering (2002), Springer: Springer Heidelberg), 26-42 · Zbl 0997.68001 |
| [18] | Naur, P., The European side of the last phase of the development of ALGOL 60, (Wexelblat, R., History of Programming Languages I (1978), ACM Press: ACM Press New York), 92-139 |
| [19] | N. Chomsky, Context free grammars and pushdown storage, quarterly Progress Report 65, MIT Research Laboratory in Electronics, Cambridge, 1962.; N. Chomsky, Context free grammars and pushdown storage, quarterly Progress Report 65, MIT Research Laboratory in Electronics, Cambridge, 1962. |
| [20] | Evey, J., Application of pushdown store machines, (Proceedings of the 1963 Fall Joint Computer Conference (1963), AFIPS Press: AFIPS Press Montreal) · Zbl 0196.52501 |
| [21] | Schützenberger, M., On context free languages and pushdown automata, Information and Control, 6, 246-264 (1963) · Zbl 0123.12502 |
| [22] | Hoogeboom, H.; Engelfriet, J., Pushdown automata, (Martín-Vide, C.; Mitrana, V.; Paun, G., Formal Languages and Applications. Formal Languages and Applications, Studies in Fuzziness and Soft Computing, vol. 148 (2004), Springer: Springer Heidelberg), 117-138 · Zbl 1088.68089 |
| [23] | Autebert, J.; Berstel, J.; Boasson, L., Context-free languages and pushdown automata, (Rozenberg, G.; Salomaa, A., Word, Language, Grammar. Word, Language, Grammar, Handbook of Formal Languages, vol. 1 (1997), Springer: Springer Heidelberg) · Zbl 0900.68286 |
| [24] | Ginsburg, S., The Mathematical Theory of Context-Free Languages (1966), McGraw-Hill: McGraw-Hill New York · Zbl 0184.28401 |
| [25] | Cousot, P., Constructive design of a hierarchy of semantics of a transition system by abstract interpretation, Theoretical Computer Science, 277, 1—2, 47-103 (2002) · Zbl 0996.68119 |
| [26] | Cousot, P., Semantic foundations of program analysis, invited chapter, (Muchnick, S.; Jones, N., Program Flow Analysis: Theory and Applications (1981), Prentice-Hall, Inc.: Prentice-Hall, Inc. Englewood Cliffs), 303-342, (Chapter 10) · Zbl 0468.68002 |
| [27] | Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1979), ACM Press: ACM Press New York, San Antonio), 269-282 · Zbl 0788.68094 |
| [28] | Cousot, P.; Cousot, R., Constructive versions of Tarski’s fixed point theorems, Pacific Journal of Mathematics, 82, 1, 43-57 (1979) · Zbl 0413.06004 |
| [29] | Ginsburg, S.; Rice, G., Two families of languages related to ALGOL, Journal of the Association for Computing Machinery, 9, 350-371 (1962) · Zbl 0196.01803 |
| [30] | Schützenberger, M., On a theorem of R. Jungen, Proceedings of the American Mathematical Society, 13, 885-889 (1962) · Zbl 0107.03102 |
| [31] | Chomsky, N.; Schützenberger, M., The algebraic theory of context-free languages, (Bradford, P.; Hirschberg, D., Computer programming and Formal Systems (1963), North-Holland Pub. Co.: North-Holland Pub. Co. Amsterdam), 118-161 · Zbl 0148.00804 |
| [32] | Aho, A.; Sethi, R.; Ullman, J., Compilers. Principles, Technique and Tools (1986), Addison-Wesley Pub. Co.: Addison-Wesley Pub. Co. Reading |
| [33] | Dijkstra, E., A note on two problems in connexion with graphs, Numerische Mathematik, 1, 269-271 (1959) · Zbl 0092.16002 |
| [34] | Hays, D., Introduction to Computational Linguistics (1967), American Elsevier: American Elsevier New York · Zbl 0166.42004 |
| [35] | Younger, D., Recognition and parsing of context-free languages in time \(n^3\), Information and Control, 10, 2, 609-617 (1967) · Zbl 0149.24803 |
| [36] | T. Kasami, An efficient recognition and syntax analysis algorithm for context-free languages, Tech. Rep., Air Force Cambridge Research Laboratory, Bedford, August 1965.; T. Kasami, An efficient recognition and syntax analysis algorithm for context-free languages, Tech. Rep., Air Force Cambridge Research Laboratory, Bedford, August 1965. |
| [37] | McCarthy, J.; Painter, J., Correctness of a compiler for arithmetic expressions, (Schwartz, J., Proceedings of the Symposium in Applied Mathematics. Proceedings of the Symposium in Applied Mathematics, Mathematical Aspects of Computer Science, vol. 19 (1967), American Mathematical Society: American Mathematical Society Providence), 33-41 · Zbl 0183.19201 |
| [38] | Leroy, X., Formal certification of a compiler back-end or: programming a compiler with a proof assistant, (Conference Record of the Thirtythird Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2006), ACM Press: ACM Press New York, Charleston), 42-54 · Zbl 1369.68124 |
| [39] | Leroy, X., Coinductive big-step operational semantics, (Sestoft, P., Proceedings of the Fifteenth European Symposium on Programming Languages and Systems. Proceedings of the Fifteenth European Symposium on Programming Languages and Systems, Lecture Notes in Computer Science, vol. 3924 (2006), Springer: Springer Heidelberg), 54-68 · Zbl 1178.68330 |
| [40] | Cousot, P., The calculational design of a generic abstract interpreter, invited chapter, (Broy, M.; Steinbrüggen, R., Calculational System Design. Calculational System Design, NATO Science Series, Series F: Computer and Systems Sciences, vol. 173 (1999), IOS Press: IOS Press Amsterdam), 421-505 · Zbl 0945.68032 |
| [41] | D. Pichardie, Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés, Ph.D. Thesis, Université de Rennes I, December 2005.; D. Pichardie, Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés, Ph.D. Thesis, Université de Rennes I, December 2005. |
| [42] | Cousot, P.; Cousot, R.; Giacobazzi, R., Abstract interpretation of resolution-based semantics, Theoretical Computer Science, 410, 46, 4724-4746 (2009) · Zbl 1187.68307 |
| [43] | Päun, G., Marcus Contextual Grammars, Studies in Linguistics and Philosophy (1997), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht · Zbl 0965.68037 |
| [44] | Ehrenfeucht, A.; Päun, G.; Rozenberg, G., Contextual grammars and formal languages, (Rozenberg, G.; Salomaa, A., Handbook of Formal Languages, vol. 2 (1997), Springer: Springer Heidelberg), 237-293 · Zbl 0866.68057 |
| [45] | Boullier, P., From contextual grammars to range concatenation grammars, Electronic Notes in Theoretical Computer Science, 53, 41-52 (2001) · Zbl 1263.68068 |
| [46] | Davey, B.; Priestley, H., Introduction to Lattices and Order (2002), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1002.06001 |
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.
