Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

ON THE CORRECTNESS OF SEMANTIC-SYNTAX-DIRECTED TRANSLATIONS

IP.com Disclosure Number: IPCOM000128004D
Original Publication Date: 1977-Dec-31
Included in the Prior Art Database: 2005-Sep-14
Document File: 20 page(s) / 47K

Publishing Venue

Software Patent Institute

Related People

Ramachandran Krishnaswamy: AUTHOR [+4]

Abstract

There has been a considerable flurry of interest in proving that a program is "correct" with respect to a given set of specifica-tions (Wegbreit [15], Dijkstra [4], King [8], Floyd [5]). This concern is motivated by the highly pragmatic fact that failures in installed software can be disasterous. A program which translates the sentences of one large, complex language to the sentences of another will itself be large and complex. Hence, such transla-tors are error-prone. A utility program such as a compiler or one which translates (looking into the future) diplomatic mes-sages which errs is intolerable. This paper presents several theorems concerning the correctness of semantic-syntax-directed translators (SSDT). The SSDT was introduced by Pyster and Buttelmann [13]. It is a generalization of the syntax-directed translator (SDT.) studied by Aho and U11-man [1], and by Buttelmann [3] among others. The 5SDT differs . from the SDT chiefly by using semantic information to in part compute the translation of a sentence. Benson [2] and Buttel-mann [3] both investigated conditions under which SDT are "semantic-preserving" or "correct".. This paper generalizes their results to the SSDT and examines correctness issues not ,addressed by either. We show that under stated conditions an SSDT can be proven correct. We also examine under what condi-tions it is decidable whether a given SSDT is provably correct. The paper itself~has six sections. The second section intro-duces needed terms and notations. The language model itself, a variant of Knuth's attributed grammar [9,10], is presented in section 3. Our translation model, the SSDT, is defined and briefly characterized in the fourth section. The correctness results are presented in section 5, and finally, the last sec-tion includes a summary and conclusions.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 11% of the total text.

Page 1 of 20

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

ON THE CORRECTNESS OF SEMANTIC-SYNTAX-DIRECTED TRANSLATIONS

By

Ramachandran Krishnaswamy Arthur Pyster

Technical Report X77-5

1. INTRODUCTION

There has been a considerable flurry of interest in proving that a program is "correct" with respect to a given set of specifica-tions (Wegbreit [15], Dijkstra [4], King [8], Floyd [5]). This concern is motivated by the highly pragmatic fact that failures in installed software can be disasterous. A program which translates the sentences of one large, complex language to the sentences of another will itself be large and complex. Hence, such transla-tors are error-prone. A utility program such as a compiler or one which translates (looking into the future) diplomatic mes-sages which errs is intolerable.

This paper presents several theorems concerning the correctness of semantic-syntax-directed translators (SSDT). The SSDT was introduced by Pyster and Buttelmann [13]. It is a generalization of the syntax-directed translator (SDT.) studied by Aho and U11-man [1], and by Buttelmann [3] among others. The 5SDT differs . from the SDT chiefly by using semantic information to in part compute the translation of a sentence. Benson [2] and Buttel-mann [3] both investigated conditions under which SDT are "semantic-preserving" or "correct".. This paper generalizes their results to the SSDT and examines correctness issues not ,addressed by either. We show that under stated conditions an SSDT can be proven correct. We also examine under what condi-tions it is decidable whether a given SSDT is provably correct. The paper itself~has six sections. The second section intro-duces needed terms and notations. The language model itself, a variant of Knuth's attributed grammar [9,10], is presented in section 3. Our translation model, the SSDT, is defined and briefly characterized in the fourth section. The correctness results are presented in section 5, and finally, the last sec-tion includes a summary and conclusions.

2. BASIC TERMS

Several concepts and notations must. be introduced before pro-ceeding further. We introduce them here. We presume the read-er is familiar with basic formal language theory as found in Hopcroft and Ullman [7].

The empty set will be denoted by (D; the powerset of set A by 2A; the length of string w by iwj; the set of non-negative in-tegers by INT; the domain of function f by dom(f), and its range by ran(f); the k-th element of ordered set w or the k-th character of string w by wk; and the set {1,...,n}.by n.

Iowa State University Page 1 Dec 31, 1977

Page 2 of 20

ON THE CORRECTNESS OF SEMANTIC-SYNTAX-DIRECTED TRANSLATIONS

A labelled ordered tree is defined recursively either as (i) a symbol B; or (ii) B(tl,...,tn) where B is a symbol, and tl,...,tn are themselves labelled ordered trees. The height, root, and frontier of a tree are defined in the standard way as given in Buttelmann [3]. The set of nodes of a tree t is nodes(t)....