<STYLE>body{background:#EEEBEA none;padding:6px;}</STYLE>

<DIV class=wikidoc>Summary: Spec# Patterns<BR>Nearby: <A href="/Wiki/SpecSharp/HomePage/">HomePage</A><BR><BR>As with all programming languages/tools, there are a number of different philosphies when it comes to using Spec#. Similarly there is a lot of room for discussion and debate over the risks and rewards of different philosphies. It is hoped that the philosphies (or patterns using recent nomenclature) can be presented and discussed here with great civility and little venom.<BR><BR>
<H3>TrustNoOne </H3><BR>This approach counts on full run-time checking of all specifications, including preconditions, postconditions, and class invariants. Even if a high degree of certainty correctness can be determined by static analysis, the full suite of constraints are still checked at run-time "just in case".<BR><BR>
<H3>TrustButVerify </H3><BR>This approach leaves the checking of preconditions (<B>requires</B>) to the callee, rather than having the caller "precheck" the preconditions. While callers are not required to prevent precondition violations, they is no requirement that do not do any checking either. There is, however, an expectation that the caller will be made aware of precondition violations in a way that supports some sort of detailed notification of which precondition failed, and allows the caller a significant chance of graceful recovery. At a minimum preconditions are still checked ar tun-time, but there is some degree of flexibility in run-time checking of class invariants and postconditions.<BR><BR>
<H3>ObjectRepair </H3><BR>Class invariants do not prevent an object from being left in an invalid state. As such, robust software should be capable of at least examining an object that has become invalid. However, class invariants are an implicit precondition on methods, thus making it "impossible" to inspect an object that has become invalid.<BR><BR>
<H3>EmbeddedLinkage </H3><BR>Objects that are elements in any sort of topological layout require some mechanism of associating relationship information (parent, previous, next, left, right, ...) for each element. However, embedding these linkage references in the object element itself is guaranteed to result in intermediate steps that violate linkage constraints, particularly when modifying linkages. This can be circumvented by making the linkage fields "not owned" by the element, and therefore not part of the element state. But at what cost?<BR><BR>
<H3>SpecificationVsTestDrivenDevelopment </H3><BR>Once a specification (precondition, postcondition, class invariant, ...) has been defined, is there any need for seperate test code? Given the built-in error detection of specifications, does further "test driven development" provide any benefits or is it purely redundant?<BR><BR>
<H3>SpecificationWeight </H3><BR>Some "high level" specifications can be extremely expensive to verify. For example, an ordered collection postcondition on an "Add" method that ensures that the entire collection is still properly ordered. Similarly the same ordered collection may have a class invariant that it is always entirely properly ordered. This could result in the entire collection being checked three times for proper ordering per each Add operation.<BR><BR>
<H3>TrainingWheels </H3><BR>This philosphy views constraints as useful during design and development, but unnecessary in the released product. Therefore, a "Release" build removes all constraint checking.<BR><BR>
<H3>PedanticParanoia </H3><BR>This philosphy results in adding constraints to the nth degree. For example, rather than simply ensuring that an element added to a stack (FIFO semantics) is indeed on the top of the stack, an extra postcondition is added that verifies that all previous elements are still in the stack in exactly the same order as before. While this level of testing is obviously appropriate, the <A href="/Wiki/SpecSharp/PedanticParanoia/">PedanticParanoia</A> approach aims for testing of these higher level semantics via constraints rather than through separate test programs.<BR>
<DIV class="filler spacer"></DIV></DIV>