美国二战经典电影语义编程理论OESPA 助力计算机基础理论研究取得突破性成果

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

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

　　今年，科学出版社出版了北京大学教授袁崇义的英文专著《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可以用于传统语言程序的语义形式化处理。