又一位圖靈獎得主去世了，他是受人尊敬的時序邏輯領域大師艾米爾? 伯努利（Amir Pnueli）。今年11月2日，這位1996年度圖靈獎得主因腦出血去世，享年68歲，只剩那些熠熠生輝的科技成就留給后人。

　　艾米爾? 伯努利于1941年出生于以色列的Nahalal，在以色列理工學院取得數學學士學位，1967年在魏茨曼學院以一篇關于海洋潮汐計算的畢業論文取得應用數學博士學位。而后伯努利留校任教。

　　在計算機出現后的最初幾十年里，計算機實質上是一個巨大的計算器，數字被錄入，計算結果被輸出。直到20世紀70年代，科學家們才意識到需要正確地驗證這些計算結果。隨著電腦變得更強大，軟件更先進，多任務和變化的數據核查變得更加困難。因此，程序員不得不考慮到時間推移下系統的行為。在這個契機下，時序邏輯被引入計算科學，這是計算科學發展歷史的重要轉折點。

　　時序邏輯也叫時態邏輯（temporal logic），是計算機科學里一個很專業很重要的領域。時序邏輯被用來描述為表現和推理關于時間限定的命題的規則和符號化的任何系統，主要用于形式驗證。20世紀60年代Arthur Prior提出介入的基于模態邏輯的特殊的時間邏輯系統，這一理論后來被艾米爾?伯努利等邏輯學家進一步發展。

　　后來，Pnueli在斯坦福大學和IBM Waston研究中心從事博士后的研究工作，從這時開始，他將工作研究方向轉移到計算機科學領域。1973年，他創辦了特拉維夫大學計算機科學系，并擔任第一任院長。1977年，Pnueli開創性地把時態邏輯引入計算機科學，他的時態邏輯是非經典邏輯中的一種，研究如何處理含有時間信息的事件的命題和謂詞。現在通常稱為時序邏輯的計算機系統，就出現在這一年，Pnueli在子編程語言與系統驗證方面做出的杰出貢獻具有里程碑意義。

　　“Pnueli實現了這一邏輯，這是計算機科學的完美契合”，賴斯大學計算工程的摩西教授如是說。1996年度圖靈獎頒獎典禮上，該獎項的題詞評價Pnueli 1977年的論文“引發了對系統的動態行為推理的基本模式轉變”。這個很杰出的技術誕生后即在軟件工程界引起轟動，掀起了軟件工程中的一場革命，目前已成為開發反應式系統和并發式系統時進行規格說明和驗證的工具，在芯片、硬件的設計上已經廣泛運用。

　　1981年，Pnueli回到魏茲曼成為計算機科學系的教授。1999年，Pnueli加入美國紐約大學計算機科學系并出任教授一職。此外，和國外絕大多數教授一樣，Pnueli并不拘泥于純學術的研究和教學。Pnueli成立了幾家軟件公司，1971年成立Mini-Systems，1984年成立AdCad。他還和朋友一起在美國馬薩諸塞州創辦了另一家公司：iLogixInc，Pnueli 擔任iLogixInc公司的首席科學家。

　　Pnueli為人謙遜隨和，與中國的淵源甚深。他和2008年去世的我國著名邏輯和軟件學家唐稚松是至交，二人均是時態邏輯方面是業界領跑人。唐稚松教授提出了世界上第一個可執行時序邏輯語言XYZ/E。如果說Pnueli獲1996年圖靈獎的最大貢獻，是因開創性地將時序邏輯引入計算科學，那么唐稚松則是第一次將這種時序邏輯形式化理論與最新軟件技術結合起來，應用該語言將狀態轉換的控制機制引入到邏輯系統之中的人。Pnueli赴美接受圖靈獎前夕，在寫給唐稚松的信中說：“我完全相信，由于使時態邏輯成為具有‘深遠影響’的理念，你應該分享這一榮譽（指圖靈獎）中一個很有意義的部分。”

　　除了圖靈獎，Pnueli還曾獲得獎項無數，其中就包括以色列獎，這是以色列給出美國國家科學院外籍院士的成員的最高榮譽。

（本文來自《程序員》雜志0912期）