計(jì)算機(jī)應(yīng)用已深入到人類社會(huì)每一個(gè)角落，新軟件必須通過(guò)測(cè)試才能投入使用。測(cè)試仍然是軟件開發(fā)必不可少的步驟。測(cè)試只能發(fā)現(xiàn)錯(cuò)誤，不能判斷是否無(wú)錯(cuò)。潛在的錯(cuò)誤隨時(shí)可能影響大眾生活。

專家們幾十年如一日用數(shù)學(xué)描述和邏輯推理來(lái)定義和證明程序正確，迄今未能取得成功。

今年，科學(xué)出版社出版了北京大學(xué)教授袁崇義的英文專著《OESPA: Semantic Oriented Theory of Programming》，提出一整套面向語(yǔ)義的編程理論OESPA。二十來(lái)年的努力終于取得突破性研究成果。

已經(jīng)退休的袁崇義長(zhǎng)期從事計(jì)算機(jī)基礎(chǔ)理論的教學(xué)和科研，不斷思考傳統(tǒng)語(yǔ)義學(xué)存在的問(wèn)題。在北京大學(xué)任教期間，袁崇義一直從事Petri網(wǎng)和形式語(yǔ)義方面的教學(xué)，同時(shí)做軟件基礎(chǔ)理論研究。

OESPA包括計(jì)算模型（編程語(yǔ)言）OE，語(yǔ)義謂詞SP和語(yǔ)義公理A。OE是二合一的，定義OE的公式既是編譯程序需要的形式語(yǔ)法，也是定義語(yǔ)義公理的形式基礎(chǔ)。

SP聯(lián)系初態(tài)和終態(tài)，能準(zhǔn)確描述程序語(yǔ)義。從SP推出的SP公式和SP演算，用于程序的語(yǔ)義計(jì)算和語(yǔ)義綜合，可借助符號(hào)處理工具完成程序正確性證明。一但開發(fā)出相應(yīng)的符號(hào)處理系統(tǒng)，測(cè)試就不再是編程必要的一步。

OESPA的成功得益于建模方法論ARM，ARM適用于幾乎所有需要構(gòu)建形式模型的應(yīng)用。實(shí)踐證明，傳統(tǒng)數(shù)學(xué)沒(méi)有為程序語(yǔ)義的形式化處理準(zhǔn)備必要的工具，正是在ARM的指引下OESPA取得了成功，填補(bǔ)傳統(tǒng)數(shù)學(xué)的空白。

OESPA是目前唯一能做語(yǔ)義計(jì)算的編程理論。袁崇義說(shuō)，“OESPA目前還只是理論，需要各界的大力支持才能走向?qū)嵱谩！痹缌x嘗試將SP和A用于C語(yǔ)言指針的語(yǔ)義處理，成功提出指針語(yǔ)義公理，說(shuō)明OESPA可以用于傳統(tǒng)語(yǔ)言程序的語(yǔ)義形式化處理。

免責(zé)聲明：本網(wǎng)轉(zhuǎn)載自其它媒體的文章，目的在于弘揚(yáng)科技創(chuàng)新精神，傳遞更多科技創(chuàng)新信息，并不代表本網(wǎng)贊同其觀點(diǎn)和對(duì)其真實(shí)性負(fù)責(zé)，在此我們謹(jǐn)向原作者和原媒體致以崇高敬意。如果您認(rèn)為本站文章侵犯了您的版權(quán)，請(qǐng)與我們聯(lián)系，我們將第一時(shí)間刪除。