Logic-based specification of visibility rules
The paper describes a new, declarative method for the formal specification of visibility rules. In contrast to common methods that are based on the specification of a symboltable (or environment), of appropriate update operations and of passing rules, the presented method is related to visibility descriptions in language reports. It consists of three steps: First, the program entities are specified, i.e. the candidates for the meaning of an identifier; the next step defines the ranges where the program entities are valid or hidden; finally, visibility is expressed in terms of these ranges. To formally define the semantics of these visibility specifications, a modeltheoretic view of abstract syntaxtrees is sketched. Using this framework, we give a fixpoint semantics for such specifications.
KeywordsPredicate Symbol Program Point Visibility Description Contextual Constraint Visibility Specification
Unable to display preview. Download preview PDF.
- [ANS83]ANSI. Pascal Computer Programming Language, ansi/ieee 770 x3.97-1983 edition, 1983.Google Scholar
- [End72]H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.Google Scholar
- [GS86]Y. Gurevich and S. Shelah. Fixed-point extensions of first-order logic. Annals of pure and applied logic, 32, 1986.Google Scholar
- [Jon80]N. D. Jones, editor. Semantics-Directed Compiler Generation, volume 94 of Lecture Notes in Computer Science. Springer Verlag, 1980.Google Scholar
- [Ode89]M. Odersky. A New Approach to Formal Language Definition and its Application to Oberon. PhD thesis, Swiss Federal Institute of Technology (ETH) Zürich, 1989. Diss. ETH No. 8938.Google Scholar
- [PH91]A. Poetzsch-Heffter. Context-dependent Syntax of programming languages: A New Specification Method and its Application. PhD thesis, Technische Universität München, 1991. (to appear in german).Google Scholar
- [Rei83]S. Reiss. Generation of compiler symbol processing mechanisms from specifications. ACM Transactions on Programming Languages and Systems, 5(2), 1983.Google Scholar
- [SH86]G. Snelting and W. Henhapl. Unification in many-sorted algebras as a device for incremental semantic analysis. Conference Record of the Thirteenth ACM Symposium on Principles of Programming Languages, 1986.Google Scholar
- [Tar55]A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 5, 1955.Google Scholar
- [Ua82]J. Uhl and andere. An Attribute Grammar for the Semantic Analysis of Ada. Lecture Notes in Computer Science 139, 1982.Google Scholar
- [Uhl86]J. Uhl. Spezifikation von Programmiersprachen und Übersetzern, volume 161 of GMD-Bericht. R. Oldenbourg Verlag, 1986.Google Scholar
- [Wat84]D. A. Watt. Contextual constraints. In B. Lorho, editor, Methods and Tools for Compiler Construction, pages 45–80. Cambridge University Press, 1984.Google Scholar