Testing and Error Detection for Formal Specification of Programming Languages and their Translation

在这项研究中，我们开发了测试和调试编程语言的正式规范及其翻译的方法(例如。,编译器)。有几种方法可以描述这样的规范。其中，我们采用了属性语法，它可以表达语义（静态语义）、执行（动态语义和解释）和翻译(例如。（代码生成）的编程语言。为了测试和调试正式规范，从实用的角度来看，以下两种工具是必要的：(a)当我们在规范中发现错误（在语义、执行和翻译方面）时帮助调试规范的工具，以及(b)从编程语言的正式规范及其翻译中生成用于测试规范的源程序的工具。对于(a)，我们将最初在逻辑编程语言调试中提出的算法调试技术应用于属性语法，开发了一种bug定位方法。我们进一步对算法进行了扩展，明确了算法与属性语法类的关系。我们使用一个名为Jun的生成器制作了一个原型系统，它基于一类属性语法。我们认为这项研究具有很高的独创性，因为以往的工作很少涉及系统的属性语法调试。至于(b)，我们开发了一种方法来生成语法和语义正确/不正确的源程序，给定编程语言的语法和语义。使用Prolog制作了一个原型系统。我们研究的一个特点是，我们可以通过设置属性语法的上下文条件（编程语言必须满足的语义条件）true/false来生成语义正确/错误的测试程序。

In this research we developed methods for testing and debugging the formal specification of programming languages and their translation(e.g., compilers).There are several ways to describe such a specification. Among others, we adopted the attribute grammar which can express the semantics(static semantics), execution(dynamic semantics and interpretation), and translation(e.g., code generation) of programming languages.In order to test and debug a formal specification, the following two kinds of tools are necessary from the practical point of view : (a) tools to assist debugging the specification when we find errors(in semantics, execution, and translation) in the specification, and(b) tools to generate source programs, to be used to test the specification, from the formal specification of the programming language and its translation.1.As for(a), we developed a bug locating method by applying the algorithmic debugging technique, originally proposed in debugging logic programming languages, to attribute grammars. We further made extensions to the algorithm and clarified the relation of the algorithm to attribute grammar classes. We made a prototype system using a generator called Jun, which is based on a class of attribute grammars. We think this research has high originality, since previous work rarely deals with systematic debugging of attribute grammars.2.As for(b), we developed a method for generating both syntactically and semantically correct/incorrect source programs, given the syntax and semantics of a programming language. A prototype system is made using Prolog. A characteristic feature of our research is that we can generate semantically correct/incorrect test programs by setting the context condition(semantic condition that a programming language must satisfy) of attribute grammars true/false.