This intention changes a library method contract.
Method contract has the following syntax:
contract ::= (clause ';')* clause
clause ::= args '->' effect
args ::= ((arg ',')* arg )?
arg ::= value-constraint
value-constraint ::= '_' | 'null' | '!null' | 'false' | 'true'
effect ::= value-constraint | 'fail' | 'new' | 'this' | 'param' number
number ::= [1-9] [0-9]*
The constraints denote the following:
- _ - any value
- null - null value
- !null - a value statically proved to be not-null
- true - true boolean value
- false - false boolean value
- fail - the method throws exception, if the arguments satisfy argument constraints
- new - every time the method is executed, it returns a non-null new object that is distinct from other objects existing in the heap prior to method execution. If the method is pure, the new object is not stored in any field or array and will be lost if method return value is not used.
- this - the method returns non-null this reference
- param1 (param2, param3, etc.) - the method returns its first (second, third, etc.) argument
Examples:
@Contract("_, null -> null")
- method returns null if its second argument is null
@Contract("_, null -> null; _, !null -> !null")
- method returns null if its second argument is null and not-null otherwise
@Contract("true -> fail")
- a typical assertFalse method which throws an exception if true
is passed to it