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