消费日报网 > 时尚生活 > 科技

我学者提出面向语义计算编程理论

时间:2019-12-03 10:08:11 来源:科技日报

2日,记者从科学出版社获悉,该出版社日前出版了北大信息学院软件理论教研室原主任、教授袁崇义的英文专著《OESPA: Semantic Oriented Theory of Programming》,书中提出了面向语义的新编程理论OESPA,这是目前唯一能做语义计算的编程理论。

  袁崇义介绍,OESPA包括计算模型(编程语言)OE,语义谓词SP和语义公理A。传统的程序语言以社会学中的形式语言学为理论基础,没有考虑语义形式化的需求。OE则是二合一的,定义OE的公式既是编译程序需要的形式语法,又是定义语义公理的形式基础。

  “传统数学中的谓词只能描述程序单独一个状态的性质,而程序语义是程序初态和终态之间的关系。SP联系初态和终态,能准确描述程序语义。语义谓词SP从语义公理A演变而成。从SP推出的SP公式和SP演算,用于程序的语义计算和语义综合,可借助符号处理工具完成程序正确性证明。”袁崇义表示,一旦开发出相应的符号处理系统,测试就不再是编程必要的一步。SP公式和SP演算还适用于描述程序规范和规范分析。

  同时,袁崇义尝试SP和A用于C语言指针的语义处理,提出了指针的语义公理,表明OESPA可以用于传统语言程序的语义形式化处理。(记者马爱平)

消费日报网版权及免责声明:
1. 凡本网注明“来源:消费日报网” 的所有作品,版权均属于消费日报网。如转载,须注明“来源:消费日报网”。违反上述声明者,本网将追究其相关法律责任。
2. 凡本网注明 “来源:XXX(非消费日报网)” 的作品,均转载自其它媒体,转载目的在于传递更多信息,并不代表本网赞同其观点和对其真实性负责。
3. 任何单位或个人认为消费日报网的内容可能涉嫌侵犯其合法权益,应及时向消费日报网书面反馈,并提供相关证明材料和理由,本网站在收到上述文件并审核后,会采取相应措施。
4. 消费日报网对于任何包含、经由链接、下载或其它途径所获得的有关本网站的任何内容、信息或广告,不声明或保证其正确性或可靠性。用户自行承担使用本网站的风险。
5. 基于技术和不可预见的原因而导致的服务中断,或者因用户的非法操作而造成的损失,消费日报网不负责任。
6. 如因版权和其它问题需要同本网联系的,请在文章刊发后30日内进行。
7. 联系邮箱:xfrbw218@163.com  电话:010-67637706

标签:
编辑: 刘坤媛
相关新闻

放射损伤与数百万人有关,我们对它知道得还是太少

福岛核泄漏事故、切尔诺贝利核事故、原子弹爆炸……在国外,核辐射曾给许多人带来伤害;我国每年也有数百万人接受核医学诊断的低剂量辐射、放射治疗的高剂量辐射。核辐射的威胁使放射生物效应与损伤防护...

雷启云: 揪出潜伏在城市下的地震元凶

雷启云在进行测量工作受访者供图  爱国情奋斗者  对地震两个字,雷启云从小就不陌生。  地处我国南北地震带北段的宁夏,历史上曾发生过两次8级以上地震。其中发生在1920年的海原8.5级特大地震,...

21世纪初 那些科技史上的高光时刻

图为洞察号火星车 图片来源:NASA官网图为Crispr-Cas9精确切割DNA 图片来源:剑桥大学图为大型强子对撞机发现“上帝粒子”图片来源:CERN  那些年,你可能“错过了大雨、错过了爱情”,却错不过科技进...

5G来了,云游戏成赢家

5G商用,到底能为人们带来哪些新的应用?云游戏正是其中的一个答案。2019年,各路巨头“亮剑”云游戏。在海外,微软、谷歌和索尼等头部企业公开了各自的云游戏项目;在国内,各游戏厂商也陆续推出云游戏...

中国科考“重器”亮相南大洋宇航员海

  首航南极的中国“雪龙2”号极地科考破冰船15日继续在南大洋宇航员海开展综合科考。连日来,一些大洋科考“重器”亮相,助力中国第36次南极考察队获取理想的科考样品。  北京时间15日凌晨5时许,科考...

4万多年前狩猎岩画面世

据英国《自然》杂志12日公开的一篇考古学论文,科学家报告了一幅在印度尼西亚发现的洞穴艺术画作。这幅作品描绘了一些类人形象狩猎猪和水牛的画面,至少可追溯至4.39万年以前,是迄今已知的最早狩猎场...