In this section, we discuss one example that demonstrates the utility of the PVE rating. We use 3C terms in this discussion, where a concept means a specification, content means an implementation, and the context is the local environment in which a concept or content is explained [Latour 90, Sitaraman 92, Tracz 90]. Given a concept and a context, consider the following four possible contents:
Let us assume that all four contents are equal on the dimension of correctness. However, it is clear that content 1 is poorly engineered compared to content 2 (assuming that the chosen components and the layering used in content 2 are appropriate). Content 2 which uses a modular design without any specification is worse than content 3. ``Local certifiability'' [Weide 92] and hence ``reusability'' makes content 4 superior to content 3. We will return to this topic later.
PVE for monolithic content
Verification effort in this case is a function of both the number of statements and the kind of statements. Clearly an implementation involving several loops will require more effort to verify than the one that uses only if-then-else statements which is probably more difficult to verify than one that uses no control statements. PVE for two loops need not be the same either because a complex loop involving a more complex loop invariant is harder to verify than one that is less complex. In general, PVE is based on the semantics of the statements used in an implementation and the implementation. Gotos and uncontrolled use of pointers obviously increase the PVE.
PVE is also dependent on the specification for which the content is written. Here, we're only comparing contents for the same specification and therefore, we can say that PVE = f(Content 1). Alternatively, PVE can also be expressed as the effort to ``reverse engineer'' content 1 into the form of Content 4 (re-1-4) plus the PVE for Content 4.
The effective PVE for monolithic content 1: min (PVE(Content 1), re-1-4 + PVE(Content 4)).
PVE for content layered on 1C-components
When the sub-contents used in a content are not specified, then verification effort is not far less than what is required in the monolithic case. Verification here involves inline code expansion. This requires calls to subprograms, procedures, etc. to be replaced with the actual content (with proper substitutions for the calling context) during the verification process. This means we must verify approximately the same code we did for the monolithic implementation. In some sense, if understanding the bigger content involves direct understanding of each of its constituents then modularization is of relatively little use.
The effective PVE for content 2: min (PVE(inline_expanded_Content 2), re-2-4 + PVE(Content 4)).
It seems likely that re-2-4 will be smaller than re-1-4 because reverse engineering smaller modules may be inherently easier.
PVE for content layered on 2C-components
In this case, we assume that the sub-contents have formally-specified concepts. The concept, however, contains only calling information (such as the pre-conditions for procedures) etc., but does not include module-level context. In this case, specification-based proof rules can be used for operation calls instead of the ones requiring inline code expansion; The sub-contents themselves need to verified locally and independently to meet their specifications. This may not be possible if the context does not contain sufficient information.
The effective PVE for content 3: min (PVE(Content 3), re-3-4 + PVE(Content 4)).
PVE for content layered on 3C-components
In this case, each sub-component can be locally certified to be correct [Weide 92]. Verification effort = PVE(Content 4) for this case is the lowest. This verification effort will be even lower if each sub-component is a reusable component and its verifiability effort is amortized over its many uses. (Without local certifiability, reusability is impractical.)
The effective PVE for content 4 = f(Content 4, rf) where rf is the reuse factor.
Though we have concentrated on the 3C model in this discussion, the Constraints module introduced in [Sitaraman 92] ``contents layered using 4C components,'' can be useful in including performance issues in the PVE factor.