Pre and post conditions for a method in the target class are defined by implementing a method in the contract which has the same parameter signature as the target's method and the same name, except that it is prefixed with "pre_" or "post_", respectively.
Due to the same parameter signature, pre conditions are invoked right before the target method with exactly the same arguments. For an example, click here.
The same as for pre conditions applies also for post conditions, except that they are called right after the target method returns. Therefore, they have access to the targets state after the target method has returned.
In order to gain access to some state information before the method was invoked, you can make use of the utility methods ContractBase.setPreconditionValue(String) and ContractBase.getPreconditionValue(String) if your contract extends ContractBase<T>. Finally, the return value of the target method is given by ContractBase.getReturnValue().
For an example, click here.