Formal Methods for Component Software: The Refinement Calculus Perspective

We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. Nondeterminism in specifications permits …