rCOS的操作語(yǔ)義及其在程序分析中的應(yīng)用.pdf

1、rCOS是A Refinement Calculus for Object Systems（對(duì)象系統(tǒng)的精化演算）的簡(jiǎn)稱。它以統(tǒng)一程序設(shè)計(jì)理論(Unifying Theories of Programming)[3]為基礎(chǔ)，是一種面向?qū)ο蟮拿枋稣Z(yǔ)言，定義了一種用于描述面向?qū)ο蟪绦蛟O(shè)計(jì)結(jié)構(gòu)的形式規(guī)范。rCOS具有非常中富的語(yǔ)言特征，包括予類(subtypes)、引用類型(reference type)、可見性(visibility)、繼承(

2、inheritance)、多態(tài)(polymorphism)、動(dòng)態(tài)綁定(dynamic binding)等。本文采用形式化的方法給出了rCOS的一種結(jié)構(gòu)化操作語(yǔ)義。對(duì)于一段rCOS程序，按照操作語(yǔ)義給出的變遷規(guī)則模擬執(zhí)行就能動(dòng)態(tài)的產(chǎn)生對(duì)象圖，而另一方面靜態(tài)分析程序段的類聲明部分就能得到對(duì)應(yīng)的類圖。對(duì)象圖和類圖構(gòu)成了rCOS程序的抽象模型。
　　 文中給出的操作語(yǔ)義一方面能動(dòng)態(tài)地構(gòu)建了對(duì)象圖，同時(shí)又能捕獲對(duì)象之間的關(guān)系。這樣有助于幫

3、助理解程序的行為，使得在程序分析方面起到了一定的作用，尤其在當(dāng)前軟件工程領(lǐng)域有著廣泛應(yīng)用的設(shè)計(jì)模式的識(shí)別上。文中將設(shè)計(jì)模式的性質(zhì)定義為兩類：通用屬性和用戶相關(guān)屬性。
　　 為了能描述對(duì)象圖或者類圖上對(duì)象與對(duì)象或者類與類之間的關(guān)系，我們定義了一種關(guān)系演算，將類之間的關(guān)系分為繼承和包含，對(duì)象之間的關(guān)系分為創(chuàng)建、調(diào)用和引用。文中選取抽象工廠模式、觀察者模式、組成模式等為例，說(shuō)明該關(guān)系演算能刻畫設(shè)計(jì)模式性質(zhì)。最后，本文給出一種通用的檢查