本文的標題是因為七月份科學人，刊出一篇關於軟體驗證的文章，軟體，別再出錯了！(因中文網站並沒有此篇內文，所以放上英文版文章"Dependable Software by Design")，主要是談到因為軟體越來越龐大，透過事先針對設計作檢核，可以減少之後軟體測試的錯誤和軟體開發成本。以物件導向開發來說，就是在OOA階段就針對UML來分析，降低軟體出錯、開發成本或避免造成重大意外。因此目前這方面大多應用在需高度安全的安全關鍵系統(Safety-Critical Systems)，如航空器、自動控制、醫療設備等等。
但此文作者，Daniel Jackson發展Alloy，使用另一種的狀態檢核方式，有別於之前談論到的Model Checking，叫做Model Finder，基礎為First Order Logic，跟Model Checker的Temporal Logic是不一樣，而作者聲稱比Model Checker更能應付複雜的軟體設計和狀態。而軟體為何不能像其他工程，如土木、機械工程，那樣針對每個元件檢測後，組合便不需再測試？原因在於軟體是離散的，不像其他工程是連續(符合物理性質)，因為每個Component皆獨立，且組合後變化成級數膨脹，而片段執行無誤，不代表整體是可運作的。
相同地，Alloy也必須給定一些Constraints，使其找出軟體設計上的Counterexamples(反例)，證明其缺陷。而規格語言是以Z Formal language為基礎。文中並列出目前各種Formal language(正規語言)的資料。
而之前研究是比較類似USE，使用OCL來表示限制式(Constraints)。
題外話，今年的IBM開發者大會將於7/25~26舉行，期待跟Dr. Ivar Jacobson合照。去年的IBM開發者大會心得。
