Correctness of classes receiving an agent

This week I have again been considering the issue of the correctness of code that receives an agent (the last time I looked at this was page:correctness_conditions_2_for_calling_an_agent).

I return to the original class which provoked my initial ponderings on this - Karine Arnout's (now Karine Bezault) `FACTORY' class. Here is the text of the class (as available from http://se.ethz.ch/people/arnout/patterns/):

indexing description: "Factory creating objects of type `G' by using agents." library: "Factory library" author: "Karine Arnout" copyright: "Copyright (c) 2002-2004, ETH Zurich, Switzerland" license: "Eiffel Forum License v2 (see License.txt)" date: "$Date: 2004/03/15 $" revision: "$Revision: 1.0 $" class FACTORY [G] create make feature -- Initialization make (a_function: like factory_function) is -- Set `factory_function' to `a_function'. require a_function_not_void: a_function /= Void do factory_function := a_function ensure factory_function_set: factory_function = a_function end feature -- Status report valid_args (args: TUPLE): BOOLEAN is -- Are `args' valid to create a new instance of type `G'? do Result := factory_function.valid_operands (args) end feature -- Factory functions new: G is -- New instance of type `G' require valid_args: valid_args ([]) do factory_function.call ([]) Result := factory_function.last_result ensure new_not_void: Result /= Void end new_with_args (args: TUPLE): G is -- New instance of type `G' initialized with `args' require args_valid: valid_args (args) do factory_function.call (args) Result := factory_function.last_result ensure new_not_void: Result /= Void end feature -- Access factory_function: FUNCTION [ANY, TUPLE [], G] -- Factory function creating new instances of type `G' invariant factory_function_not_void: factory_function /= Void end

There are some problems with this class.

The first problem is the postcondition of `new' and `new_with_args'. This postcondition only holds if `factory_function' has the same postcondition, and there is no way to require this in the creation procedure. In this particular case, the issue is trivially fixed by changing the type of `factory_function' to FUNCTION [ANY, TUPLE, !G]. But in general, we cannot assert a postcondition of a called agent, so the problem remains.

The second problem (and I think this is more serious, perhaps), is the call on the agent may fail if the agent has unsatisfied preconditions. And there is no way to amend the class to check if the preconditions are satisfied or not.

I have been re-reading Karine's thesis this week, and it occurred to me that throughout the library, not only is it not possible to check if the agent's preconditions are satisfied, but that if it were possible, there isn't much the library classes could do about it (raise an exception, I suppose). So the real requirement seems to be that the agent has no non-trivial preconditions.

We recall that a trivial precondition is one that can be written as:

assertion_tag: True

Now that we have attached types, many non-trivial preconditions can be eliminated, and so the requirement that the agent has no non-trivial preconditions does not appear to be a severe limitation.

The question remains how to express this requirement in the class invariant for `FACTORY' (and correspondingly as a precondition to the creation procedure). A first attempt is:

no_non_trivial_precondition: True

This serves for documentation purposes, but programmers sometimes fail to notice such things, and an automated proof checker will effectively ignore it completely. We lose the benefit of runtime assertion monitoring.

So instead we could add an attribute to class `ROUTINE':

has_precondition: BOOLEAN -- Does `Current' have any non-trivial preconditions?

Now the invariant clause simply reads:

no_non_trivial_precondition: not factory_function.has_precondition

But we have gained nothing over using the existing query precondition (args) unless it proves possible to implement. I think it does.

In order to implement it, an Eiffel compiler needs to be able to check the preconditions when it sees the agent keyword.

The simplest form is

agent r

No problem here, I think. in the abstract syntax tree fragment for `r', just check each precondition present. If there are any preconditions whose expression is not just the keyword True, then leave `has_precondition' as False. otherwise set it to True.

Then there is the qualified variant:

agent a.g

I don't see any problem here either. The type of `a' is known to the compiler, so it should again be able to navigate to the relevant abstract syntax tree fragment.

Then there are open targets:

agent {SOME_TYPE}.g

This looks even simpler then the previous one to me, as the type is explicitly given.

But I have not implemented an Eiffel compiler. So I would like to hear what Manu, Eric and Helmut think of the practicality of this.

Returning to the issue of postconditions, what can a user of class FACTORY infer about the created object (and therefore rely upon to satisfy preconditions of feature calls on that object? Simply, whatever postconditions `factory_function' has. It would be nice to express this on the postcondition of new and new_with_args. We can do this with a documentation-style postcondition:

postconditions_from_factory_function: True

and this seems quite sufficient for a human reader of the class. Nor do I see much of a need for runtime assertion monitoring here. But it would be nice to have a notation that a tool could check, for automatic proofs.

I think it is quite easy to devise a suitable notation here. How about postconditions_from_factory_function: agent.factory_function ?

This avoids introducing any new keywords, and does not conflict with existing Eiffel syntax. Admittedly it has far from intuitive syntax, but that won't matter for a tool.