Correctness of classes receiving an agent

by Colin Adams (modified: 2010 Jan 28)

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.

Comments
  • Manu (8 years ago 16/10/2008)

    Actually agent {SOME_TYPE}.g

    Actually agent {SOME_TYPE}.g is not simpler than its counterpart agent a.g, it is the same level of complexity. What you are suggesting is a continuation of what we already started doing in our compiler, that is to say catch errors early on. If you do agent a.f and that at creation time `a' is Void, we now generate a call on Void target (before it was only discovered when executing the agent).

    So I'd go further than what you suggested. Instead of setting `has_precondition' I'll actually evaluate all assertions not involving an argument in the two forms of an agent agent g and agent a.g. That way you catch errors early on. Same goes with checking the invariant.

    As for postcondition I'm not sure to see what you mean. Do not forget that you have `old' expressions in a postcondition and it makes it harder to verify a postcondition of a routine outside its execution.

    • Colin Adams (8 years ago 16/10/2008)

      Are you saying you will evaluate the preconditions at compile time, or at runtime?

      Anyway, that does not address the problem that I was trying to deal with, which is the correctness condition for a class such as FACTORY. What precondition on the agent does the author write, so that clients know which agents they can pass?

      For postconditions, I was only suggesting a marker. Not verification.

      Colin Adams

      • Manu (8 years ago 17/10/2008)

        In a few years from now, we would evaluate some at compile time, but for the time being, it would be at runtime.

        For your other question, in the factory class you are saying that you do not want any precondition that cannot be easily evaluate to True. My experience shows that if you want to be 100% sure, you need to pass a routine that does not have any precondition. What I'd like to see however is a way to specify in the type of the agent some constraint. For example:

        my_action (p: PROCEDURE [ANY, TUPLE [a: STRING]] require a /= Void)

        Which simply says to the client of `my_action' that he can safely pass an agent with the same precondition. It is not perfect and it still does not protect us, but it would help us writing less defensive programming when using agents for which you currently have no way to know how you are going to be called.

        • Colin Adams (8 years ago 17/10/2008)

          Firstly, that particular precondition isn't necessary, since we can use an attachment marker.

          But more seriously, in the general case, this doesn't help, as the problem is not whether the client can meet the preconditions of the supplier, but whether the supplier can meet the preconditions of the agent.

          Anyway, evaluating at compile time is impossible (as the precondition might involve an attribute, which changes in value between compile time and agent-call time), and evaluation at agent creation runtime has the same problem.

          Evaluation at agent call time is what we have now, and results in exceptions (precondition violation by the caller of the agent). this is a bug in the caller of the agent, and it is impossible to fix.

          My thesis is that usually (I haven't seen a counter-example in practise yet, although I can envisage some) the supplier can never meet the preconditions for the agent. My proposal therefore provides a practical solution that will work correctly. If it turns out that the agent call will fail due to a precondition violation, then the agent creation fails first due to a precondition violation, and this correctly place the blame on the creator of the agent, where it can be fixed.

          Colin Adams

          • Manu (8 years ago 17/10/2008)

            What I'm saying is that whenever you can, you evaluate a precondition at compile time during the agent creation. If not you do it at runtime. Of course not all the assertions can be verified (like the one involving an attribute), but you can easily verify the ones for which it involves one of the closed operands. In both cases, you get the precondition violation much earlier than at agent call time and getting a correctness violation earlier is always better.

            My proposal is to help programmers write their routine properly which is I think an issue when you want to use a library and you have no idea on how the library is going to call your agents which what matters. Supplier is for me the one providing the agent and the client is the one calling it; in this definition it is up to the supplier to provide weaker precondition than the one requested by the client.

            • Colin Adams (8 years ago 17/10/2008)

              What assertions are you going to be checking against? At the moment, we have no way of specifying any assertions.

              And how do you make a library like FACTORY (or a routine like do_all) correct? My proposal addresses that directly.

              Colin Adams