這本實用的教科書適用於形式化方法的入門課程或高級課程。本書以B形式化方法的一個擴展Event-B作為工具，展示了一種完成系統建模和設計的數學方法。
簡-埃蒙德·阿布瑞爾（Jean-Raymond Abrial）是國際著名電腦科學家，曾任蘇黎世聯邦理工學院客座教授，他基於精化的思想提出了一種系統化的方法，教讀者如何逐步構造出所期望的模型，並通過嚴格的證明完成對所構造模型做系統化的推理。
本書將介紹如何根據實際需要去構造各種程式，以及如何更為普遍地構造各種離散系統的模型。
本書提供了大量的示例，這些示例源自電腦系統開發的各個領域，包括順序程式、併發程式和電子線路等。
本書還包含了大量具有不同難度的練習和開發專案。書中的每個例子都用Rodin平臺工具集證明過。
本書適合作為高等院校電腦、軟體工程、網路工程、資訊安全等專業高年級本科生、研究生的教材，也可供相關領域的研究人員和技術人員參考。
簡-埃蒙德·阿布瑞爾（Jean-Raymond Abrial）是國際著名電腦科學家，曾任蘇黎世聯邦理工學院客座教授，他基於精化的思想提出了一種系統化的方法，教讀者如何逐步構造出所期望的模型，並通過嚴格的證明完成對所構造模型做系統化的推理。
本書將介紹如何根據實際需要去構造各種程式，以及如何更為普遍地構造各種離散系統的模型。
本書提供了大量的示例，這些示例源自電腦系統開發的各個領域，包括順序程式、併發程式和電子線路等。
本書還包含了大量具有不同難度的練習和開發專案。書中的每個例子都用Rodin平臺工具集證明過。
本書適合作為高等院校電腦、軟體工程、網路工程、資訊安全等專業高年級本科生、研究生的教材，也可供相關領域的研究人員和技術人員參考。