1、該文主要研究的對(duì)象是Oz 語(yǔ)言的約束的π-演算語(yǔ)義,類和對(duì)象的π-演算語(yǔ)義.借助帶多態(tài)和子類型關(guān)系的π-演算這一中間語(yǔ)言來(lái)作為我們研究Oz語(yǔ)言的形式化工具,該文主要討論了Oz語(yǔ)言的邏輯部分和面向?qū)ο蟛糠?我們的研究?jī)?nèi)容主要有:1.在該文中,我們采用類型變量和動(dòng)態(tài)調(diào)度的方式來(lái)表示Oz語(yǔ)言的數(shù)據(jù),而不是Oz語(yǔ)言所采用的指針表示方法,其目的就是為了提高Oz語(yǔ)言系統(tǒng)的效率.從而為我們下一步構(gòu)造帶類型的Oz虛擬機(jī)以及進(jìn)一步地?cái)U(kuò)充Oz語(yǔ)言的用類型來(lái)

2、指導(dǎo)的自動(dòng)垃圾回收功能提供了基礎(chǔ).2.我們用多態(tài)的π-演算解釋了γ-演算:Oz語(yǔ)言的核演算.我們翻譯的獨(dú)到之處在于:將引用作為多態(tài)的單元來(lái)處理,而單元的通道被用來(lái)與環(huán)境通信,在解釋a=b時(shí),系統(tǒng)明確地表示運(yùn)行時(shí)錯(cuò).對(duì)于多態(tài)類型一直存在著兩種不同方式的解釋:其一采用明確的方式,其二采用隱含的方式.我們采用了多態(tài)類型的顯示解釋方式,在多態(tài)類型的Barbed等價(jià)關(guān)系上給出了我們所作變換正確性的形式化證明.3.最后用類型的異步π-演算給出了一種

3、Oz語(yǔ)言的面向?qū)ο蟛糠值念?對(duì)象,繼承,方法應(yīng)用在順序情況下的形式化描述.在我們所見(jiàn)到的文獻(xiàn)中,很少涉及到用π-演算來(lái)刻劃基子類的面向?qū)ο蟪绦虻念惖睦^承特性.借助將對(duì)象類型分為接口類型和實(shí)現(xiàn)類型的思想,用類型的異步π-演算給出了類的繼承特性的形式化描述,因此我們的工作更進(jìn)一步地表明了π-演算可以作為一種中間語(yǔ)言來(lái)解釋基于類的面向?qū)ο筇匦?上述結(jié)果也具有重要的實(shí)踐意義,將早期的帶類型和子類型關(guān)系的π-演算的理論工作應(yīng)用于實(shí)踐,尤其是我們用