Code template for a postcondition contract clause. Eiffel Software ensure code