科技日報北京12月2日電 （記者馬愛平）2日，記者從科學(xué)出版社獲悉，該出版社日前出版了北大信息學(xué)院軟件理論教研室原主任、教授袁崇義的英文專著《OESPA: Semantic Oriented Theory of Programming》，書中提出了面向語義的新編程理論OESPA，這是目前唯一能做語義計算的編程理論。
袁崇義介紹，OESPA包括計算模型（編程語言）OE，語義謂詞SP和語義公理A。傳統(tǒng)的程序語言以社會學(xué)中的形式語言學(xué)為理論基礎(chǔ)，沒有考慮語義形式化的需求。OE則是二合一的，定義OE的公式既是編譯程序需要的形式語法，又是定義語義公理的形式基礎(chǔ)。
“傳統(tǒng)數(shù)學(xué)中的謂詞只能描述程序單獨(dú)一個狀態(tài)的性質(zhì)，而程序語義是程序初態(tài)和終態(tài)之間的關(guān)系。SP聯(lián)系初態(tài)和終態(tài)，能準(zhǔn)確描述程序語義。語義謂詞SP從語義公理A演變而成。從SP推出的SP公式和SP演算，用于程序的語義計算和語義綜合，可借助符號處理工具完成程序正確性證明。”袁崇義表示，一旦開發(fā)出相應(yīng)的符號處理系統(tǒng)，測試就不再是編程必要的一步。SP公式和SP演算還適用于描述程序規(guī)范和規(guī)范分析。
同時，袁崇義嘗試SP和A用于C語言指針的語義處理，提出了指針的語義公理，表明OESPA可以用于傳統(tǒng)語言程序的語義形式化處理。
中國-博士人才網(wǎng)發(fā)布
聲明提示：凡本網(wǎng)注明“來源：XXX”的文/圖等稿件，本網(wǎng)轉(zhuǎn)載出于傳遞更多信息及方便產(chǎn)業(yè)探討之目的，并不意味著本站贊同其觀點(diǎn)或證實(shí)其內(nèi)容的真實(shí)性，文章內(nèi)容僅供參考。
