Introducing Dynamic Constraints in B

In B, the expression of dynamic constraints is notoriously missing. In this paper, we make various proposals for introducing them. They all express, in di erent complementary ways, how a system is allowed to evolve. Such descriptions are independent of the proposed evolutions of the system, which are de ned, as usual, by means of a number of operations. Some proof obligations are thus proposed in order to reconcile the two points of view. We have been very careful to ensure that these proposals are compatible with re nement. They are illustrated by several little examples, and a larger one. In a series of small appendices, we also give some theoretical foundations to our approach. In writing this paper, we have been heavily in uenced by the pioneering works of Z. Manna and A. Pnueli 11 , L. Lamport 10 , R. Back 5 and M. Butler 6 .

• Type: Conference
• Year: 1998
• Where: B
• Authors: Jean-Raymond Abrial, Louis Mussat
• Keywords: B 1998, Dynamic Constraints, Erent Complementary Ways, Software Engineering, Various Proposals