Code template for a precondition contract clause. Eiffel Software require code