File Exists Code template contract predicate to ensure a file exists on a local or networked drive Eiffel Software file_exists Eiffel code contract invariant precondition postcondition A string variable containing a path to a file