Correctness conditions (2) for calling an agent

by Colin Adams (modified: 2010 Jan 28)

Following on from correctness_conditions_for_calling_an_agent, I have thought about the following scheme (it would require ECMA to be amended to require a tag on assertions, but this should be done anyway. Also, the tag would have to be unique with all the preconditions for a given feature - likewise for postconditions.):

class ROUTINE feature -- Access preconditions: !ARRAY [STRING] -- All precondition tags for `Current' ensure no_void_results: not Result.has (Void) no_empty_strings: Result.for_all (agent {STRING}.is_empty) postconditions: !ARRAY [STRING] -- All postcondition tags for `Current' ensure no_void_results: not Result.has (Void) no_empty_strings: Result.for_all (agent {STRING}.is_empty) has_precondition (a_tag: !STRING): BOOLEAN -- Does `Current' have a precondition labeled `a_tag'? has_postcondition (a_tag: !STRING): BOOLEAN -- Does `Current' have a postcondition labeled `a_tag'? precondition_holds (a_tag: !STRING; a_args: like operands): BOOLEAN -- Does precondition `a_tag' evaluate to `True'? require has_precondition_a_tag: has_precondition (a_tag) valid_arguments_for_current: valid_operands (a_args) postcondition_holds (a_tag: !STRING; a_args: like operands): BOOLEAN -- Does postcondition `a_tag' evaluate to `True'? require has_postcondition_a_tag: has_postcondition (a_tag) valid_arguments_for_current: valid_operands (a_args) preconditions_hold (a_args: like operands): BOOLEAN -- Do all preconditions hold? require valid_arguments_for_current: valid_operands (a_args) do Result := preconditions.for_all (agent precondition_holds (?, a_args)) end postconditions_hold (a_args: like operands): BOOLEAN -- Do all postconditions hold? require valid_arguments_for_current: valid_operands (a_args) do Result := postconditions.for_all (agent postcondition_holds (?, a_args)) end feature -- Basic operations call (a_args: like operands) -- Call `Current' passing `a_args' as actual arguments. require valid_operands: valid_operands (args) preconditions_hold: preconditions_hold (a_args) ensure postconditions_hold: postconditions_hold (a_args)

This has the (unwanted, by me) additional effect that it is now safe to use inline agents in preconditions, as the client can test if the precondition for routine y holds by calling:

-- first build TUPLE l_args from l_arg1 and l_arg2 then: if (agent y).preconditions_hold (l_args) then y (l_arg1, l_arg2)

Inline agents are still horrible for stylistic reasons, but my proposal for a replacement will wait for a later message.

Comments

Eric Bezault (17 years ago 1/4/2007)
Nothing new that the ECMA committee didn't know

When you wrote:

no_empty_strings: Result.for_all (agent {STRING}.is_empty)

I guess you meant:

no_empty_strings: not Result.there_exists (agent {STRING}.is_empty)

Note that it would have been less confusing to write:

no_empty_strings: Result.for_all (agent (s: STRING): BOOLEAN do Result := not s.is_empty end)

! ;-)

