Formal Specification Language Lfc Is To Achieve And Applied Research

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.