計(jì)算機(jī)軟件專(zhuān)家。1943年8月生于上海市。1965年畢業(yè)于復(fù)旦大學(xué)數(shù)學(xué)系。2005年當(dāng)選為中國(guó)科學(xué)院院士。
1980年起，從事程序設(shè)計(jì)理論及其應(yīng)用研究。1986年和C.A.R.Hoare提出了“程序分解算子”，并將規(guī)范語(yǔ)言與程序語(yǔ)言看成是同一類(lèi)數(shù)學(xué)對(duì)象。接著又提出了采用“關(guān)系代數(shù)”作為程序和軟件規(guī)范的統(tǒng)一數(shù)學(xué)模型，使得關(guān)系代數(shù)可用來(lái)描寫(xiě)程序的分解和組合過(guò)程，直接支持軟件的開(kāi)發(fā)。在數(shù)據(jù)精化方面，給出了處理非確定性程序語(yǔ)言數(shù)據(jù)精化的完備方法。1995年，在總結(jié)了多類(lèi)程序語(yǔ)言語(yǔ)義理論和方法的基礎(chǔ)上，與C.A.R.Hoare提出了程序設(shè)計(jì)統(tǒng)一理論和連接各類(lèi)程序理論的數(shù)學(xué)法則。還提出了用形式化的界面理論溝通幾種程序語(yǔ)言，以及非確定性數(shù)據(jù)流的數(shù)學(xué)模型及代數(shù)定律。近年來(lái)，研究的軟硬件協(xié)同設(shè)計(jì)系統(tǒng)，為減少系統(tǒng)芯片設(shè)計(jì)時(shí)間和降低成本提供了有益的方法。
