形式规约语言LFC的实现和应用研究

【作者】 黄文集；

【导师】 董韫美；

【作者基本信息】 中国科学院研究生院（软件研究所） ， 计算机软件与理论， 2004， 博士

【摘要】 LFC是以上下文无关语言上的递归函数(CFRF)理论为基础的形式规约语言，能较好地支持形式规约的获取和检验。同时LFC也是一种函数式语言，具有良好的数学基础、引用透明、无副作用、模式匹配等特点。本文工作主要是研究形式规约语言LFC的实现和应用，另外还包括一个上下文无关语言句子枚举算法。 在理论方面，提出了一个上下文无关语言句子枚举算法。该枚举算法首先计算上下文无关语言的最小序句子和最大序句子，然后从最小序句子开始按照一定的顺序扫描字符串，直至扫描到最大序句子为止，对被扫描的字符串进行判断取舍。在扫描的过程中采用削减和前瞻策略，很大程度上减少了被扫描字符串的个数，可以取得较好的时空性能。 在实现方面，提出了编译LFC的技术路线，设计一个目标抽象机，通过程序翻译的方法将源程序翻译为目标抽象机代码，然后再将抽象机代码转换为汇编代码，汇编装配连接执行。翻译过程中，将进行参数一致化、模式分量翻译、模式的编码、公共子表达式的提取、模式匹配树的构造及优化工作。由于LFC是一个有类型的语言，为其设计了一个类型系统，支持参数化多态，给出了类型检查算法，还讨论了类型系统实现中需要解决的问题。为实现编译目的，设计了一个目标抽象机HSECD机，详细讨论了HSECD机的结构、指令、工作原理和指令优化方法。提出从HSECD机指令生成汇编指令的方法，包括如何组织存储结构和宏扩展。此外，为上下文无关语言句子的分析树设计了一种简单表示形式，这种表示形式可以提高空间效率，并且易于实现。根据CFRF的特点，提出了后缀形式的计算方法，减少在函数计算中存在的动态语法分析，避免了不必要的求值计算，使效率得到提高。在此基础上，实现了LFC的编译器。 在应用方面，实现了一个用LFC编写的从XML DTD到XML Schema的转换工具，检验了LFC的能力。更多还原

【Abstract】 Huang Wenji(Computer Software & Theory) Directed by Dong YunmeiThe implementation and application of formal specification language LFC are studied in this thesis. LFC is a formal specification language based on recursive functions defined on context free languages (CFRF) and supports the acquisition and validation of formal specification very well. LFC is yet another functional programming language which has many characteristics, such as good mathematics basis, reference transparency, no side effect, pattern matching, etc.In theory, an algorithm of enumerating sentences of CFG is presented. First, the minimal and maximal sentences of CFG are calculated. Then the character strings are scanned one by one from the minimal sentence in certain order till the maximal sentence. The scanned character strings are printed or skipped according to a rule. In the process, reducing and look-ahead strategies are adopted to reduce the number of the scanned character strings. So good time and space efficiency can be achieved.In implementation, the technique solution of compiling LFC is presented. The solution is that we design a target machine, and translate the source codes into the target machine codes by program translation, then generate the assembly codes from the target machine codes, assemble and link the assembly codes into exe file, at last execute the exe file to get the result of program. Renaming parameters, translating pattern, generating code of pattern, extracting common sub expression, constructing and optimizing pattern-matching tree, are finished during program translation. For compilation, we design a target abstract machine-HSECD machine and discuss the structure, instruction, principle and optimization of HSECD machine in detail. The method of generating assembly codes from HSECD instructions including arranging store structure and macro expansion is put forward. Moreover, we present an intermediate representation for parsing tree of CFL sentence that can be easily implemented and needs less space occupancy. According to the characteristic of CFRF, we develop the calculation method of postfix form that can reduce calling CFL sentence parsing and redundant evaluation to improve the efficiency. From these, a compiler is constructed.In application, we finish a converter of XML DTD to XML Schema in LFC that proves the application power of LFC.更多还原