post-conditions, and invariants for modules, formal methods in detailed design
are most appropriate for verifying correctness when the interaction between
system components is predefined and well-understood. In a Service-Oriented
Architecture (SOA), [236] by contrast, the order and interactions of components