Don Harrison wrote:
> 
> Richie Bielak wrote:
> 
> :Samuel Tardieu wrote:
> :
> :[...]
> :>
> :> Well, I find the corresponding Ada code readable enough:
> :>
> :>    select
> :>       delay 0.010;               --  The 10ms you were talking about
> :>       raise Timeout_Failure;     --  Raise an exception, or do anything else
> :>                                  --  you need (use a fast version of
> :>                                  --  your computation for example).
> :>    then abort
> :>       [...your code here...]     --  This piece of code will be
> :>                                  --  aborted if it is not terminated within
> :>                                  --  the 10ms you required above.
> :>    end select;
> :>
> :
> :That's neat. Except that a postcondition will be part of the contract
> :(i.e. specification) for the routine, so the caller will know what to
> :expect. Your code is part of the implementation.
> 
> I agree - it's belongs in a contract.

I think it only belongs in a contract if the timing of an method
invocation is concerned. However, this avenue of the thread was started
with the observation that a program should not depend on timing in an
unspecified/undocumented way.

The execution time of a method is one thing we need to time, and for
this the postcondition is the proper place.

However, there are a lot more things we may have to time, but that are
not directly linked to a particular (interface of) an object. For
example:

- the timing between two iterations of a loop
- the interval between two read outs of a memory mapped IO-port
- the timing of the execution of a method where the timing is critical
  on the part of the calling method and not of the called method itself
- timing of the interaction with the user (which is not a method for
  which one can specify a contract)
- timing of a number of instructions within a method
- etc.

So even though timing specifications with postconditions are useful, it
definitely is not sufficient for many HRT systems.

-- 
Groeten, Karel Th�nissen

-- my e-mail address is scrambled to confuse spammers
-- remove the confusion to obtain my true address