Re: procedure Make_File_Gone (Name : in String);

[Robert A Duff <bobduff@shell01.TheWorld.com>]

tmoran@acm.org writes:

>> I'm of course partial to Purge for this use. :-)
>
> Another verb.  Both the phrase Delete_File and the word Purge say "go
> do something" and they leave unclear what to do if you can't do the
> action. I'd like to concisely make clear the post condition I'm trying
> to achieve - in this case, the absence of a file of the given name.

I think you mean precondition.  The postcondition of the two is
the same -- the file isn't there.

I think distinguishing Delete_File and Delete would be confusing.
How would you remember which is which?

I'd say Delete_File should raise an exception if the file doesn't
exist, and Maybe_Delete_File should silently do nothing in that case.

> Ideally this should be clear from the procedure name without having
> to look in the ARM or depend on a comment of uncertain modernity.
>
> And yes, there could be a race where someone created a new file of that
> name immediately afterward, but avoiding such races is part of the
> higher level design.

Sure, that's true of pretty-much all file operations.

- Bob