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

在这项研究中，我们开发了测试和调试编程语言及其翻译的形式规范的方法（例如，有几种方法来描述这样的规范。其中，我们采用了属性语法，它可以表达语义（静态语义），执行（动态语义和解释）和翻译（例如，为了测试和调试一个正式的规范，从实际的角度来看，以下两种工具是必要的：（a）当我们发现错误时，协助调试说明书的工具（在语义、执行和翻译方面），以及（B）生成源程序的工具，用于测试规范，1.对于（a），我们将最初在调试逻辑程序设计语言中提出的算法调试技术应用于属性文法，提出了一种错误定位方法。对该算法作了进一步的扩展，并阐明了该算法与属性文法类的关系。我们使用一个名为Jun的生成器实现了一个原型系统，该生成器基于一类属性文法。我们认为这项研究具有很高的独创性，因为以前的工作很少涉及属性语法的系统调试。2.对于（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.