Online Eiffel Documentation
EiffelStudio

Precondition

Enter a precondition in the require field. A precondition clause will be added to the feature:

...
require
	n >= 0
...