[[Property:title|Design by Contract in SCOOP]]
[[Property:link_title|Design by Contract]]
[[Property:weight|5]]
[[Property:uuid|f8df5904-d1ee-31d7-f618-fb8bf1ddc876]]

The backbone of the Eiffel Method is design by contract. Preconditions, postconditions, and class invariants are used in Eiffel for extending software interfaces into software specification. This is essentially the same in concurrent Eiffel with SCOOP as it is in traditional, sequential Eiffel. However, because of the concurrent nature of processing under SCOOP, the runtime semantics of the elements of Design by Contract are different for concurrent systems.


==Preconditions==

The role of the precondition is somewhat different in SCOOP than in sequential Eiffel. In non-concurrent Eiffel we view the precondition of a routine as defining a set of obligations on potential callers of the routine. That is, the set of conditions that must be true before correct execution of the routine can be expected. So, we could look at the precondition clauses in sequential Eiffel as '''correctness conditions'''. A typical example might be a square root routine that returns the square root of a passed argument value. A precondition clause, i. e., a correctness condition, for this routine will be that the argument must be non-negative. It is the responsibility of the caller to ensure that this property of the argument holds at the time of the feature call.

In concurrent Eiffel, the same correctness conditions are still valid, but there are cases in which we must view the clients role here a little differently.
In the case of a precondition clause that depends on a separate object, even if the client tests the condition ahead of the call, there is no assurance that action by some other concurrent processor may have invalidated the precondition clause between the time that the check was made and the time that the feature application takes place.

In SCOOP preconditions can therefore additionally take the role of a '''wait condition'''.
Wait conditions are useful for cases where the caller can't guarantee that a property on an object is true at the time of the call, but it knows that it will eventually become true.
If a wait condition fails, the current processor will stall its execution, release the locks on its arguments, and wait until the precondition is fulfilled.

A typical example is a <code>CONSUMER</code> object trying to dequeue an item from a shared <code>BUFFER</code>.
In the following example, the precondition in <code>{CONSUMER}.consume</code> is treated as a wait condition:
<code>
class CONSUMER feature
	consume (a_buffer: separate BUFFER): INTEGER
		require
			not_empty: not a_buffer.is_empty
		do
			Result := a_buffer.item
			a_buffer.remove
		end
end
</code>

A precondition clause is only treated as a wait condition when there's a separate call.
However, the opposite is not true - not all precondition clauses with a separate call are treated as wait conditions.
The rule is a bit tricky to understand, but as a general rule of thumb, a precondition violation is raised when the SCOOP runtime detects that there's no possibility that a precondition clause may become true in the future if the routine releases its exclusive access.

{{Info| Alright, here are the exact rules: The decision depends on the context of the '''caller''' of the routine.
If one of the separate objects used as a target in a precondition clause is ''locked'' (see definition in [[Asynchronous Calls]]) in the context of the caller, the precondition is treated as a correctness condition. Otherwise, it is a wait condition.}}

{{SeeAlso|The <code>{PRODUCER}.store</code> feature in the [[Producer-consumer|producer-consumer]] example. When called by <code>{PRODUCER}.produce</code> it becomes a '''wait condition'''.}}

==Postconditions==

As with preconditions the effect of concurrent execution can make a difference in how postconditions are viewed. 

If a routine has executed correctly, then the postcondition of the routine will hold at the time that it terminates. This is true whether or not concurrency is involved. However, when a postcondition involves separate calls, clients must be cautious about how they depend upon the state guaranteed by postconditions. 


==Class invariants==

The '''separate argument''' rule in [[Separate Calls]] tells us that a separate call is valid only on a target which is a formal arguments of the enclosing routine. Because class invariants are not routines and therefore have no arguments, separate calls are not allowed in class invariants. 

{{Info|Technically, it should be possible in a class invariant to code an inline agent that gets passed arguments of separate types, then execute separate calls within the inline agent. But generally, it can be assumed that class invariants contain no separate calls. }}

The semantics of class invariants will be the same as in sequential Eiffel, precisely because invariants must include only non-spearate calls. To put it the terms of SCOOP, the class invariant ensuring the validity of any particular object will be evaluated entirely by the processor handling that object.