中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 中科院软件所  > 中科院软件所
题名:
基于上下文无关语言递归函数的规约语言研究
作者: 陈海明
答辩日期: 1999
专业: 计算机软件
授予单位: 中国科学院软件研究所
授予地点: 中国科学院软件研究所
学位: 博士
关键词: 递归函数 ; 上下文无关语言 ; 形式规约语言 ; 求值 ; 实现 ; 解释器
摘要: 上下文无关语言递归函数(简称CFRF)是专为描述计算机上的非数值算法而提出的,特点是能够非常直接地描述结构对象的加工算法。本文研究基于CFRF的形式规约语言及其实现方法,并用于形式规约的获取和检验工作。为研究语言,首先从实用性出发,对上下文无关语言原始递归函数(简称CFPRF)的定义形式进行扩充。提出了比CFPRF原始定义条件更宽的另一种联立递归式、多重归纳式和部分构造式,并证明它们是CFPRF。进而得到一个函数类CFPRF~+,它以CFPRF为真子类。我们还讨论了CFPRF~~+与CFRF的关系。提出了形式规约语言LFC(Language for CFRF)。它支持包括CFRF、数上递归函数和字上递归函数在内的多种类递归函数,提供了基于CFPRF的联立递归式和上述定义式的数种函数定义手段,支持的函数类CFPRF~+。LFC语言也是一个通用的函数式语言,除了具备一般函数式语言所具有的特点(如引用透明性、简洁、良好的数学特性等)外,还因基于CFRF而特别适于描述复杂结构对象的算法。LFC语言把上下文无关语言(简称CFL)作为数据类型,这种类型的表达式是使用通用字连接函数形成的隐式结构的表达式,具有很强的表示能力和灵活性。LFC具有高次、可执行、能证明的特点。由于上下文无关文法可以通过机器学习方法获得,CFRF可以用结构归纳法通过机器辅助构造形成,因此LFC适于形式规约的机器辅助获取。所得到的规约可以进行原型速成,因此得到检验。LFC还与规约库相联系,使规约获取和检验的交互性得到较好的支持。在实现方面,研究了LFC语言的实现方法。根据CFRF的特点,提出了面向树的计算方法,它是一种对于用各种定义方式定义的CFRF都适合的通用实现方法。为此,设计了表达式的一种可以表示出结构的表示形式,以及基于这种表示形式的LFC的中间表示形式。CFL之间的相等、包含和相交关系的不可判定性,结LFC的类型检查带来了困难。我们提出了LFC的一个实用类型系统,给出了相应的算法,从而可以实现表达式形式的转换。在此基础上,设计了LFC函数定义到中间表示表式的翻译和变换方法,包括对函数递归参数和定义形式的分析,参数一致化,模式的表达式表示形式的翻译,部分构造式达到完全构造式的变换,如模式匹配翻译等,我们还讨论了LFC中间表示形式的实现方法,设计了一种利用Scheme解释器的快速实现方法,实现了中间表示形式到Scheme的翻译。本文工作首次把CFL作为函数式语言的数据类型,并研究了表达式表示形式和类型系统等有关问题,它们可为相关研究提供参考。根据以上研究,在机器上实现了LFC的解释器,和实验性运算构造和检验系统FC(Function Constructor),并作为形式规约获取系统SAQ的一个子系统。还进行了实验,检验了本文的研究结果。
英文摘要: Recursive functions defined on context free languages (CFRF for short) are proposed especially for expressing non-numeric algorithms used on computers, having the feature of describing algorithms fairly directly for structured objects. In this thesis a formal specification language based on CFRF and its implementation method are studied, which is then used in specification acquisition and checking. In order to design the language, we first make some extensions to the definition form of primitive recursive functions defined on context free languages (CFPRF for short) for practical purposes. A mutually recursive form which is less restricted than the original definition form of CFPRF, a multiple induction form and an incomplete construction form are presented. Proofs are given to show that they are CFPRFs. From these forms we go further and get a class of functions named CFPRF~+, which includes CFPRF as its proper subclass. The relation between CFPRF~+ and CFRF is discussed. A formal specification language called LFC (Language For CFRF) is proposed, which supports the many-sorted recursive functions including CFRF, recursive functions defined on numbers and recursive functions defined on words, and which offers several function definition means based on the forms mentioned above. LFC is also a general-purpose functional programming language. Besides having properties possessed by other functional programming languages (e.g. referential transparency, conciseness, and sound mathematical properties), it is particularly suited to express algorithms for objects with complex structures. LFC uses context free language (CFL) as its data type. An expression which is of CFL type is an implicitly structured expression formed by using the general concatenation function, having strong expressiveness and flexibility. LFC is high-level and executable, and properties of its programs are provable. Because context free grammar can be obtained by machine learning method, and CFRF can be constructed by the assistance of machine using structural induction method, LFC is convenient for machine aided formal specification acquisition. The acquired specification can be used to do rapid prototyping, therefore it is checked. LFC is also related to specification bases, facilitating the interactivity of specification acquisition and checking. The possible implementation methods of LFC are studied, and a tree-oriented evaluation method is proposed according to the characteristics of CFRF, which is a general method suited for CFRFs defined in various forms. To realize the method, an expression representation which can represent the structure of expressions, and an intermediate representation of LFC based on this expression representation are devised. The undecidabilities of the equality, inclusion and intersection relations between two CFLs cause difficulties in type checking LFC programs. We present a practical type system for LFC, and offer the related algorithms. These make the representation conversion of expression possible. Based on the above work, a method is presented for translating LFC function definitions into the intermediate representation, which includes analyses of recursive parameters and definition forms of functions, parameter substitution, representation translation of patterns and expressions, transformation of function definitions from incomplete construction forms to complete construction forms, and pattern-matching translation. The implementation approaches of LFC intermediate representation are also discussed, and a rapid implementation method is presented, in which a Scheme interpreter is utilized and the translation from the intermediate representation to Scheme code is realized. In our work, CFL is used as the data type of a functional programming language for the first time, and the relevant issues such as expression type of a functional programming language for the first time, and the relevant issues such as expression representation and type system are studied, which can be references to related researches. According to the above studies, a LFC interpreter, and an experimental function construction and checking system FC (Function Constructor) which is one component of the specification acquisition and checking system SAQ, are developed. Some experiments are made to examine our research results.
语种: 中文
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6002
Appears in Collections:中科院软件所

Files in This Item:
File Name/ File Size Content Type Version Access License
LW002844.pdf(2527KB)----限制开放-- 联系获取全文

Recommended Citation:
陈海明. 基于上下文无关语言递归函数的规约语言研究[D]. 中国科学院软件研究所. 中国科学院软件研究所. 1999-01-01.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[陈海明]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[陈海明]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace