From: dl@g.g.oswego.edu (Doug Lea)
Newsgroups: comp.lang.c++
Subject: Re: Proposal: Preconditions and PostConditions in C++
Date: 15 Oct 92 12:58:59 GMT
	<1992Oct13.164331.29699@genghis.borland.com>
	<1992Oct13.194121.116854@Cookie.secapl.com>
Organization: SUNY Oswego


I haven't read this newsgroup for a while, but just caught some
discussion about our A++ work. I'll append excerpts from a
draft tech report that describes status and prospects. Comments
would be very welcome. (Sorry about the format; I just did
a light pass pulling out the latex formatting.)

---------------------------------

Conclusions about originally planned A++ tool...

We believe that it will not be feasible to build a tool with the
functionality described by Cline and Lea until:

  1) No additional major syntactic and semantic extensions 
        are made to the language, so that annotation
        syntax may be added without conflict.

  2) Common shallow representation formats, parsers and
        related tools are fully developed.

  3) Deeper semantic models become better understood.

  4) Unverifiable conformance to ``safe'' programming rules is
        mandated for users of the part of the tool that attempts to
        statically analyze constraints.  (These include lack of
        pointer arithmatic, and probably, use of garbage collection or
        other facilities to test pointer liveness.)


Items (1) and (2) are necessary even for the construction
of simpler tools that provide only translation, not static
analysis. The viability of the basic ideas for producing
shallow tools may be seen in the success of such strategies
for other OO languages including Eiffel.

... An exploration of alternative class-based approaches:

Even though the prospects of A++ as a tool remain unfullfilled, many
of its underlying goals are within ready reach.

In the realm of OO programming support, there are always two possible
plans of attack: To build a tool that operates outside of the
language, or to build a class library that ``extends'' the language to
the extent possible within class definition and usage rules.

We originally conceived of A++ as an extra-linguistic
framework. However, tool status is  not required in order to
support the definition of constraints that are directly expressible in
the language and written for purposes of run-time checking. A library
of classes can be devised that provide many of the same benefits.

The development advantages of this approach are obvious:

    * There is no need for parsing, representation formats, 
            or related tool infrastructure.
    * There are  many fewer language evolution issues. (Only
            those that would affect  any C++ library.)
    * The human factors surrounding the use of ``helpful classes''
          versus ``correctness tools'' may lead to greater acceptance
          by programmers.
    * Programmers may integrate use of support classes and
            mechanisms into their routine programming styles.

However, there are some drawbacks:

  * Full static analysis is precluded, or at least much more
        difficult. (It becomes possible only by analyzing
        the parsed, represented code maintained by other tools.)

  * Class-based constructs are sometimes more awkward to
        use than is a good annotation syntax. (Although in many
        common cases, people (surprisingly) find the reverse to be true.)

  * The key C++ constructs that make this approach possible
        are among the ones causing problems in Phase 1: Templates,
        Exceptions, and Run-Time type information are neither quite
        ``in'' nor ``out'' of the language, but instead are present
        with incomplete, varying support in current C++ compilers.
        (Thus many of the support classes described below have not yet
        been tested, and/or have only been tried via temporary
        work-araound strategies.)

... (Some examples:)

Invariants

Consider the simplest and perhaps most common use of annotations
in C++, the single-variable data invariant. For example (using A++)

class Date
{
  int month;
  int year;
  // ...
always: 1 <= month && month <= 12;
  //...  
}

There is a simple way for programmers to avoid defining this
invariant. Instead of using a constrained integer, the programmer
could have created a ` Month' class:

class Month
{
  int m;
always: 1 <= m && m <= 12;
  // define int operations like + on months
}

class Date
{
  Month month;
  int year;
  //...
};

These clearly have equivalent effect.
This maneuvre merely pushed the need for constraint maintenance down
one level, from ` Date' to ` Month'.  

This is arguably better C++ style. Whenever one class includes
a constrained version of another class or type as an attribute,
a programmer may either specify restrictions that hold only in
the new class, or create a special class embodying these restrictions.
The latter strategy is generally preferable:

  * Constraints become localized to their immediate targets.
  * The constrained classes may be reused in other contexts.
  * It minimizes per-class annotations and redundant specification
        of similar constraints across different classes.
  * The construction of many simply constrained classes may
        be automated by use of templates and/or macros.

The last point is pragmatically useful.  Automatic generation is
especially simple in the present (common) case of using built-in types
and unary constraints. Here, given the appropriate template library
classes, a programmer need only write:

int monthOK(int m) { return 0 <= m && m <= 12; }
typedef Month ConstrainedInt<monthOK>;

This general strategy extends to arbitrary constraints on arbitrary
numbers of built-in types. The basic reason they succeed is that
interfaces for built-ins are predetermined by the language. Creating
versions that maintain constraints amount simply to the writing of
templates that reproduce these interfaces, but intercept normal
operations with constraint checks in the appropriate ways.  Also, it
is possble to specifiy conversion rules from these types to their
corresponding builtins that maintain transparency for most programming
purposes (generally, in all contexts except those requiring pointers.)

