Ensuring Consistency between Designs, Documentation, Formal Specifications, and Implementations

Software engineering experts and textbooks insist that all of the artifacts related to a system, (e.g., its design, documentation, and implementation), must be kept in-sync. Unfortunately, in the real world, it is a very rare case that any two of these are kept consistent, let alone all three. In general, as an implementation changes, its source code documentation, like that of Javadoc, is only occasionally updated at some later date. Unsurprisingly, most design documents, like those written in UML, are created as a read-only medium—they reflect what the designers thought they were building at one point in the past, but have little to do with the actual running system. Even those using formal methods make this mistake, sometimes updating an implementation and forgetting to make some subtle change to a related specification. The critical problem inherent in this approach is that abstraction levels, while theoretically inter-dependent, are actually completely independent in semantics and from the point of view of the tools in pervasive use. Entities in different layers have no formal relationship; at best, informal relations are maintained by ad hoc approaches like code markers, or code is generated once and never touched again. This paper presents a new approach to system design, documentation, implementation, specification, and verification that imposes a formal refinement relationship between abstraction levels that is invisible to the programmer and automatically maintained by an integrated set of tools. The new concept that enables this approach is called a semantic property, and their use is discussed in detail with a set of examples using the high-level specification language EBON, the detailed design and specification language JML, and the Java programming language as the implementation language.