计算机应用已深入到人类社会每一个角落,新软件必须通过测试才能投入使用。测试仍然是软件开发必不可少的步骤。测试只能发现错误,不能判断是否无错。潜在的错误随时可能影响大众生活。
专家们几十年如一日用数学描述和逻辑推理来定义和证明程序正确,迄今未能取得成功。
今年,科学出版社出版了北京大学教授袁崇义的英文专著《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可以用于传统语言程序的语义形式化处理。
免责声明:本网转载自其它媒体的文章,目的在于弘扬科技创新精神,传递更多科技创新信息,并不代表本网赞同其观点和对其真实性负责,在此我们谨向原作者和原媒体致以崇高敬意。如果您认为本站文章侵犯了您的版权,请与我们联系,我们将第一时间删除。