A precondition annotation to indicate that a method requires certain expressions to have a
certain qualifier at the time of the call to the method. The expressions for which the annotation
must hold after the method's execution are indicated by expression and are specified
using a string. The qualifier is specified by qualifier.