Version 1.3 of ais/ai-00288.txt
!standard 11.5 (00) 02-03-08 AI95-00288/01
!standard 11.4.1 (10)
!class amendment 02-02-05
!status work item 02-02-05
!status received 02-02-05
!priority Medium
!difficulty Medium
!subject Pre/Postconditions and Invariants
!summary
To augment the basic "assert" pragma capability proposed in AI-00286,
we propose pragmas for specifying pre/post conditions for subprograms,
and invariants for packages and types.
The semantics for these pragmas are defined in terms of the
Assertion_Error exception used by the Assert pragma and the
Assertion_Policy configuration pragma.
!problem
A number of programming paradigms include the heavy use of
pre/post conditions on subprograms and/or the use of invariants
associated with types or modules (i.e. packages).
Having a basic standardized "Assert" pragma supports this
approach to some degree, but generally requires that the
Assert pragmas actually be inserted inside the bodies of
the associated code. It would be much more appropriate if
these pre/post conditions and invariants appeared on the
specification of the subprograms, types, and packages rather
than buried in the body, as it really represents part
of the contract. In particular, one wants any implementation
of a given package spec to conform to all of the pre/post conditions
and invariants specified, in the same way one wants any implementation
of a package to conform to the constraints of the parameter and result
subtypes of the visible subprograms of the package.
Effectively, pre/post conditions and invariants may be considered
as generalized, user-definable constraints. They have the same power
to define more accurately the "contract" between the user and
implementor of a package, and to thereby catch errors in usage
or implementation earlier in the development cycle. They also can
provide valuable documentation of the intended semantics of an abstraction.
!proposal
Preconditions and Postconditions:
The pragmas Precondition, Classwide_Precondition, Postcondition,
and Classwide_Postcondition have the following form:
pragma Precondition(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Precondition(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Postcondition(subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
pragma Classwide_Postcondition(dispatching_subprogram_local_name,
boolean_expression [, [Message =>] string_expression]);
The (dispatching_)subprogram_name must name the immediately preceding
subprogram. For Classwide_Precondition and Classwide_Postcondition,
the subprogram must be a dispatching subprogram.
The boolean expression is defined within the context of the
subprogram specification so that the formal parameter names are
directly visible.
For a postcondition on a function, the attribute "Result" is defined
on the subprogram name, yielding the value returned by the function.
For a postcondition on a procedure, the attribute "Incoming"
is defined on each of the IN OUT elementary
formal parameters, yielding the value of the formal parameter
at the beginning of the execution of the procedure.
If a Classwide_Precondition or Classwide_Postcondition pragma is specified
for a primitive subprogram, then it also applies to all overridings
of the primitive. By contrast, Precondition/Postcondition
pragmas may be applied to non-primitive subprograms, and are not inherited.
For a Classwide_Precondition or Classwide_Postcondition, if a formal
parameter name corresponding to a controlling operand of the subprogram
appears in the boolean expression, it is view converted to the associated
class-wide type, implying that dispatching is performed if calls on primitive
functions occur in the expression. All other formal parameter names
appearing within the boolean expression of a precondition or postcondition
pragma have the type specified in the subprogram's parameter profile.
If the assertion policy in effect at the point of a precondition
pragma is "Check," then upon a call on the specified subprogram, after
evaluating the actual parameters and making the parameter associations,
the check associated with the precondition pragma is performed.
This consists of the evaluation of the boolean expression,
and if False, a raise of the Ada.Assertions.Assertion_Error exception, with
the specified Message if provided. It is not specified whether
any check for elaboration of the subprogram body is performed
before or after the precondition check.
If multiple precondition pragmas apply to the same subprogram (through
inheritance of Classwide_Preconditions), then only if all of the boolean
expressions evaluate to False, is Assertion_Error raised; an
implementation-defined message is associated with the exception occurrence
in this case. If any one of them evaluates to True, the subprogram
call proceeds normally. The order in which multiple precondition pragmas are
checked is not specified, and if one of them evaluates to True, it is
not specified whether the others are checked.
If the assertion policy in effect at the point of a postcondition
pragma is "Check," then upon successful return from a call on the specified
subprogram (as opposed to a return due to the propagation of an exception),
and prior to copying back any by-copy [IN] OUT parameters, the check
associated with the postcondition pragma is performed.
This consists of evaluating the boolean expression, and if
false, raising Ada.Assertions.Assertion_Error, with
the specified Message, if any. It is not specified whether the
exception, if any, is raised at the point of the return statement or
after leaving the subprogram. (I.e. it is not specified whether the exception
can be handled within the subprogram.)
If multiple postcondition checks apply to the same subprogram, then
Assertion_Error is raised if any of them evaluates to False;
the message provided corresponds to one of the failing checks.
The order of performing the checks is not specified, and if one of them
evaluates to False, it is not specified whether the others are checked.
If more than one evaluates to False, it is not specified which
message is provided with the exception occurrence. It is not specified
whether any constraint checks associated with copying back [IN] OUT
parameters are performed before or after the postcondition checks.
For a dispatching call or a call via an access-to-subprogram, the
precondition/postconditions that apply to the call are determined by
the subprogram actually invoked. Note that for a dispatching call, if there
is a Classwide_Precondition that applies to the subprogram named
in the call, then the rules for checking preconditions ensure that so
long as this Classwide_Precondition is satisfied, the overall precondition
check will succeed (because if any precondition evaluates to True, the
call proceeds normally).
Invariants
The pragmas Package_Invariant, Type_Invariant, and Classwide_Type_Invariant
have the following form:
pragma Package_Invariant(package_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Type_Invariant(first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
pragma Classwide_Type_Invariant(tagged_first_subtype_local_name,
boolean_function_name [, [Message =>] string_expression]);
The package_local_name for Package_Invariant must denote the immediately
enclosing program unit, which must be a package. The boolean_function_name
for Package_Invariant must denote a parameterless function declared
within the specified package that has a Standard.Boolean result.
The first_subtype_local_name for Type_Invariant must denote a first
subtype declared in the immediately enclosing region, which must be
a package. The boolean_function_name for Type_Invariant must denote
a function with one parameter of the type denoted by the
first_subtype_local_name, and a Standard.Boolean result.
The tagged_first_subtype_local_name for Classwide_Type_Invariant must
denote a tagged first subtype declared in the immediately enclosing
region, which must be a package. The boolean_function_name for
Classwide_Type_Invariant must denote a dispatching function with one
parameter of the type denoted by the tagged_first_subtype_local_name,
and a Standard.Boolean result.
If the assertion policy at the point of an invariant pragma is
"Check," then the associated check is performed at the following
places:
* For a Package_Invariant pragma, upon return
from a call on any procedure defined within the declarative
region of the package that is visible outside the package,
a call is performed on the specified parameterless function;
also, immediately after completing elaboration of the package.
* For a Type_Invariant pragma, upon return from a call
on any procedure that
- has one or more [IN] OUT parameters of the specified type,
- is defined within the immediate scope of the type, and
- is visible outside the immediate scope of the type,
one call is performed on the specified boolean function for each such
[IN] OUT parameter. Similarly, after evaluation of a function call or
type converstion that returns the specified type, a call is performed
on the specified boolean function passing the result. Finally, after
default initialization of an object of the type, a call is performed
on the specified boolean function passing the default-initialized object.
* For a Classwide_Type_Invariant pragma, upon return from a call
on any procedure that
- has one or more [IN] OUT parameters of a type within the
derivation class of the specified type,
- is defined within the immediate scope of the type, and
- is visible outside the immediate scope of the type,
one call is performed on the specified boolean dispatching function
for each such [IN] OUT parameter. The parameter is view-converted
to the class-wide type prior to the call, ensuring that the call is
a dispatching call. Similarly, after evaluation of a function call or
type conversion that returns a type within the derivation class, a
dispatching call is performed on the specified boolean function passing
the result. Finally, after default initialization of an object of a
type within the derivation class, a dispatching call is performed on
the specified boolean function passing the default-initialized object.
If any of these calls return False, Ada.Assertions.Assertion_Error is
raised, with the specified Message if any.
The invariant checks are performed prior to copying back
any by-copy [IN] OUT parameters. However, it is not specified
whether any constraint checks associated with the copying back are
performed before or after the invariant checks. If there are any
postconditions associated with the procedure, it is not specified
whether these checks are performed before, after, or interleaved with
the invariant checks.
Assertion Policy
If the assertion policy at the point of a pre/postcondition or invariant
pragma is "Check" then the semantics are as described above. If the assertion
If the assertion policy at the point of the pragma is
"Ignore" then the pragma has no effect. If the assertion
policy at the point of the pragma is "Assume_True" then if the check
associated with the pragma would have failed, execution is erroneous.
If the assertion policy at the point of the pragma is
"Evaluate_And_Assume_True" then the evaluations necessary to do the
check are performed, but if the check fails, execution is erroneous.
!wording
!discussion
Pre/Postcondition Pragmas
The precondition and postcondition pragmas provide a basic capability
for defining the "contract" of a subprogram. Implementation of the
corresponding checks is tied to the assertion policy in effect
at the point of the pragma (rather than at the call or the body),
to ensure that the checks may be inserted either
at the point of the call or inside the subprogram body, and both
the caller and the callee "know" whether the check will be
performed (which might affect optimization).
We provide a separate "Classwide_" version of the pragmas to distinguish
between conditions that apply to a particular version of a dispatching
operation from those that apply to all overridings of the operation.
This distinction is missing in Eiffel, and represents a weakness (in
our view) of their model. The "Classwide_" version necessarily must be
less specific, i.e. less "tight," and hence cannot catch as many bugs
by itself as the combination of an inherited condition and a condition
specific to a particular body.
A possible implementation model for the pre/postcondition checks is as follows.
Existing calls on Proc or Func are replaced with calls on "Proc_with_check"
or "Func_with_check" if the assertion policy is "Check" at the point of the
pragmas. The "_with_check" subprograms are defined as follows:
procedure Proc_with_check(
...; Elementary_Inout_Param1 : in out Inout_Type1; ...) is
--
begin
--
if not <precondition_bool_expr1>
and then not <precondition_bool_expr2>
and then not ...
then
raise Ada.Assertions.Assertion_Error;
--
end if;
declare
--
Elementary_Inout_Param1'Incoming : constant Inout_Type1 :=
Elementary_Inout_Param1;
... --
begin
--
Proc(..., Elementary_Inout_Param1, ...);
--
if not <postcondition_bool_expr> then
raise Ada.Assertions.Assertion_Error;
--
end if;
... --
end;
end Proc_with_check;
function Func_with_check(...) return Result_Type is
--
begin
--
if not <precondition_bool_expr1>
and then not <precondition_bool_expr2>
and then not ...
then
raise Ada.Assertions.Assertion_Error;
--
end if;
declare
--
--
Func'Result: Result_Type renames Func(...);
begin
--
if not <postcondition_bool_expr> then
raise Ada.Assertions.Assertion_Error;
--
end if;
... --
--
return Func'Result;
end;
end Func_with_check;
Note we don't specify exactly where the precondition checks occur relative
to elaboration checks so these checks may be done "outside" or "inside"
the subprogram as is most convenient. Similarly, we don't specify whether
the postcondition checks are performed at the point of the return statement,
or at the end of the call, to provide implementation flexibility.
This means that in some implementations Assertion_Error could be caught inside
the subprogram. This does not seem to be a serious concern, and the
implementation flexibility seems valuable.
However, we do require that dynamically bound calls, i.e. calls via
an access-to-subprogram dereference or a dispatching call, have the
applicable pre/postconditions checked. This implies that in most
situations, the pre/postcondition checks will need to be implemented by
adding code "inside" the subprogram, or by having two separate
subprograms (as above), one which is used by dynamically bound
calls which includes the check, and one which is used when
the checks are performed by the caller.
To do the best job of optimizing precondition checks, one would
generally want to expand them at the point of the call. On the
other hand, postcondition checks are probably most optimizable when
done inside the subprogram. This would imply that under heavy
optimization, it might be useful to have a separate version for
dynamically bound calls that performs the precondition checks "inside,"
while statically bound calls would perform the check at the
point of call, and then call the version that bypasses the precondition
check if the checks succeed. This is similar to an approach that
some compilers use for access-before-elaboration checking.
Having postcondition checks inside seems preferable in any case.
We don't provide a pre/postcondition pragma for access-to-subprogram types.
That might be useful in some cases. However, the pre/postcondition
would (presumably) only apply on calls through a value of the type,
which means additional implementation complexities, in that the
checking code could not be inserted inside the designated subprograms,
and would have to be at the call point, or in some kind of "indirection"
stub. I suppose one approach would be to interpret a pre/postcondition
pragma on an access-to-subprogram type as a requirement for statically
matching (or provably "stronger"?) pre/postconditions on all subprograms
to be designated by values of the type. That begins to get into
theorem proving, etc., which might be appropriate for a separate tool,
but is beyond what we want the "average" Ada compiler to have to do. ;-)
Invariant Pragmas
We have provided both type oriented and package oriented "invariant"
pragmas. This reflects the fact that some abstractions are
for abstract data types, while others are for abstract state machines.
We only enforce the package-oriented invariant on return from visible
procedures of the package. If a visible function has side-effects,
the implementor may want to insert an explicit postcondition on
the function, or a Assert pragma inside.
For type invariants, we apply them on [IN] OUT parameters of
procedures after the call, and on the result of functions and conversions.
The invariants are defined by referring to a boolean function.
The more general boolean_expression allowed in the other assertion-like
pragmas was not used because it was unlikely that the invariant
could be defined in terms of visible entities, and there was
no obvious way to refer to the particular instance of the type
for the Type_Invariant pragma. In addition, given that the
checks may be performed at the call point, space economization argues
for bundling the invariant into a callable subprogram. The programmer
might as well do this bundling him/herself.
Invariant checks apply to all calls on (relevant) procedures
declared in the visible part of the package, even those within the package.
This allows the checks to be performed inside the procedures rather than
at the call point, and makes the invariant pragmas equivalent to a series of
postcondition pragmas. We considered making invariant checks apply only to
calls from outside the package, but this appeared to complicate the
implementation and description with little additional benefit.
The invariant checks are performed as postcondition checks to ensure
that violations are caught as soon as possible. Presumably the invariants
could also be enforced as preconditions, but those checks would in
general be redundant, and the failures would be harder to track down
since the call that actually created the problem would be harder
to identify.
We do not specify any inheritance of invariant pragmas. It might
make sense for a type invariant to be inherited by its descendants.
However, in that case, a separate Inheritable_Type_Invariant would
probably be appropriate, based on the same argument given above
relating to inheritable pre/postcondition pragmas.
Presumably we would allow these pragmas in generic packages, with the
obvious semantics in the instance.
We have not specified whether the invariants apply to any
inherited primitive subprograms that are implicitly declared
within the package containing the pragma. We have not specified
whether invariants apply to dynamically-bound calls, which might
reach subprograms that are not declared in the visible part of
the package. Clearly these issues need to be resolved.
Assertion Policy
We have used the Assertion_Policy pragma defined in AI-00286,
with the same options and interpretation. It might make sense
to define separate pragmas, such as Precondition_Policy,
Postcondition_Policy, and Invariant_Policy, but with the
same set of identifiers. This would give the programmer more
control. On the other hand, typically either the programmer wants
full debugging, or full speed. Intermediate points seem relatively
rare.
!example
generic
type Item is private;
package Stacks is
type Stack is private;
function Is_Empty(S : in Stack) return Boolean;
function Is_Full(S : in Stack) return Boolean;
procedure Push(S : in out Stack; I : in Item);
pragma Precondition(Push, not Is_Full(S));
pragma Postcondition(Push, not Is_Empty(S));
procedure Pop(S : in out Stack; I : out Item);
pragma Precondition(Pop, not Is_Empty(S));
pragma Postcondition(Pop, not Is_Full(S));
function Top(S : in Stack) return Item;
pragma Precondition(Top, not Is_Empty(S));
function Is_Valid_Stack(S : in Stack) return Boolean;
pragma Type_Invariant(Stack, Is_Valid_Stack);
Stack_Error : exception;
private
--
end Stacks;
!ACATS test
!appendix
From: Tucker Taft
Sent: Wednesday, February 6, 2002, 12:19 PM
The semantics for inheritable preconditions is probably not quite
right in this proposal. It should be possible to "weaken" preconditions
as you go down the type hierarchy. This would imply that an
inherited precondition should be "or'ed" with the preconditions
specified directly on a subprogram, or perhaps simply overridden.
Probably the simplest is to say that an inherited precondition
represents a "default" precondition, which is overridden by
any other precondition specified directly on a primitive.
So if both Inherited_Precondition and Precondition are specified
on a primitive, then only the Precondition applies to the
primitive itself, while the Inherited_Precondition is the default
precondition for any overridings of the primitive.
If Inherited_Precondition is specified on an overriding, it becomes
the default for further overridings, replacing the Inherited_Precondition
applicable to the parent type's primitive.
This means that a precondition can be either strenghtened or
weakened as you go down a type hierarchy, but by default,
it stays the same. Strengthening a precondition as you go
down is a little weird, but not completely inappropriate.
The true "classwide" precondition for a primitive would be the "and"
of the specific preconditions on each implementation of the primitive.
It would be wise for a user to define the Inherited_Precondition so
that it matches this combination, or is stronger than it. But it is
probably not practical to try to enforce this, nor is it wise to
implicitly "weaken" a precondition specified explicitly on a primitive by
"or"ing in the Inherited_Precondition.
****************************************************************
From: Robert Dewar
Sent: Sunday, March 10, 2002, 11:05 AM
I find this the kind of proposal that should be made AFTER people have
some experience with the facility. If you can't get anyone to implement
a trial version, then that is itself an indication that the proposal is
reaching. I certainly don't see any serious users of Ada champing at the
bit for this type of capability, but it would seem quite reasonable for
someone to experiment with the implementation of something like this.
I certainly do NOT think it is reasonable to try to even semi-standardize
a facility of this kind without implementation and usage experience.
****************************************************************
From: Tucker Taft
Sent: Monday, March 11, 2002, 9:01 PM
> > Also, we do provide an inheritable type invariant,
> > even though the discussion says we don't. Sorry about that...
>
> Umm, I can't find anything in the proposal that says that either
> Type_Invariant or Class_Type_Invariant is inherited. Thus, I left the
> discussion alone.
The Class_Type_Invariant applies to all types in the
derivation class, so that implies it is inherited.
****************************************************************
From: Randy Brukardt
Sent: Monday, March 11, 2002, 9:16 PM
Humm, OK, I didn't view that as "inheritance". (The difference between
classwide operations and inherited ones is very important to keep straight
in Ada.) What else with a class_type_invariant apply to except to all
members of the class?
But if this is inheritance, you would need to say something about overriding
(as you did for pre and post conditions). OTOH, if it is additive, then it
isn't inheritance (at least not in the traditional sense).
****************************************************************
From: Tucker Taft
Sent: Friday, October 18, 2002, 4:00 PM
When we last discussed AI-288, which introduced the concept
of pre/post condition pragmas (and invariants), we expressed
concern about the infinite recursion problem, if a two subprograms
were mutually recursive when the pre/post conditions were
taken into account. An example used was:
function Is_Empty(S : Stack) return Boolean;
pragma Postcondition(Is_Empty, not (Is_Empty'Result and Is_Full(S)));
function Is_Full(S : Stack) return Boolean;
pragma Postcondition(Is_Full, not (Is_Full'Result and Is_Empty(S)));
Apparently Eiffel suppresses pre/post conditions when evaluating
pre/post conditions. This seems like a kludge, and certainly
makes implementation significantly harder, since you need
non-checking versions, and you have to compile pre/post conditions
using a different mode.
In thinking more about this, the simplest solution seems to be
"programmer beware." The above example is not a very good one,
and perhaps if there were a more convincing example I would
be more sympathetic, but it seems easy enough for the programmer
to watch out for these situations.
In general, the functions used in pre/post conditions should
be pure (or nearly so ;-), and should not have significant
preconditions of their own. Postconditions on a function
seem like somewhat odd beasts in any case, and would probably
be used sparingly. They would presumably express properties
of the returned value such as /= 0, or /= null. Using them
to express an identity would seem to be adequately handled
by having the identity on only one of the functions involved,
rather than on both. E.g.
function "/="(Left, Right : T) return Boolean;
pragma Postcondition("/=", "/="'Result = not (Left = Right));
There would seem no need to put the complementary identity
on the "=" function.
Similarly, one might express the effect of "<", "<=", and ">="
in terms of ">", but then it would be odd to express the
effect of ">" in terms of "<", because then you effectively
have a circular definition.
In any case, in my revision of AI-288 (which will also be
split into two), I plan to propose to treat the problem of
infinite recursion for pre/post conditions as the programmer's
problem, rather than the implementor's problem.
****************************************************************
From: Robert A. Duff
Sent: Friday, October 18, 2002, 4:31 PM
> Postconditions on a function
> seem like somewhat odd beasts in any case, and would probably
> be used sparingly. They would presumably express properties
> of the returned value such as /= 0, or /= null.
Please explain why they are "odd beasts". I agree that they normally
"express properties of the returned value". But why are the examples
"/= 0, or /= null" usual? Why not properties expressed in terms of the
input parameters?
> In any case, in my revision of AI-288 (which will also be
> split into two), I plan to propose to treat the problem of
> infinite recursion for pre/post conditions as the programmer's
> problem, rather than the implementor's problem.
That seem wise. I can't think of any better way to deal with mutual
recursion.
****************************************************************
From: Alan Burns
Sent: Tuesday, January 7, 2003, 5:01 AM
he HRG was asked (by ARG) to look at these AIs on
assert and pre/post conditions etc.
Please find attached our considerations (which
was on the whole are not supportive). To prevent these
thoughts getting lost, perhaps they should be
incorporated into the AIs
----
Comment from the HRG on AI288 - Pre/Postconditions and Invariants
The AI proposes the extension of the assertion mechanism (AI286) to
provide support for "programming by contract". Specifically it provides
a mechanism to express pre and postconditions for operations and
statements about invariant properties of types and packages.
As with AI286, the fundamental question to be answered is "does the
proposal aid the construction and verification of high-integrity,
software-driven systems"?
The proposal has a number of problems that, in the HRG's opinion,
results in a negative answer to this question.
In particular, as presented, the AI describes a mechanism that is
more suitable for debugging than constructing a system "by contract".
The author appears to recognise this by stating its aim as: "to ... catch
errors in usage or implementation earlier in the development cycle".
Specific weakness in the proposal include the following:
1. It is built on the Assert mechanism proposed in AI286 and
shares all the problems associated with that AI. Indeed, some of those
weaknesses are more severe if assert is to be employed in the
way proposed. In particular, the desire to promote the contract to
package specifications is fundamentally incompatible with the visibility
rules of Ada. How, for example, will the invariant condition of an
abstract state machine package be expressed in its specification if the
data to which the invariant applies is, correctly, hidden in the package
body? Only a proliferation of extra functions (perhaps with side-
effects?) can be employed.
2. Although the attribute "incoming" provides the initial value of
parameters that are imported and exported by an operation, there is no
equivalent mechanism for global variables used by the operation. This
makes it impossible to express pre and post conditions that rely on the
initial values of global variables. Since such globals may well be
invisible at the point where the pre/post condition is being expressed,
this deficiency may well be insoluble.
Trivial example:
X : Integer;
...
procedure Inc is
begin
X := X + 1;
end Inc;
The postcondition of Inc, "X = X'Incoming + 1, cannot be expressed.
Furthermore, the value X'Incoming cannot be provided by the compiler
because, unlike a parameter which has its mode, we don't know whether a
global is referenced or updated until we reach the sequence of
statements in the subprogram body. The initial value could only be
provided if some form of flow analysis was performed before compilation.
3. The AI proposes that postconditions are evaluated at the end of a
subprogram's normal execution but before any copying back of exported
parameters. Unfortunately, if the postcondition assertion fails, then
any parameters passed by reference and updating global variables will
already have been modified. The system "state" is therefore in an
unknown condition when the exception is raised making its use in
deployed systems problematic. The fact that system behaviour after a
failed postcondition depends on the parameter passing mechanism used
introduces a new and unwelcome form of "undefined" behaviour which is
inappropriate for the high-integrity systems at which the AI is aimed.
4. The proposed freedom to allow any form of pre and postcondition for
overidden tagged operations is dangerously flawed. For any sensible
tagged type hierarchy, it must be the case that:
Root op precondition -> Overridden op precondition and
Overridden op postcondition -> Root op postcondition.
In other words, an overriding operation must "ask less and promise
more". These rules are well established by the work of Barbara Liskov
and Jeannette Wing and are partially implemented in Eiffel. Any attempt
to present Ada as providing "programming by contract" which was even
weaker than Eiffel in this respect would be very harmful to the
credibility of the language.
Conclusion
----------
The HRG cannot support this proposal in its current form.
****************************************************************
From: Tucker Taft
Sent: Tuesday, January 7, 2003, 6:00 AM
Well, that is a "pan" if I ever saw one ;-).
However, I am wondering whether the HRG had any notion
of what "form" of proposal they might support?
... or do they conclude that any improvement in this area
is beyond the scope of the standard? In other words,
was the ultimate suggestion "drop it" or "try harder"?
****************************************************************
From: Alan Burns
Sent: Tuesday, January 7, 2003, 7:21 AM
In such stark terms I think the view was "drop it", but let me
deconstruct that a bit. The HRG looked at these as `do they
help verification', in other words do they help static analysis.
And the view was no they do not (for reasons explained in the
emails). But if you view these AIs as helping construct run-time
checks for protected execution then they may well be fine.
The HRG does not believe that the static analysis and dynamic protection
can be obtained from the same language primitives. Static analysis
needs so much extra stuff (specifications, visibility into inner
scopes etc) if these are represented as comments then there is no
confusion. Run-time checks are part of the execution and have a
different role.
So do not drop it if there is value in terms of dynamic protection,
just put the emphasis there.
****************************************************************
Questions? Ask the ACAA Technical Agent