PostB: The Post-condition Extension onto the B-Method

In the traditional B-method, operations are designed only by pre-conditions and a series of substitutions, and it works well. However, with the appearance and development of the modeling by the integration of semi-formal methods (especially UML) and formal methods, the condition changes. Without the formal notations interrelated to the post-condition, B-method cannot be embedded into UML models conveniently and flexibly in order to exert all its powers to describe systems exactly. This conditions indeed limit the adoption of B, and it is really necessary to extend the correlative definitions and properties. Therefore, this paper proposes the PostB, the extension referred to the formal notations of the post-condition to the B method, as well as the extended set-theorem models and proof obligations referred to it.