2日，記者從科學出版社獲悉，該出版社日前出版了北大信息學院軟件理論教研室原主任、教授袁崇義的英文專著《OESPA: Semantic Oriented Theory of Programming》，書中提出了面向語義的新編程理論OESPA，這是目前唯一能做語義計算的編程理論。

　　袁崇義介紹，OESPA包括計算模型（編程語言）OE，語義謂詞SP和語義公理A。傳統(tǒng)的程序語言以社會學中的形式語言學為理論基礎，沒有考慮語義形式化的需求。OE則是二合一的，定義OE的公式既是編譯程序需要的形式語法，又是定義語義公理的形式基礎。

　　“傳統(tǒng)數學中的謂詞只能描述程序單獨一個狀態(tài)的性質，而程序語義是程序初態(tài)和終態(tài)之間的關系。SP聯(lián)系初態(tài)和終態(tài)，能準確描述程序語義。語義謂詞SP從語義公理A演變而成。從SP推出的SP公式和SP演算，用于程序的語義計算和語義綜合，可借助符號處理工具完成程序正確性證明?！痹缌x表示，一旦開發(fā)出相應的符號處理系統(tǒng)，測試就不再是編程必要的一步。SP公式和SP演算還適用于描述程序規(guī)范和規(guī)范分析。

　　同時，袁崇義嘗試SP和A用于C語言指針的語義處理，提出了指針的語義公理，表明OESPA可以用于傳統(tǒng)語言程序的語義形式化處理。

責編/李雪敏