Not Is null pointer
Code template contract predicate to ensure an entity represents a valid pointer
Eiffel Software
not_is_null
Eiffel
code
contract
invariant
precondition
postcondition
A entity representing a pointer
not_${pointer}_is_null: ${pointer} /= default_pointer${end}