Documents a postcondition. Applies to methods and routines, and sometimes to properties. A postcondition is a statement which you as a caller can assume to be true when the method (etc) returns. It is part of the contract between the caller and callee, with the "burden" on the callee.