Correctness conditions for calling an agent

by Colin Adams (modified: 2007 Mar 17)

I was recently reading the paper "From Design Patterns to Reusable Components: The Factory Library by Karine Arnout and Bertrand Meyer" and I noticed that although they had succeeded in turning the pattern "Abstract Factory" into a component, the resulting class (ABSTRACT_FACTORY) did not have a sound contract.

The reasons were that the basic feature, `new', has a post-condition that says its Result is non-Void, and no pre-conditions. Yet there was no attempt to ensure that calling the agent would deliver the post-condition, or indeed that it was safe to call the agent at all.

This is a general problem for routines that receive an arbitrary agent, such as an iterator.

It appears that this particular design pattern should really be classified as one of those that could be implemented with sufficient support from the language. And that therefore Eiffel could be fruitfully extended to achieve this.

Actually, if I inspect class ROUTINE (in EiffelStudio 5.7), I see that the necessary routines are already there - they are just not implemented yet:

precondition (args: like operands): BOOLEAN is -- Do `args' satisfy routine's precondition -- in current state? do Result := True --| FIXME compiler support needed! end postcondition (args: like operands): BOOLEAN is -- Does current state satisfy routine's -- postcondition for `args'? do Result := True --| FIXME compiler support needed! end

These two routines (along with valid_operands, which already works correctly) provide most of what is needed to ensure correct operation for a routine that receives a generic agent.

I say almost, as it is not quite enough.

Back to {ABSTRACT_FACTORY}.new. As I mentioned before, its post-condition said that the Result was not Void. This Result comes directly from the agent (which must be a FUNCTION). So a further condition for correctness of this routine would be to ascertain that the agent indeed guaranteed a non-Void Result.


In this particular case, the post-condition can be removed altogether, by making use of an attachment mark in the return type of the agent (at least, I think ECMA syntax allows us to do this).

But I believe there may be a general need for routines that receive a generic agent to be able to interrogate the post-conditions of the agent.

Comments
  • Andreas Leitner (17 years ago 20/3/2007)

    Colin, you hit the nail on the head. The combination of agents are contracts leave room for improvement indeed.

    Example: what is the result of `for_all' in class LINEAR for example when you provide it with an agent that is bound to a routine whose precondition is not satisfied for all elements of a given container? Who's fault is it if a precondition of an agent invocation is violated?

    Another example: the routine postcondition' (as cited above) in its current state does not make much sense. How can a state statisfy a postcondition. Clearly a routine execution is missing. Otherwise how can a postcondition like count = old count + 1' ever be satisfied?

    Andreas

    • Colin Adams (17 years ago 25/3/2007)

      Contract of do_all

      It may be significant that postcondition has no clients that I can find. The obvious client is call, which ought to have a post-condition of:

      post_condition_satisfied: postcondition (args)

      I am also interested in the contract of {ARRAY}.do_all.

      Clearly if it is to be truly a do_all, the pre-condition of the agent must always hold. How to express this as a pre-condition for do_all? The obvious way to do it is to use for_all and {PROCEDURE}.precondition.

      But this is not sufficient, as the pre-conditions for the agent may depend upon the state of the agent, which might change during the execution of do_all.


      It would seem that at present we are obliged to state the pre-condition as a comment. The implication (for the verifying compiler) seems to be that do_all cannot be proven statically to be correct, and only do_if should ever be used.

      Colin Adams