科技日报记者 马爱平
计算机应用已经深入到人类社会的每一个角落，可新软件必须通过测试才能投入使用。测试只能发现错误，不能判断是否无错，潜在的错误可能影响我们的生活。科学家们几十年如一日尝试用数学描述和逻辑推理来定义和证明程序正确，测试仍然是软件开发必不可少的步骤。
日前，科学出版社出版了国内知名Petri网专家、北大信息学院软件理论教研室原主任、教授袁崇义的英文专著《OESPA: Semantic Oriented Theory of Programming》，书中提出了面向语义的新编程理论OESPA。
袁崇义介绍，OESPA包括计算模型（编程语言）OE，语义谓词SP 和语义公理A。传统的程序语言以社会学中的形式语言学为理论基础，没有考虑语义形式化的需求。OE则是二合一的，定义OE的公式既是编译程序需要的形式语法，又是定义语义公理的形式基础。
“传统数学中的谓词只能描述程序单独一个状态的性质，而程序语义是程序初态和终态之间的关系。SP联系初态和终态，能准确描述程序语义。SP从语义公理A演变而成。从SP推出的SP公式和SP演算，用于程序的语义计算和语义综合，可借助符号处理工具完成程序正确性证明。”袁崇义表示，一但开发出相应的符号处理系统，测试就不再是编程必要的一步。SP公式和SP演算还适用于描述程序规范和规范分析。
专家表示，OESPA的成功得益于建模方法论ARM.，ARM适用于几乎所有需要构建形式模型的应用。OESPA是目前唯一能做语义计算的编程理论。
实践证明，传统数学没有为程序语义的形式化处理准备必要的工具，正是在ARM的指引下OESPA取得了成功，填补了传统数学的这一空白。
同时，袁崇义尝试SP和A用于C语言指针的语义处理，提出了指针的语义公理，表明OESPA可以用于传统语言程序的语义形式化处理。
