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

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

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

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