The behavior of a type is specified by the actions it participates in. Each action is specified by (some number of) actions spec(s). An action spec defines the effects of that action in terms of the attributes of the objects involved, and the conditions under which those effects hold, using:

The postconditions and guarantee must hold for any action occurrence, provided its precondition and rely condition were met. The rely and guarantee conditions are less often utilized, and only for non-atomic actions with significant duration, which can happen concurrently with other actions.

For example, the Order object type may have associated actions fulfill, invoice, and pay. An action specification may look as follows:

-- What it means to fulfill an order
Order :: fulfill
pre: the order must be in the pending state
rely: while the order is being fulfilled the product specifications had better not change
post: the fulfilled order has been shipped to the customer based on the product specifications, and the order has been inserted into the billing queue
guarantee: true i.e. not particular rule maintained during an order's fulfillment.

Invariants add implicit constraints to all actions (within the "scope" of those invariants). Static invariants must apply at states before and after each action, are implicitly added to all the preconditions and postconditions of all those actions; and dynamic invariants (also called "effect invariants") apply to each postcondition (state transition) for all those actions.

For example, if our static invariants already ruled that no two lineItems in an order can be for the same product, then we do not need to re-state this in the pre/post conditions of fulfill. Similarly, if we had a dynamic invariant that ruled any time the billing queue changes, the accounting department is notified, then we do not need to re-state this in the postcondition of fulfill.   

A state transition is a graphical definition of an action specification.

A significant part of good models depends on using techniques to simplify action specifications so they form a natural description for the client's conceptual view of things. Convenience attributes, effects, subtypes, and joins are all useful ways of structuring a model so they are conceptually simply, yet can still be made precise if needed.

For example, the postcondition the order has been inserted into the billing queue could be simplified by simply defining the state (convenience boolean attribute) billable to mean the same as the order is in the billing queue. Then the postcondition would simply need to say the order is billable.

Further, if the postcondition was more complex: the order has been inserted into the billing queue of the accounting representative with the least billing backlog in that customer's region... you would greatly simplify that by introducing a convenience attribute on order called accountingRepOfChoice, define that to mean the accounting representative with the least billing backlog in that customer's region... and describe the postcondition as the order is billable with the accountingRepOfChoice for that order.