Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
Specification and verification of context conditions for programming languages
Bibliography: p. 204-211.
Saved in:
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
Department of Computer Science
2015
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613143678582784 |
|---|---|
| access_status_str | Open Access |
| author | Kaplan, Simon Mark |
| author2 | MacGregor, Ken |
| author_browse | Kaplan, Simon Mark MacGregor, Ken |
| author_facet | MacGregor, Ken Kaplan, Simon Mark |
| author_sort | Kaplan, Simon Mark |
| collection | Thesis |
| description | Bibliography: p. 204-211. |
| format | Thesis |
| id | oai:open.uct.ac.za:11427/15898 |
| institution | University of Cape Town (South Africa) |
| language | eng |
| last_indexed | 2026-06-10T12:31:28.055Z |
| license_str | Not specified — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from UCTD — University of Cape Town Open Access Repository |
| publishDate | 2015 |
| publishDateRange | 2015 |
| publishDateSort | 2015 |
| publisher | Department of Computer Science |
| publisherStr | Department of Computer Science |
| record_format | dspace |
| source_str | UCTD — University of Cape Town Open Access Repository |
| spelling | oai:open.uct.ac.za:11427/15898 Specification and verification of context conditions for programming languages Kaplan, Simon Mark MacGregor, Ken Computer Science Bibliography: p. 204-211. 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. 2015-12-20T15:43:14Z 2015-12-20T15:43:14Z 1986 Doctoral Thesis Doctoral PhD http://hdl.handle.net/11427/15898 eng application/pdf Department of Computer Science Faculty of Science University of Cape Town |
| spellingShingle | Computer Science Kaplan, Simon Mark Specification and verification of context conditions for programming languages |
| thesis_degree_str | Doctoral |
| title | Specification and verification of context conditions for programming languages |
| title_full | Specification and verification of context conditions for programming languages |
| title_fullStr | Specification and verification of context conditions for programming languages |
| title_full_unstemmed | Specification and verification of context conditions for programming languages |
| title_short | Specification and verification of context conditions for programming languages |
| title_sort | specification and verification of context conditions for programming languages |
| topic | Computer Science |
| url | http://hdl.handle.net/11427/15898 |
| work_keys_str_mv | AT kaplansimonmark specificationandverificationofcontextconditionsforprogramminglanguages |