Documents a precondition. Applies to methods and routines, and sometimes to properties. A precondition is a statement which is assumed true when the method gets called. It is part of the contract between the caller and callee, with the "burden" on the caller. A good practice is to assert the preconditions of a method.
Example
@pre InputArgument1<>nil @pre InputArgument2 must be either 1,2 or 3.