计算机研究与发展
計算機研究與髮展
계산궤연구여발전
JOURNAL OF COMPUTER RESEARCH AND DEVELOPMENT
2014年
4期
856-864
,共9页
PAR方法%Radl算法%程序生成%算法推导%生成规则
PAR方法%Radl算法%程序生成%算法推導%生成規則
PAR방법%Radl산법%정서생성%산법추도%생성규칙
PAR method%Radl algorithms%program generation%algorithm derivation%generation rule
算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.
算法設計是一項創造性工作,傳統的設計與描述方法難以保證算法的正確性.在PAR方法中通過定義具有數學引用透明性的算法描述語言Radl,可實現對問題規約進行形式化推導得到用遞推關繫描述的算法.Radl算法的覈心就是遞推關繫組,從而易于進行形式化推導和證明.通過深入剖析Radl算法特性,揭示Radl算法與抽象順序程序Apla(abstract programming language)間本質關繫,定義基于Radl語法產生式的Apla程序生成規則,實現瞭Apla程序自動生成繫統,併對其可靠性進行繫統研究,著重形式化驗證瞭實現繫統的覈心算法.使用PAR方法開髮的算法是正確的,採用形式化證明的生成繫統具有可靠性保證,從而保證瞭算法從設計到實現的高可靠性,併通過實現自動化開髮工具提高瞭程序的開髮效率.
산법설계시일항창조성공작,전통적설계여묘술방법난이보증산법적정학성.재PAR방법중통과정의구유수학인용투명성적산법묘술어언Radl,가실현대문제규약진행형식화추도득도용체추관계묘술적산법.Radl산법적핵심취시체추관계조,종이역우진행형식화추도화증명.통과심입부석Radl산법특성,게시Radl산법여추상순서정서Apla(abstract programming language)간본질관계,정의기우Radl어법산생식적Apla정서생성규칙,실현료Apla정서자동생성계통,병대기가고성진행계통연구,착중형식화험증료실현계통적핵심산법.사용PAR방법개발적산법시정학적,채용형식화증명적생성계통구유가고성보증,종이보증료산법종설계도실현적고가고성,병통과실현자동화개발공구제고료정서적개발효솔.
