Event-B建模實際操作：控制橋上的汽車（二）

緊接上節。現在我們要繼續工作，做出初始模型的第一個精化。一個精化就是一個比初始模型更精確的模型。雖然它更精確，但也不應該與初始模型矛盾。這樣，我們就必須證明這個精化與初始模型的一致性。 First Refinement: Introducing the One-Way Bridge We are now going to proceed with a refinement of our initi

>>阅读原文<<