計算機應用已深入到人類社會每一個角落，新軟體必須通過測試才能投入使用。測試仍然是軟體開發必不可少的步驟。測試只能發現錯誤，不能判斷是否無錯。潛在的錯誤隨時可能影響大眾生活。
專家們幾十年如一日用數學描述和邏輯推理來定義和證明程序正確，迄今未能取得成功。
今年，科學出版社出版了北京大學教授袁崇義的英文專著《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可以用於傳統語言程序的語義形式化處理。
來源：新華網