84 2006.07
GEORGE RETSECK 11 sa.ylib.com 85
86 2006.07 CHRIS CARTER Denver International Airport
Alloy的運作 Alloy能幫助軟體設計師尋找並修復設計上的瑕疵 因 設計 檔案系統負責把電腦裡的檔案歸進不同的資料夾 為它使用的語言可釐清程式結構 而自動化分析器可搜尋 並儲存在磁碟上 Alloy的重要任務是 釐清不同的操作 出大量系統執行的可能結果 找出 反例 並顯示為什 會對檔案結構產生什麼影響 以下便是設計師藉由Alloy 麼達不到預期的效果 模擬並檢查操作的範例 將資料夾 或稱 目錄 從檔 在下面的簡例當中 工程師利用Alloy評估檔案系統的 案結構的一處移到另一處 程式碼 結果 步驟一 定義物件 定義物件 關係圖 根目錄 設計師確認系統的物件 檔案 目錄 整個檔 包含關係 案系統 以及物件彼此之間的關係 Alloy的 模型為整個檔案系統 file system 定義了三 目錄群 個要素 檔案群 files 目錄群 dirs 以 及 包含 關係 contains 即每個目錄內包 含的檔案群及目錄群的對映關係 子目錄 檔案群 步驟二 模擬操作 檔案 檔案 搬移操作 接 著 設 計 師 模 擬 檔 案 系 統 的 搬 移 m o v e _dir 之前的檔案系統稱為fs 之後的則是 fs 這項操作牽涉到兩個目錄 一是被搬移 的目錄 d 一是搬移後的位置所在目錄to 接 下來的三行程式碼是三項限制 描述了所欲達 成的結果 首先 無論是被搬移的物件 或是 目錄d 物件的新位置 都是檔案系統內的目錄 第二 d 目錄 則是這項操作的重心 雖然目錄群和 d 原本的 目錄to 所有對映關係消失了 且增加了to和 d 之間的 對映 但新的 包含 關係仍和舊有的一模一 樣 第三 沒有其他任何更動 所有檔案 皆可達 步驟三 指定條件 接著設計師制定關鍵的條件 從根目錄可 以 到達 每個檔案和目錄 透過路徑 這在Alloy的模型中會記錄為 判定 稱為 狀態 1 move_ok 換句話說 搬移動作並不會讓檔 案或目錄無法從根目錄到達 藍圖 問題 目錄不能搬移到 自身底下 步驟四 尋找並修復瑕疵 新的限制 不容許錯誤的搬移 Alloy能產生所有可能的系統狀態 到達一定 的規模 接著執行check move_ok 檢查每個 狀態的 判定 即可模擬軟體運作時可能發 LUCY READING-IKKANDA 生的任何搬移 Alloy這時發現了 判定 的 評估所有狀態 狀態 2 狀態 3 反例 目錄可搬移到自己底下 這個動作會讓 狀態 4 目錄和根目錄失聯 成為 不可到達 的目 狀態 5 錄 為解決這個問題 設計師加上一條新限 制 禁止目錄搬移到自己及自己的子目錄下 sa.ylib.com 狀態 6 目錄 狀態 8 狀態 9 狀態10 狀態11 1 目錄 檔案 檔案 狀態12 狀態 7 科學人 87
88 2006.07 GREG RICHTER Blue Mountain Avionics
sa.ylib.com 89
COURTESY OF LOMA LINDA UNIVERSITY MEDICAL CENTER 90 2006.07
sa.ylib.com 91
1. Software s Chronic Crisis. W. Wayt Gibbs in Scientific American, September 1994. 2. Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer. Sarfraz Khurshid and Daniel Jackson in Proceedings of the 15th IEEE International Conference on Automated Software Engineering, Grenoble, France. IEEE, September 2000. 3. Automating First-Order Relational Logic. Daniel Jackson in Proceedings of the 8th ACM SIGSOFT International Symposium on Foundations of Software Engineering: Twenty-First Century Applications. ACM Press, 2000. 4. A Micromodularity Mechanism. Daniel Jackson, Ilya Shlyakhter and Manu Sridharan in Proceedings of the Joint 8th European Software Engineering Conference (ESEC) and 9th ACM SIGSOFT Symposium on the Foundations of Software Engineering. ACM Press, 2001. 5. Alloy: A Lightweight Object Modeling Notation. Daniel Jackson in ACM Transactions on Software Engineering and Methodology, Vol. 11, Issue 2, pages 256 290; April 2002. 6. Software Abstractions: Logic, Language, and Analysis. Daniel Jackson. MIT Press, 2006. http://people.csail.mit.edu/dnj/ 7. Alloy http://alloy.mit.edu EMILY HARRISON 92 2006.07