Also, if routines precondition' and postcondition' (currently specified in ISE's ROUTINE class) were implemented, your proposal is not very different from the currently intended (but not explicitly specified, because not implemented) behavior:

call (a_args: like operands) -- Call `Current' passing `a_args' as actual arguments. require valid_operands: valid_operands (args) preconditions_hold: precondition (a_args) ensure postconditions_hold: postcondition (a_args)

I think that the problem we are facing is not really how to specify things correctly (using tags or not), but rather how to implement it. I'm sure that if ISE knew how to implement their precondition' and postcondition' routines in ROUTINE then `call' would be properly specified with these contracts. For example even today you can write:

if (agent y).precondition (l_args) then y (l_arg1, l_arg2)

but because `precondition' is not implemented and always returns True, this is useless.
- Colin Adams (17 years ago 1/4/2007)
  Tags
  
  Thanks for the correction, and the April Fool's joke.
  
  But I think that with my tags proposal, implementation should be fairly straight-forward, I would have thought (this was the point of the posting). (It also has the advantage that in most cases you will be able to write lighter-weight code, by just testing a particular precondition, when you know most hold from the context). Colin Adams
- Colin Adams (17 years ago 1/4/2007)
  Avoiding re-inventing the wheel
  
  How is one supposed to know what the ECMA committee have and have-not considered? This is one of the chief points from my article Learning from the W3C process. Colin Adams
  - Eric Bezault (17 years ago 1/4/2007)
    Closed standard design process
    
    I'll let Manu (the ECMA Eiffel committe convener) answer this question about the way ECMA works. I for one would prefer a more open process, and feel lucky to be part of this committee.
    - Manu (17 years ago 2/4/2007)
      ECMA process
      
      Anyone can join the process as long as you are part of either a company/institution that is an ECMA member. The minutes and various proposals are currently only accessible by the ECMA members. As far as I know, the committee is free to decide whatever it wants regarding the publication of the various documents used (minutes, drafts, ...).
Andreas Leitner (17 years ago 2/4/2007)
Maybe I am missing something, but I still don't see how postcondition_holds' can be implemented without calling the actual implementation? Or should the postcondition just be evaluated on the current state + arguments? If so, how can a postcondition_holds' ever ealuate to True for a postcondition like `count = old count + 1'?
- Colin Adams (17 years ago 2/4/2007)
  Calling the implementation
  
  By "calling the implementation", do you mean the implementation of the body or of the postcondition code?
  
  I don't see where the difficulty lies. It works in workbench mode.
  
  Colin Adams
  - Colin Adams (17 years ago 2/4/2007)
    Transmitting old values
    
    As usual, I answered too quickly, before thinking.
    
    I now see that preservation of old values across the call might be tricky (or not possible, for an implementation in Eiffel code). Colin Adams
    - Andreas Leitner (17 years ago 2/4/2007)
      I think its not only about the preservation. If you ask a routine whether a postcondition is satisfied, wich prestate and which poststate are you referring to? What is the meaning of `r.preconditions_hold ([1,2,3])'? Does it ask whether some past execution satisfied the postcondition, the last one, or maybe a hypthesized one?
      
      I am not completely clear on it either, but at the moment the only thing that makes sense to me is to ask either:
      
      1) Given this set of arguments, this prestate and this poststate, does the postcondition hold?
      
      2) For the last execution of this agent, did the postcondition hold?
      
      I think 1) is very tricky to implement. (What is a prestate and what is a poststate?) 2) is easier to implement, in fact it can be as simple as a variable. But in the end I am not sure about its usefulness, after all if the last execution failed I would have noticed because an exception was thrown. Btw, for 2) you don't need arguments either.
      
      Andreas
      - Franck Arnaud (17 years ago 11/4/2007)
        removing dynamic postconditions mitigates the problem but...
        
        You can escape old and state issues by not having postconditions in the ROUTINE interface. There's no use case I can think of for checking postcondition explicitly at runtime (a failed postcondition can only be a bug), while there's a use case for checking some preconditions as part of establishing the client fulfills its side of the contract and takes remedial action otherwise.
        
        Although even there is does get a bit fuzzy in that the only preconditions a client should be entitled to check is the preconditions which are part of the _static_ agent interface, for instance let's say we have a classic Eiffel pattern:
        
        deferred class DRAWABLE feature is_visible: BOOLEAN is -- Is drawable target ready to receive instructions? deferred end draw (a_shape: SHAPE) is -- Draw a shape on some target. require a_shape_not_void: a_shape /= Void visible: is_visible deferred end end
        
        which you would use as such:
        
        drawable: DRAWABLE ... if drawable.is_visible then drawable.draw (a_tower) end
        
        In agentified Eiffel the same pattern becomes:
        
        drawable: ROUTINE [ANY, TUPLE [SHAPE]] ... -- (1) generic preconditions checking if drawable.preconditions_holds ([a_tower]) then drawable.call ([a_tower]) end -- or (2) tagged preconditions checking if drawable.precondition_holds ("is_visible", [a_tower]) then drawable.call ([a_tower]) end
        
        Both patterns suffer from problems. (1) is checking too much, leaking debug code into non-debug execution flow. This illustrate the major drawback of exposing preconditions, it leaks the internal programming language plumbing inside the program. I think it has been a great strength of Eiffel to have fairly limited reflection facilities, so that you don't have "bits of compilers" leaking into programs, both conceptually and as part of the runtime footprint. This stuff is moving in the wrong direction.
        
        (2) suffers a variant of the same problem, in that while semantically equivalent to the classic Eiffel pattern, it has also leaked compiler stuff into runtime, with some drawbacks for example the tag is a string, so there will be no compilation time error if is_visible is renamed etc, or if there's a typo in the first place, and the compiler cannot, or painfully, dead code away the 'debug' contracts that are always true in a correct program (and that damage extend to all routines with the same signature that are agent targets, and their descendants!). Also code analysis or automated verification becomes a harder problem.
        
        Mark Harrah (17 years ago 12/4/2007)
        Agent Contracts
        
        I agree that exposing and then explicitly checking pre/postconditions is not desirable, at least not as a general solution to agent contracts. Here are some thoughts on a possible form of a solution.
        
        We have code that wants to call a feature that is bound at runtime. We may statically specify the type of feature (query or function) and the number, order, and type of open arguments that this feature must have.
        
        However, we cannot statically guarantee to the client that binds a feature and gives it to our code anything more about those arguments. Neither can we describe what we expect from the feature.
        
        So, we can currently write that we want the following entity:
        
        to_call: PROCEDURE[TARGET_TYPE, TUPLE[argument_1: TYPE_1; ...]]
        
        But, perhaps we want to write something more like
        
        to_call: agent_interface prototype
        
        (using 'agent_interface' as a keyword) for a feature `prototype' defined as:
        
        prototype(argument_1: TYPE_1; ...) -- Defines the contract of an agent require precondition_1: ... agent_interface ensure precondition_2: ... end
        
        The assignment
        
        to_call := agent implementation
        
        would require the feature implementation' to effect prototype' as if prototype' were a feature inherited as deferred. That is, implementation' would have to
        
        Be a procedure with arguments that conform to the arguments of `prototype' (as is currently required)
        
        Use assertion extensions (that is, 'require else' and 'ensure then')
        
        Have a combined precondition and combined postcondition (like a redeclaration of a feature)
        
        Additionally, I think there are some more details such as feature calls with `Current' as the target probably cannot or should not be allowed in the assertions of the interface.
        
        An example following the previously provided DRAWABLE/SHAPE example:
        
        to_do: agent_interface draw_shape draw_shape(drawable: DRAWABLE; a_shape: SHAPE) -- Draw a shape on the given target. require a_shape_not_void: a_shape /= Void visible: drawable.is_visible deferred end usage: drawable: DRAWABLE a_tower: SHAPE ... to_do := agent {DRAWABLE}.draw to_do.call([drawable, a_tower])
        
        EDIT: corrected example usage
        
        Simon Hudon (16 years ago 3/8/2007)
        Exposing pre/postconditions of agent
        
        I disagree with the point that opposes exposing the preconditions and postconditions of agents. It seems to me like the only way to get complete specifications of higher order routines (somewhat related to higher order functions). In simpler terms, the postcondition function of agents may be used in postconditions of routines that receive agents as parameters (directly or indirectly) to describe the work in terms of the given agent.
        
        If I bring the problem in a functional context, we can see what could be desirable for Eiffel. I'll use a lisp-like syntax and presume a design by contract macro set to make my example. Let specify the map function (for non-lispers: this function applies a given function to every elements of a list and returns a list containing the results).
        
        (def-dbc-function (map f list) (require (not (null? f))) (deferred) (ensure (implies (not (null? list)) (equal? result (cons (f (car list)) (map f (cdr list))))) (implies (null? list) (null? result))))
        
        We can see a parallel with iterators in Eiffel. The main problem is that we cannot specify a procedure like do_all as we did map since it applies a procedure object and we do not know what we may call the frame of the operation. I think that's why no easy definition comes up for the postcondition feature of routines.
        
        The only alternative is to write the loop as the implementation and the specification and then freeze the implementation. This is not quite convenient because there may be reasons to redefine it.
        
        Simon