Specification and verification of context conditions for programming languages

 

Show simple item record

dc.contributor.advisor MacGregor, Ken en_ZA
dc.contributor.author Kaplan, Simon Mark en_ZA
dc.date.accessioned 2015-12-20T15:43:14Z
dc.date.available 2015-12-20T15:43:14Z
dc.date.issued 1986 en_ZA
dc.identifier.citation Kaplan, S. 1986. Specification and verification of context conditions for programming languages. University of Cape Town. en_ZA
dc.identifier.uri http://hdl.handle.net/11427/15898
dc.description Bibliography: p. 204-211. en_ZA
dc.description.abstract Context conditions - also called static semantics - are the constraints on computer programs that cannot be reasonably expressed by a context-free grammar, but that can be statically checked without considering the execution properties - semantics - of the program. Such conditions tend to be arbitrary and complex. This thesis presents a new specification formalism called CFF/AML. This formalism is · designed to be both useful for the specification of programming languages to an environment generator and also simple to use. The driving insight behind CFF/AML is that a language specifier conceives of the context condition checks associated with a programming language syntax description in procedural terms. CFF/AML supports this view of context condition specification, thus simplifying the task of the language specifier. CFF/AML has been formally by constructing a temporal proof system for the metalanguage. This proof system can also be used to verify CFF/AML specifications. The construction of the temporal proof system for CFF/AML uncovered a deficiency in the existing theory, namely that there was no way to prove subprograms, especially recursive subprograms, correct. The theory was extended to handle recursive subprograms. The approach developed in this thesis allows recursive subprograms to be proven correct using the same approach as was used previously for iterative constructs. This thesis makes a number of contributions to Computer Science. An approach to language specification - CFF/AML - is developed that greatly reduces the problems associated with building a language specification for input to a programming language environment generator. The theory of temporal proof systems is extended to include a methodology for handling proofs of recursive subprograms. A formal description of the CFF/AML metalanguage has been developed using temporal logic as the framework for the description. This is the first attempt to use temporal logic for such a task. As CFF/AML constructs can be dynamically scoped, this development differs from that required for statically scoped languages. We have also used this temporal proof system formally to prove that context condition specifications are correct. These proofs are an advancement on earlier work in the field of formal reasoning about context condition specification as they allow formal proof of the correctness of evaluations, as well as proving termination. en_ZA
dc.language.iso eng en_ZA
dc.subject.other Computer Science en_ZA
dc.title Specification and verification of context conditions for programming languages en_ZA
dc.type Doctoral Thesis
uct.type.publication Research en_ZA
uct.type.resource Thesis en_ZA
dc.publisher.institution University of Cape Town
dc.publisher.faculty Faculty of Science en_ZA
dc.publisher.department Department of Computer Science en_ZA
dc.type.qualificationlevel Doctoral
dc.type.qualificationname PhD en_ZA
uct.type.filetype Text
uct.type.filetype Image
dc.identifier.apacitation Kaplan, S. M. (1986). <i>Specification and verification of context conditions for programming languages</i>. (Thesis). University of Cape Town ,Faculty of Science ,Department of Computer Science. Retrieved from http://hdl.handle.net/11427/15898 en_ZA
dc.identifier.chicagocitation Kaplan, Simon Mark. <i>"Specification and verification of context conditions for programming languages."</i> Thesis., University of Cape Town ,Faculty of Science ,Department of Computer Science, 1986. http://hdl.handle.net/11427/15898 en_ZA
dc.identifier.vancouvercitation Kaplan SM. Specification and verification of context conditions for programming languages. [Thesis]. University of Cape Town ,Faculty of Science ,Department of Computer Science, 1986 [cited yyyy month dd]. Available from: http://hdl.handle.net/11427/15898 en_ZA
dc.identifier.ris TY - Thesis / Dissertation AU - Kaplan, Simon Mark AB - Context conditions - also called static semantics - are the constraints on computer programs that cannot be reasonably expressed by a context-free grammar, but that can be statically checked without considering the execution properties - semantics - of the program. Such conditions tend to be arbitrary and complex. This thesis presents a new specification formalism called CFF/AML. This formalism is · designed to be both useful for the specification of programming languages to an environment generator and also simple to use. The driving insight behind CFF/AML is that a language specifier conceives of the context condition checks associated with a programming language syntax description in procedural terms. CFF/AML supports this view of context condition specification, thus simplifying the task of the language specifier. CFF/AML has been formally by constructing a temporal proof system for the metalanguage. This proof system can also be used to verify CFF/AML specifications. The construction of the temporal proof system for CFF/AML uncovered a deficiency in the existing theory, namely that there was no way to prove subprograms, especially recursive subprograms, correct. The theory was extended to handle recursive subprograms. The approach developed in this thesis allows recursive subprograms to be proven correct using the same approach as was used previously for iterative constructs. This thesis makes a number of contributions to Computer Science. An approach to language specification - CFF/AML - is developed that greatly reduces the problems associated with building a language specification for input to a programming language environment generator. The theory of temporal proof systems is extended to include a methodology for handling proofs of recursive subprograms. A formal description of the CFF/AML metalanguage has been developed using temporal logic as the framework for the description. This is the first attempt to use temporal logic for such a task. As CFF/AML constructs can be dynamically scoped, this development differs from that required for statically scoped languages. We have also used this temporal proof system formally to prove that context condition specifications are correct. These proofs are an advancement on earlier work in the field of formal reasoning about context condition specification as they allow formal proof of the correctness of evaluations, as well as proving termination. DA - 1986 DB - OpenUCT DP - University of Cape Town LK - https://open.uct.ac.za PB - University of Cape Town PY - 1986 T1 - Specification and verification of context conditions for programming languages TI - Specification and verification of context conditions for programming languages UR - http://hdl.handle.net/11427/15898 ER - en_ZA


Files in this item

This item appears in the following Collection(s)

Show simple item record