The standard implementation of these classes is to arrange that
constraint violations occuring inside the generated class trigger
exceptions.  But it is also possible to provide mechanisms such that
programmers can avoid the overhead resulting from constraint checks.
There are several ways to implement this. The simplest is to
include code in the templates that references a preprocessor variable
that is normally defined as ` TRUE' but may be redefined to `
FALSE'. Thus the template code might read:

  ... if (CHECK && !monthOK(m)) throw ConstraintError; ...

A compiler may then remove the checks as dead code when
` CHECK' is ` FALSE'.

...

Also note that this level of invariants does not significantly
interact with subtyping logic for the clients of such classes.

...

Smart Wrapper Classes

The examples in the previous section all dealt with constrained
built-in types, and worked by duplicating known interfaces.
This technique cannot generally work for user-defined types.
However, equivalently useful effects may be had via ``smart
pointers''.

Smart pointers are classes that overload ` operator ->()'
and related operators to that the classes ``look'' like pointers.
Howver, upon dereference, they may perform any kind of
processing whatsoever (so long as they ultimately dereference
to the declared type.)

For example, suppose a programmer wished to declare a ` Parser'
class that used a ` Stack' that was constrained to never be full.
In A++, this might look like:


class Parser
{
  Stack* s;
always:  !s.full();
  //...
}


This effect may be obtained instead through:

int notFull(Stack* s) { return !s.full(); }

typedef notFullStack  ConstrainedPtr<Stack, notFull>;

class Parser
{
  notFullStack* s;
  //...
}

Constrained smart pointer classes share with constrained builtins the
minor problem in C++ of possessing occasionally detectable differences
from the classes they replace {edelson}. In partial compensation,
beyond the explicit constraint checking they perform, they also
provide protection against errors like performing pointer arithematic.

Contracts

The support classes in the previous sections do not address the need
for ``relational constraints'' or (data-oriented) contracts {helm}
among objects.  For example, (This is not a particularly good example
stylistically but is simple and general enough to illustrate issues.)

class BankAccount
{
  BankCustomer* customer;
  int customerID;
always: customerID == customer->id();
  //...
};


This kind of constraint is different than those above in that it
directly references two or more objects. It may be desirable to place
checks in either the ` BankAccount' class, the ` BankCustomer'
class, or perhaps both.

Moreover, in the majority of cases, it is more useful to programmers
if mechanisms are developed that actually perform propagation,
rather than check for its effects. Classes may be constructed that
ensure that a relational constraint continues to hold whenever 
any of the component attributes are updated.

This tactic preserves some of the goals of the A++ tool in removing
redundant checks when they cannot ever fail. Automatic propagation
causes these constraints to always hold, at least to the extent
specified by the programmer. They may not be implemented in the
fastest possible way -- manually defined updates performed only under
the minimum necessary situations will almost always outperfrom this.
But this strategy is likely to be much faster than exception-based
schemes or other interventions, and thus an acceptable ``canned''
solution to constraint maintenance.

Toward this end, one may devise prototypes of classes that are
similar to those for constrained built-ins, but take as (template)
arguments those messages to send whenever values are modified.

For example, the above class could be replaced with:

class BankAccount
{
  BankCustomer* customer;
  PropagatedInt<customer, customer::set_id> customerID;
};

(And perhaps similarly for the inverse case.)

The `PropagatedInt' class automatically sends the indicated
update message to the indicated target whenever the underlying
value has changed. (This is a very common set of protocols
in GUI programming, so should not be unfamilar to programmers.)

This example employed only equality relations over attributes of
built-in types. These are both most common and most amenable for
automated support.  We are also investigating the development of more
general schemes that deal with more arbitrary relations across objects
of arbitrary classes. However, there are intrinsic limits to this
approach. It leads ultimately to creation of a complete
constraint-propagation facility that is beyond the requirements of
everyday programming, and is inherently slow.

Method Annotations

The above techniques all apply at the level of  objects.  They
specify constraints that hold at all execution points and may 
never be broken throughout the lifetime of an object.  A++ and
similar systems also support annotations that apply only on a
per-method basis. These include:

  *[Postconditions] Assertions that hold at the exit point of a
        method if all preconditions are satisfied.

  *[Preconditions] Assertions that must hold on entry point of a
        method in order for postconditions to hold upon exit. (The
        relation between preconditions and postconditions is 
        implication.  If a precondition holds, so will the
        postcondition.)

  *[Public Invariants] Assertions that serve as both preconditions
        and postconditions for  all public methods of a class.
        These describe those properties that must hold both before and
        after each method. Unlike object invariants, these properties
        may be momentarily broken and then re-attained during the
        course of any method.


When these constructs are employed within a programming, rather than
tool context, they must be successfully integrated into other
mechanisms dealing with unexpected events. Thus, their use and support
must mesh with policies reflecting issues in the use of exceptions
that are otherwise unrelated to correctness-oriented annotations.
These may be roughly categorized as follows:


  *[Errors] Generally, the failure of any postcondition
    (even if expressed via a public invariant) indicates the presence
    of an error in the implementation of the  receiver of a
    message.  These should normally be handled through
    ``catastrophic'' exceptions in the same manner as object invariant
    failures.

  *[Notifications] Most often, the failure of any precondition
    indicates the presence of  client misbehavior of some sort.
    These should normally be handled through programmer-defined
    exceptions or similar strategies that communicate to clients or
    other entities that the desired effects were unattainable.  The
    main policy difference between this and the previous case is that
    normally, notifications are caught by clients or their proxies,
    while failures are normally caught by more general error handling
    facilities.

  *[Surprises] Certain postconditions may legitimately fail
    even though all preconditions clear and there are no
    implementation ``errors''. These generally occur when there is no
    available means to fully express the precondition. For example, a
    ` write' method may fail because a disk is full. This situation
    is uncheckable in most operating systems. Such methods are forced
    to employ ``try-and-see'' strategies, where they attempt an
    operation and then use either of the above modes to propagate
    failure. This strategy is recommended, for example, by
    {stroustrup-2} as the standard policy for dealing with 
    resource acquisition matters that have this property. It is also
    common when dealing with system services involving ``time-out''
    protocols.

