Pre-post notation is questionable in effectively specifying operations of object-oriented systems

摘要

There is a growing tendency for people in the community of object-oriented methods to use pre- and post-conditions to write formal specifications for operations (methods) of classes. The motivation for trying to take advantage of well established formalism in precisely defining the functionality of operations is laudable, but unfortunately this exercise may be flawed because the use of pre- and post-conditions containing method calls (or similar) with side effects are likely to cause confusion in the interpretation of specifications. This paper analyzes, with comprehensible examples, why using pre-post notation is not effective to specify operations in objectoriented systems in general, discusses existing approaches to using pre-post notation for object-oriented systems, and offers some solutions to the problem.