一種基于學分制排課系統的Z規格說明

摘要：運用形式化方法建模在軟件開發過程中可提高目標系統的正確性和可靠性，在此提出了一種利用Z語言進行語義分析的方法。該方法在序列圖Z規范的基礎上，用屬性集表示對象狀態，并將序列圖的上下文表示為Z形式約束，通過檢查上下文約束與對象狀態間的一致性對序列圖進行語義分析。在此以一個基于學分制的排課系統為例，使用面向對象的形式規格說明語言Z，描述了一個精確、完整的高校排課系統的形式化數學模型。過程顯示，該方法具有精確的描述性和很強的抽象性，能為軟件系統的開發和驗證提供科學的框架。

關鍵詞：形式化方法；規格說明；Z語言；排課系統

中圖分類號：TP311-34文獻標識碼：A文章編號：1004-373X(2012)12-0050-04