形式规约语言LFC的实现和应用研究
|
摘要
LFC是以上下文无关语言上的递归函数(CFRF)理论为基础的形式规约语言，能较好地支持形式规约的获取和检验。同时LFC也是一种函数式语言，具有良好的数学基础、引用透明、无副作用、模式匹配等特点。本文工作主要是研究形式规约语言LFC的实现和应用，另外还包括一个上下文无关语言句子枚举算法。
在理论方面，提出了一个上下文无关语言句子枚举算法。该枚举算法首先计算上下文无关语言的最小序句子和最大序句子，然后从最小序句子开始按照一定的顺序扫描字符串，直至扫描到最大序句子为止，对被扫描的字符串进行判断取舍。在扫描的过程中采用削减和前瞻策略，很大程度上减少了被扫描字符串的个数，可以取得较好的时空性能。
在实现方面，提出了编译LFC的技术路线，设计一个目标抽象机，通过程序翻译的方法将源程序翻译为目标抽象机代码，然后再将抽象机代码转换为汇编代码，汇编装配连接执行。翻译过程中，将进行参数一致化、模式分量翻译、模式的编码、公共子表达式的提取、模式匹配树的构造及优化工作。由于LFC是一个有类型的语言，为其设计了一个类型系统，支持参数化多态，给出了类型检查算法，还讨论了类型系统实现中需要解决的问题。为实现编译目的，设计了一个目标抽象机HSECD机，详细讨论了HSECD机的结构、指令、工作原理和指令优化方法。提出从HSECD机指令生成汇编指令的方法，包括如何组织存储结构和宏扩展。此外，为上下文无关语言句子的分析树设计了一种简单表示形式，这种表示形式可以提高空间效率，并且易于实现。根据CFRF的特点，提出了后缀形式的计算方法，减少在函数计算中存在的动态语法分析，避免了不必要的求值计算，使效率得到提高。在此基础上，实现了LFC的编译器。
在应用方面，实现了一个用LFC编写的从XML DTD到XML Schema的转换工具，检验了LFC的能力。
Huang Wenji(Computer Software & Theory) Directed by Dong Yunmei
The 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.
在理论方面，提出了一个上下文无关语言句子枚举算法。该枚举算法首先计算上下文无关语言的最小序句子和最大序句子，然后从最小序句子开始按照一定的顺序扫描字符串，直至扫描到最大序句子为止，对被扫描的字符串进行判断取舍。在扫描的过程中采用削减和前瞻策略，很大程度上减少了被扫描字符串的个数，可以取得较好的时空性能。
在实现方面，提出了编译LFC的技术路线，设计一个目标抽象机，通过程序翻译的方法将源程序翻译为目标抽象机代码，然后再将抽象机代码转换为汇编代码，汇编装配连接执行。翻译过程中，将进行参数一致化、模式分量翻译、模式的编码、公共子表达式的提取、模式匹配树的构造及优化工作。由于LFC是一个有类型的语言，为其设计了一个类型系统，支持参数化多态，给出了类型检查算法，还讨论了类型系统实现中需要解决的问题。为实现编译目的，设计了一个目标抽象机HSECD机，详细讨论了HSECD机的结构、指令、工作原理和指令优化方法。提出从HSECD机指令生成汇编指令的方法，包括如何组织存储结构和宏扩展。此外，为上下文无关语言句子的分析树设计了一种简单表示形式，这种表示形式可以提高空间效率，并且易于实现。根据CFRF的特点，提出了后缀形式的计算方法，减少在函数计算中存在的动态语法分析，避免了不必要的求值计算，使效率得到提高。在此基础上，实现了LFC的编译器。
在应用方面，实现了一个用LFC编写的从XML DTD到XML Schema的转换工具，检验了LFC的能力。
Huang Wenji(Computer Software & Theory) Directed by Dong Yunmei
The 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.
引文
[1] 董韫美．规约获取与复用的MLIRF方法．中国计算机科学技术新发展(中国计算机学会第9次全国学术会议论文集)．西南师范大学出版社，1996
[2] 董韫美等．Collection of SAQ Report no．1-7．中国科学院软件研究所计算机科学重点实验室报告：ISCAS-LCS-95-09，1995
[3] 董韫美等．Collection of SAQ Report no．8-16．中国科学院软件研究所计算机科学重点实验室报告：ISCAS-LCS-96-1，1996
[4] Dong Yun-mei. Recursive functions of context free languages (Ⅰ). SCIENCE IN CHINA(Series F),2002,45(1):25～39
[5] Dong Yun-mei. Recursive functions of context free languages (Ⅱ). SCIENCE IN CHINA(Series F),2002,45(2):81～102
[6] 陈海明．基于上下文无关语言递归函数的规约语言研究．中国科学院软件研究所博士论文，1999
[7] M Mac, Airchinnigh. VDM--a formal method at work. Springer-Verlag, 1987.356～361
[8] J R Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 1996
[9] J M Spivey. Understanding Z: a specification language and its formal semantics. Cambridge Tracts in Theoretical Computer Science, 1988
[10] T Bolognesi, E Brinksma. Introduction to the ISO specification language LOTOS. Computer Network ISDN Systems, 1987, 14(1):25～59
[11] J V Guttag, J J Horning, J M Wing. Larch in five easy pieces. Technical Report, Digital Systems Research Center, Paolo Alto, 1985
[12] G Smith. A formal specification of signaling system no.7 telephone user part. In International Conference on Networks, Singapore, 1989
[13] T M Brookes, M Green, J S Fitzgerald, P G Larsen. A comparison of the conventional and formal design of a secure system component. Nordic Seminar on Dependable Computing Systems, Denmark, 1994
[14] B Durnota. Object-oriented formal specification for spatial representation: a terrain model and its channel network. Workshop On Spatial And Temporal Interaction: Representation And Reasoning, Singapore, 1994.113～131
[15] M P Ward, K H Bennett. Formal methods to aid the evolution of software. Journal of Software Engineering and Knowledge Engineering, 1995,5(1):25～47
[16] M Ward, F W Calliss, M Munro. The maintainer's assistant. In Proceedings of
Conference on Software Maintenance, Miami, 1989.307～315
[17] B Cheng, B Auernheimer. Applying formal methods and object-oriented analysis to existing flight software. In Proceedings Of 18th Annual NASA Software Engineering Workshop, 1993.274～282
[18] B Legard, F Peureux, M Utting. Automated boundary testing from Z to B. LNCS 2391, 2002.21～40
[19] R Fletcher, A S M Sajeev. A framework for testing object-oriented software using formal specification. Technical Reports TR95-15, Monash University, 1995
[20] Z Dang, R A Kemmerer. Using the ASTRAL model checker for cryptographic protocol analysis. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997
[21] A N Choudary, V Gehlot, B Narahari. Parallel real-time systems: formal specification. In Proceedings of the 4th International Conference on High Performance Computing, 1997
[22] D M Geman, D D Cowan, P Alencar. A formal specification language for hypermedia applications. In 1st International Workshop on Hypermedia Development, Pittsburgh, U.S.A., 1998
[23] C Meadow. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1992,1 (1):5～36
[24] R Groenboom, E Saaman, E Rotterdam, G R Lavalette. Formalizing anaesthesia: a case study in formal specification. LNCS 1051, 1996. 120～139
[25] P Hudak. Concept, evolution and application of functional programming languages. ACM Computing Surveys, 1989, 21 (3):359～411
[26] A J Field, P G Harrison. Functional programming. Addison-Wesley, 1988
[27] A Church. The calculi of lambda conversion. NJ:Princeton University Press, 1941
[28] P W MKoopman, M Van Eekelen, M J Plasmeijer. Operational machine specification in a functional programming language. Software Practice and Experience, 1995, 25(5):463～499
[29] R Douence, P Fradet. Towards a taxonomy of functional language implementations. In Proceedings of PLILP'95, 1995.27～44
[30] T Johnsson. Compiling lazy functional languages: an introduction. Ph.D thesis, Chalmers University of Technology, Sweden, 1997
[31] P Jones. The implementation of functional programs. London: Prentice Hall, 1987
[32] P Henderson. Functional programming: application and implementation. London: Prentice Hall, 1980
[33] P J Landin. The mechanical evaluation of expressions. Computer Journal, 1964,6(4):308～320
[34] W H Burge. Recursive programming techniques. Mass:Addison-Wesley Publishing Company, 1975
[35] D A Turner. An implementation of SASL. Technical Report 4, University of St.Andrews, 1975
[36] L Cardelli. The functional abstract machine. Technical report TR-107, AT&T Bell Laboratories, 1983
[37] G Cousineau, P L Curien, M Mauny. The categorical abstract machine. In Proceedings of Conference on Functional Programming Languages and Computer Architecture, France, 1985.50～64
[38] R D Lins, B O Lira. CMC:a novel way of compiling functional languages. University of Kent, UK, 1992
[39] 廖湖声．函数式语言编译实现技术的研究．软件学报，1995，增刊
[40] J Berstel, L Boasson. The set of minimal words of a context-free language is context-free. Journal of Computer and System Sciences, 1997, 55(3):477～488
[41] Domosi. Unusual algorithms for lexicographic enumeration. Technical Report 184, TUCS, 1998
[42] E Mkinen. On lexicographic enumeration of regular and context-free languages. Acta Cybernet, 1997, 13(1):55～61
[43] J Earley. An efficient context-free parsing algorithm. Comm. of ACM, 1970, 13(2): 94～102
[44] IEEE Standard 1178-1990. IEEE standard for the Scheme programming language. IEEE, 1991
[45] 陈海明．一类递归函数的编译实现．SAQ repon no．33．Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, 2000
[46] 陈海明，董韫美．上下文无关语言语法树的一种表示形式．计算机研究与发展，2000，37(10)：1179～1184
[47] R Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1978,17(3):348～375
[48] R Milner, M toftre, R Harper. The definition of stantdard of ML. the MIT Press, 1990
[49] C Strachey. Fundamental concepts in programming languages. Lecture notes for the International Summer School in Computer Programming, Copenhagen, 1967
[50] H B Curry, R Feys. Combinatory logic. Amsterdam: North-Holland,1958
[51] R Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society,1969,146(1):29～60
[52] L Cardelli. Basic polymorphic type checking. Science of Computer Programming, 1987,8(2):147～172
[53] S Jenkins, G T Leavens. Polymorphic type-checking in scheme.Computer Languages, 1996,22(4):215～223
[54] A J Kfoury, S M Pericas-Geertseny. Type inference for recursive definitions. 14th Symposium on Logic in Computer Science, Italy, 1999.119～159
[55] 郑红军，张乃孝．一种带约束的多态类型系统．计算机学报，1999，22(4)：343～350
[56] J Yang, G Michaelson, P Trinder. How do people check polymorphic types? In Twelfth Annual Meeting of the Psychology of Programming Interest Group Proceedings, Memoria, 2000.67～77
[57] J C Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1991, 1(3):245～285
[58] J H Siekmann. An introduction to unification theory. Formal techniques in artificial intelligence: A Sourcebook, Elsevier Science, 1990
[59] S R Kosaraju. Efficient tree pattern matching. 30th Annual Symposium on Foundation of Computer Science, 1989
[60] M Dubiner, Z Galil, E Magen. Faster tree pattern matching. Journal of the ACM, 1994, 41(2):205～213
[61] 万战勇．SAQ规约库管理系统的扩充、重新实现和一个应用．中国科学院软件研究所硕士学位论文，1997
[62] 陈自明．SAQ系统用于程序语言的转换器．中国科学院软件研究所硕士论文，1997
[63] H Chen. Statically typed XML processing by the LFC language. CIT, India, 2003.177～182
[64] T Bray, J Paoli, C M Sperberg-Macuqueen. Extensible Markup Language(XML) 1.0(W3C Recommendation). http://www.w3.org/TR/REC-xml, 2000
[65] W3c.XML Schema. http://www.w3.org/Schema, 2001
[66] Altova. XML SPY. http://www.altoval.com, 2004
[2] 董韫美等．Collection of SAQ Report no．1-7．中国科学院软件研究所计算机科学重点实验室报告：ISCAS-LCS-95-09，1995
[3] 董韫美等．Collection of SAQ Report no．8-16．中国科学院软件研究所计算机科学重点实验室报告：ISCAS-LCS-96-1，1996
[4] Dong Yun-mei. Recursive functions of context free languages (Ⅰ). SCIENCE IN CHINA(Series F),2002,45(1):25～39
[5] Dong Yun-mei. Recursive functions of context free languages (Ⅱ). SCIENCE IN CHINA(Series F),2002,45(2):81～102
[6] 陈海明．基于上下文无关语言递归函数的规约语言研究．中国科学院软件研究所博士论文，1999
[7] M Mac, Airchinnigh. VDM--a formal method at work. Springer-Verlag, 1987.356～361
[8] J R Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 1996
[9] J M Spivey. Understanding Z: a specification language and its formal semantics. Cambridge Tracts in Theoretical Computer Science, 1988
[10] T Bolognesi, E Brinksma. Introduction to the ISO specification language LOTOS. Computer Network ISDN Systems, 1987, 14(1):25～59
[11] J V Guttag, J J Horning, J M Wing. Larch in five easy pieces. Technical Report, Digital Systems Research Center, Paolo Alto, 1985
[12] G Smith. A formal specification of signaling system no.7 telephone user part. In International Conference on Networks, Singapore, 1989
[13] T M Brookes, M Green, J S Fitzgerald, P G Larsen. A comparison of the conventional and formal design of a secure system component. Nordic Seminar on Dependable Computing Systems, Denmark, 1994
[14] B Durnota. Object-oriented formal specification for spatial representation: a terrain model and its channel network. Workshop On Spatial And Temporal Interaction: Representation And Reasoning, Singapore, 1994.113～131
[15] M P Ward, K H Bennett. Formal methods to aid the evolution of software. Journal of Software Engineering and Knowledge Engineering, 1995,5(1):25～47
[16] M Ward, F W Calliss, M Munro. The maintainer's assistant. In Proceedings of
Conference on Software Maintenance, Miami, 1989.307～315
[17] B Cheng, B Auernheimer. Applying formal methods and object-oriented analysis to existing flight software. In Proceedings Of 18th Annual NASA Software Engineering Workshop, 1993.274～282
[18] B Legard, F Peureux, M Utting. Automated boundary testing from Z to B. LNCS 2391, 2002.21～40
[19] R Fletcher, A S M Sajeev. A framework for testing object-oriented software using formal specification. Technical Reports TR95-15, Monash University, 1995
[20] Z Dang, R A Kemmerer. Using the ASTRAL model checker for cryptographic protocol analysis. DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997
[21] A N Choudary, V Gehlot, B Narahari. Parallel real-time systems: formal specification. In Proceedings of the 4th International Conference on High Performance Computing, 1997
[22] D M Geman, D D Cowan, P Alencar. A formal specification language for hypermedia applications. In 1st International Workshop on Hypermedia Development, Pittsburgh, U.S.A., 1998
[23] C Meadow. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1992,1 (1):5～36
[24] R Groenboom, E Saaman, E Rotterdam, G R Lavalette. Formalizing anaesthesia: a case study in formal specification. LNCS 1051, 1996. 120～139
[25] P Hudak. Concept, evolution and application of functional programming languages. ACM Computing Surveys, 1989, 21 (3):359～411
[26] A J Field, P G Harrison. Functional programming. Addison-Wesley, 1988
[27] A Church. The calculi of lambda conversion. NJ:Princeton University Press, 1941
[28] P W MKoopman, M Van Eekelen, M J Plasmeijer. Operational machine specification in a functional programming language. Software Practice and Experience, 1995, 25(5):463～499
[29] R Douence, P Fradet. Towards a taxonomy of functional language implementations. In Proceedings of PLILP'95, 1995.27～44
[30] T Johnsson. Compiling lazy functional languages: an introduction. Ph.D thesis, Chalmers University of Technology, Sweden, 1997
[31] P Jones. The implementation of functional programs. London: Prentice Hall, 1987
[32] P Henderson. Functional programming: application and implementation. London: Prentice Hall, 1980
[33] P J Landin. The mechanical evaluation of expressions. Computer Journal, 1964,6(4):308～320
[34] W H Burge. Recursive programming techniques. Mass:Addison-Wesley Publishing Company, 1975
[35] D A Turner. An implementation of SASL. Technical Report 4, University of St.Andrews, 1975
[36] L Cardelli. The functional abstract machine. Technical report TR-107, AT&T Bell Laboratories, 1983
[37] G Cousineau, P L Curien, M Mauny. The categorical abstract machine. In Proceedings of Conference on Functional Programming Languages and Computer Architecture, France, 1985.50～64
[38] R D Lins, B O Lira. CMC:a novel way of compiling functional languages. University of Kent, UK, 1992
[39] 廖湖声．函数式语言编译实现技术的研究．软件学报，1995，增刊
[40] J Berstel, L Boasson. The set of minimal words of a context-free language is context-free. Journal of Computer and System Sciences, 1997, 55(3):477～488
[41] Domosi. Unusual algorithms for lexicographic enumeration. Technical Report 184, TUCS, 1998
[42] E Mkinen. On lexicographic enumeration of regular and context-free languages. Acta Cybernet, 1997, 13(1):55～61
[43] J Earley. An efficient context-free parsing algorithm. Comm. of ACM, 1970, 13(2): 94～102
[44] IEEE Standard 1178-1990. IEEE standard for the Scheme programming language. IEEE, 1991
[45] 陈海明．一类递归函数的编译实现．SAQ repon no．33．Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, 2000
[46] 陈海明，董韫美．上下文无关语言语法树的一种表示形式．计算机研究与发展，2000，37(10)：1179～1184
[47] R Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 1978,17(3):348～375
[48] R Milner, M toftre, R Harper. The definition of stantdard of ML. the MIT Press, 1990
[49] C Strachey. Fundamental concepts in programming languages. Lecture notes for the International Summer School in Computer Programming, Copenhagen, 1967
[50] H B Curry, R Feys. Combinatory logic. Amsterdam: North-Holland,1958
[51] R Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society,1969,146(1):29～60
[52] L Cardelli. Basic polymorphic type checking. Science of Computer Programming, 1987,8(2):147～172
[53] S Jenkins, G T Leavens. Polymorphic type-checking in scheme.Computer Languages, 1996,22(4):215～223
[54] A J Kfoury, S M Pericas-Geertseny. Type inference for recursive definitions. 14th Symposium on Logic in Computer Science, Italy, 1999.119～159
[55] 郑红军，张乃孝．一种带约束的多态类型系统．计算机学报，1999，22(4)：343～350
[56] J Yang, G Michaelson, P Trinder. How do people check polymorphic types? In Twelfth Annual Meeting of the Psychology of Programming Interest Group Proceedings, Memoria, 2000.67～77
[57] J C Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1991, 1(3):245～285
[58] J H Siekmann. An introduction to unification theory. Formal techniques in artificial intelligence: A Sourcebook, Elsevier Science, 1990
[59] S R Kosaraju. Efficient tree pattern matching. 30th Annual Symposium on Foundation of Computer Science, 1989
[60] M Dubiner, Z Galil, E Magen. Faster tree pattern matching. Journal of the ACM, 1994, 41(2):205～213
[61] 万战勇．SAQ规约库管理系统的扩充、重新实现和一个应用．中国科学院软件研究所硕士学位论文，1997
[62] 陈自明．SAQ系统用于程序语言的转换器．中国科学院软件研究所硕士论文，1997
[63] H Chen. Statically typed XML processing by the LFC language. CIT, India, 2003.177～182
[64] T Bray, J Paoli, C M Sperberg-Macuqueen. Extensible Markup Language(XML) 1.0(W3C Recommendation). http://www.w3.org/TR/REC-xml, 2000
[65] W3c.XML Schema. http://www.w3.org/Schema, 2001
[66] Altova. XML SPY. http://www.altoval.com, 2004