... The interaction of support classes and design methodology:

Adoption of a standard good-programming practice assists in the
integration of different exception-based programming
tactics. An especially good candidate is a design methodology
based around the notion that.

    Whenever possible, code bodies are invoked (and their postconditions
    claimed to hold) only if their preconditions are met.

This rule is most notably present in Dijkstra's ``guarded command
language''. It is employed in a broader OO context in {dCLF.}
It is a complementary design convention to that used in most of
the above examples, in which methods are always allowed to
fire, but raise exceptions or patch constraints when necessary.
Combinations of these approaches are useful.

...

This leads to a number of simplifications in how programmers
may define and use constraints:

  * Preconditions are no longer treated as ``annotations'' but as
         guards that enable different code bodies to ``fire''
        depending on internal and external conditions.  In fact, the
        term ``precondition'' becomes misleading.  Methods may have
        several different guards that indicate disjoint sets of
        conditions and actions. 

  * Only the conditions associated with public invariants have any
        ``special'' status.  These may be required to hold before any
        other guards may even be evaluated.

  *  Every guard has an associated code body, even if it is
        simply a ` throw'. In fact, notification-based throws and
        normal returns are considered variants of the same notion of
        informing clients of the results of a message. (Of course,
        pragmatics and efficiency dictate that programmers should
        arrange to use normal return mechanisms for such purposes
        whenever reasonable.)

  *  Every code body may have an associated postcondition that may
        also generate a error-based exception. There need be only a
        single ` XError exception type per class ` X', to
        indicate implementation errors that are generally
        unknowable in nature.

  * Only those failures that may legitimately occur despite
        correct implementation and precondition clearance (i.e.,
        ``try-and-see'' failures) should be dealt with manually on a
        case-by-case basis by programmers. Of these, only those that
        should not result in ` XError' exceptions need actually be
        dealt with.  (Try-and-see failures have exactly the same
        conceptual status as implementation errors. They differ only
        in that these ``errors'' are known to be locally uncorrectable.)

...

How can a set of classes and utilities help programmers obtain the
benefits of guard-based method design and implementation?

Perhaps the best answer is to avoid the question, and move toward
design notations that require expression of methods in this form. We
are separately pursuing this strategy in a distributed OO context. 

However, to face it head on, a number of small classes, templates,
and macros are of immediate obvious value. These include

Precondition Templates
These are variants of ` assert' macros, including extensions of
those described in {gautron}. They allow simpler expression
of alternative flow of control based on
evaluated boolean guards.  Through usage conventions, these can be
made to properly follow the kinds of subtyping constraints enforced
in A++.

Exception Class Templates
Templates that guarantee some of the above properties of exception
classes, but allow per-class specialization and subclass specialization.
Similarly, classes using notification protocols, perhaps in
combination with exceptions, may be defined.

Delayed message handling
These include support classes for building  message queues.
This allows the development of classes in which methods do
not trigger  unless preconditions clear. (They are otherwise
queued). This tactic (common in distributed OO applications) allows
development of extremely safe classes, but is generally inapplicable
when clients must receive immediate responses. Because the nature
and handling of delayed messages varies significantly from class
to class, prospects for full automation appear somewhat limited,
but should be further explored.

...

Other C++ Safety Provisions
Some safety provisions and guards are untestable at run-time in C++.
The most famous examples surround liveness of pointers and references.
Among other things, it is impossible to determine whether a pointer is
bound to an object that has been ` delete'd.  Solutions cannot be had
via these kinds of support tools, but instead must rely on utilities
like garbage collection mechanisms. The search for general-purpose
garbage collection facilities is the subject of much current research
in the C++ community.

...
--
Doug Lea  dl@g.oswego.edu || dl@cat.syr.edu || (315)341-2688 || (315)443-1060
|| Computer Science Department, SUNY Oswego, Oswego, NY 13126 
|| Software Engineering Lab, NY CASE Center, Syracuse Univ., Syracuse NY 13244