When `_ensures` is not used to annotate a function like in the following code: ``` _ensures true ``` The same applies to the annotations `_requires` when not used to annotate a function and `_invariant` when not used to annotate a loop.
When
_ensuresis not used to annotate a function like in the following code:The same applies to the annotations
_requireswhen not used to annotate a function and_invariantwhen not used to annotate a loop.