Not File Exists Code template contract predicate to ensure a file does not exist on a local or networked drive Eiffel Software not_file_exists Eiffel code contract invariant precondition postcondition A string variable containing a path to a file