據科技日報報道，科學出版社近日出版了北大信息學院軟件理論教研室原主任、教授袁崇義的英文專著《OESPA：Semantic Oriented Theory of Programming》一書，在此書中，作者提出了面向語義的新編程理論——OESPA，為目前世界上唯一能做語義計算的編程理論。
計算機軟件
目前計算機應用已經深入到社會的各個角落，幾乎每個行業都往信息化轉型，很多崗位都已經離不開計算機。但是軟件是由人開發出來的，目前的軟件開發過程，必須經過測試員測試才能上線發佈使用。而測試員測試軟件，僅能發現錯誤，卻不能判斷無錯，可能會存在很多遺漏的未發現的bug，可能是輕微的，也可能致命的，都或多或少會影響軟件的使用及體驗。科學家們幾十年如一日地嘗試用數學和邏輯推理來定義和證明程序的正確，但測試依然是目前軟件開發必不可少的過程。
軟件測試
袁崇義介紹，OESPA 包括計算模型（編程語言）OE，語義謂詞 SP 和語義公理A。傳統的程序語言以社會學中的形式語言學為理論基礎，沒有考慮語義形式化的需求。OE 則是二合一的，定義 OE 的公式既是編譯程序需要的形式語法，又是定義語義公理的形式基礎。
“傳統數學中的謂詞只能描述程序單獨一個狀態的性質，而程序語義是程序初態和終態之間的關係。SP 聯繫初態和終態，能準確描述程序語義。語義謂詞 SP 從語義公理A演變而成。從 SP 推出的 SP 公式和 SP 演算，用於程序的語義計算和語義綜合，可藉助符號處理工具完成程序正確性證明。”袁崇義表示，一旦開發出相應的符號處理系統，測試就不再是編程必要的一步。SP 公式和 SP 演算還適用於描述程序規範和規範分析。
所以，以後測試員要失業了？
你怎麼看？
分享到:
閱讀更多 026倉庫 的文章
