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

编程语言及其翻译的形式规范的测试和错误检测

基本信息

批准号：
05680269
负责人：
SASSA Masataka
金额：
$ 1.28万
依托单位：
Tokyo Institute of Technology
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1993
资助国家：
日本
起止时间：
1993 至 1994
项目状态：
已结题

项目摘要

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.

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