Radl→Apla程序生成系统及其可靠性研究

《Radl→Apla程序生成系统及其可靠性研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、摘要随着信息技术的发展，计算机软件已经应用到了生活的各个方面，软件的可靠性也越来越受到关注，人们不仅对安全性至关重要软件系统提出了高可靠的要求，而且对于普通的应用软件也希望尽可能不出错。众所周知，传统的软件测试手段并不能满足人们对高质量软件的要求，而形式化开发方法因其具有严格的理论基础，可以用于开发正确、高效的程序。本文实现了由Radl算法程序到Apla程序的映射过程，其中使用Radl语言来描述由PAR方法开发的算法程序，选用Apla语言作为映射的目标语言。为了使这种映射过程具有高可靠性，本文采用形式化的描述方法分别从词法、语法和语义三个层次精确地定义Radl语言，

2、保证了Radl语言描述的程序正确地反映了推导所得算法的逻辑思想；并且基于Radl语言属性文法，以Radl语法产生式作为最小映射单元，定义了Radl语言映射单元到Apla语言语义单元的语义等价映射规则；同时采用形式化推导方法，根据Radl语言词法、语法、语义及Radl算法程序到Apla程序的映射规则的定义，推导出Radl语言词法分析、语法分析和语义分析实现的代表性算法。基于形式化推导的语法制导翻译的方法，将Radl算法程序按映射规则映射成Apla程序，保证了所实现的系统是在相关理论的指导下进行的，并且高可靠的实现了相关理论的要求。本文主要做了如下几方面工作，其中某些方

3、面具有一定的创新性：1．分别形式化的定义Radl语言的词法、语法和语义。2．以Radl语法产生式为单元，系统定义由Radl生成Apla程序的生成规则。3．采用形式化推导方法得到生成系统的核心代表性算法。关键词：PAR方法；Radl；程序生成；算法推导AbstractWiththedevelopmentofinformationtechnology,computersoftwarehasbeenappliedtoeveryaspect，andpeoplepaymoreandmoreattentiontothereliabilityofsoftware．Usersnot

4、onlyrequirehighreliabilityforsafety-criticalsoftwaresystem，butalsohopethatgeneralapplicationsoflrwarealsodoesn’tgowrong．Asweallknow,traditionalsoftwaretestingcannotbeabletosatisfypeople’Sdemandsforhigh-qualitysoRware．Onthecontrary,foritsrigoroustheory,formaldevelopmentmethodologyCandev

5、elopcorrectandefficientprocedures．ThispaperhasachievedthemappingofRadlalgorithmtoAplaprogram．ThepaperadoptsRadltodescribethealgorithmdevelopedbyPARmethod，andchoosesAplaasthetargetlanguageofmapping．Inordertoletthemappingprocesshavehighreliability,thispaperusesformalmethodtodefinethesour

6、celanguage······Radllanguagepreciselyinthreelevelsrespectively,whicharemorphology,syntaxandsemantics．ItassuresthatthealgorithmdescribedbyRadlreflectsaccuratelythelogicalthinkingofalgorithmderived．BasedonattributegrammarofRadllanguageandlettingRadlsyntaxproductionrulesastheminimumunitof

7、mapping，theequalmappingruleisdefined．Atthesametime，accordingtothemorphology,syntax，semanticsofRadlandthedefinitionofmappingrulesofRadltoApla，formalderivationmethodisadoptedtoderivethecorealgorithmoflexicalanalysis，grammaranalysisandsemanticanalysisofRadl．Underthemethodbasedonformalde