科技是第一生产力、人才是第一资源、创新是第一动力 加快建设科技强国,实现高水平科技自立自强
氢能科技 沙蓬绿色种养产业模式 联源科技 超联科技 园区 园区 园区 园区 园区

语义编程理论OESPA 助力计算机基础理论研究取得突破性成果

   2019-10-14 本站综合消息
60
核心提示:计算机应用已深入到人类社会每一个角落,新软件必须通过测试才能投入使用。测试仍然是软件开发必不可少的步

计算机应用已深入到人类社会每一个角落,新软件必须通过测试才能投入使用。测试仍然是软件开发必不可少的步骤。测试只能发现错误,不能判断是否无错。潜在的错误随时可能影响大众生活。

专家们几十年如一日用数学描述和逻辑推理来定义和证明程序正确,迄今未能取得成功。

今年,科学出版社出版了北京大学教授袁崇义的英文专著《OESPA: Semantic Oriented Theory of Programming》,提出一整套面向语义的编程理论OESPA。二十来年的努力终于取得突破性研究成果。

已经退休的袁崇义长期从事计算机基础理论的教学和科研,不断思考传统语义学存在的问题。在北京大学任教期间,袁崇义一直从事Petri网和形式语义方面的教学,同时做软件基础理论研究。

OESPA包括计算模型(编程语言)OE,语义谓词SP和语义公理A。OE是二合一的,定义OE的公式既是编译程序需要的形式语法,也是定义语义公理的形式基础。

SP联系初态和终态,能准确描述程序语义。从SP推出的SP公式和SP演算,用于程序的语义计算和语义综合,可借助符号处理工具完成程序正确性证明。一但开发出相应的符号处理系统,测试就不再是编程必要的一步。

OESPA的成功得益于建模方法论ARM,ARM适用于几乎所有需要构建形式模型的应用。实践证明,传统数学没有为程序语义的形式化处理准备必要的工具,正是在ARM的指引下OESPA取得了成功,填补传统数学的空白。

OESPA是目前唯一能做语义计算的编程理论。袁崇义说,“OESPA目前还只是理论,需要各界的大力支持才能走向实用。”袁崇义尝试将SP和A用于C语言指针的语义处理,成功提出指针语义公理,说明OESPA可以用于传统语言程序的语义形式化处理。


免责声明:本网转载自其它媒体的文章,目的在于弘扬科技创新精神,传递更多科技创新信息,并不代表本网赞同其观点和对其真实性负责,在此我们谨向原作者和原媒体致以崇高敬意。如果您认为本站文章侵犯了您的版权,请与我们联系,我们将第一时间删除。
 
 
更多>同类资讯
推荐图文
推荐资讯
点击排行
网站首页  |  关于我们  |  联系方式  |  使用说明  |  隐私政策  |  免责声明  |  网站地图  |   |  粤ICP备05102027号

粤公网安备 44040202001358号