We have demonstrated a strong connection between PVE and modular design of software in this section. We believe similar results can be established for most other issues that are essential for a ``well-engineered'' software product.
Metrics for PVE
How can the PVE be measured? Common metrics such as cyclomatic complexity and lines of code provide some indication of the PVE within a module. Module interaction can provide a measure of PVE across modules. However, for PVE to be an accurate predictor, metrics based on formal assertions such as pre- and post-conditions of procedures, loop invariants, and semantics of statements need to designed and developed.
Designing for lower PVE
It is possible to design software so that its PVE is minimized, and this is an important advantage of the PVE factor. For example, Ada components designed following the guidelines in [Hollingsworth 92] will require lower PVE than ones that are not. Alternatively, adherence to guidelines such as these may provide a useful PVE metric.
Finally, we emphasize again that PVE is independent of software correctness. PVE is a useful factor irrespective of whether verification is feasible. For a software engineer, it provides an objective that can be understood through formal training and can be followed. In the end, it is the thought (that verifiability is important) that counts!