澳門大學科技學院與聯合國大學國際軟件技術研究所將於2006年5月26日下午5時於澳門大學國際圖書館STDM演講廳聯合舉辦學術講座,特別邀請Tony Hoare教授主講“The Ideal of Program Correctness(程序正確性的理想)。此次講座為澳門大學廿五週年校慶傑出學者講座之一。

Tony Hoare 又名Charles Antony Richard Hoare,1980年獲計算機科學最高學術獎圖靈獎(Turing Award),是世界上最有影響力的計算機科學家之一。作為計算機科學教授,他長期在牛津大學工作。退休後受聘於微軟公司,現為微軟劍橋研究院高級研究員。他在計算機與理論的諸多方面做出了卓越貢獻:他早年發明的快速排序算法(Quicksort)是計算機最有名的一個算法;為了解決程序正確性問題,他提出了一種邏輯系統,後來被稱為Hoare邏輯,它是形式驗證方法的主要途徑之一;Tony Hoare又提出了通信順序進程CSP理論,在學術界產生了深遠的影響。2000年他獲得日本稻盛財團設立的國際大獎京都獎(尖端技術領域)。同年,英國女王伊麗莎白二世授予他爵士爵位,以表彰他對教育與計算機科學所做出的重大貢獻。上星期三在北京,中國科學院向他頒授“愛因斯坦講席教授證書和紀念獎牌。

軟件驗證為計算機科學領域的一個長期目標。“可驗證的編譯器”被認為是計算機學界本世紀的一個重大挑戰性項目。Tony Hoare教授目前正在組織這個國際性項目。他這次講座將圍繞程序正確性的理想模型程序驗證器展開敘述。針對挑戰性,該項目提出了近期要達到的具體目標以及完成這個目標要達到的具體要求。他還將介紹程序驗證器的理論系統、所需工具及部分實驗。

計算機科學界對Tony Hoare教授的學術成就並不陌生。從上世紀六、七十年代應用過他開發的高級程序設計語言:ALGOL60的資深軟件工程師到今天在課堂上練習他發明創造的Quicksort算法、Hoare邏輯及CSP理論的計算機科學系學生,都感受到大師學問的奇妙精湛。