IncFileUse:
PROC [file: File.Capability, exclusive:
BOOL ←
TRUE]
RETURNS [ok:
BOOL];
... increments # of users of a given file. If exclusive, then the increment only takes place if the initial count was 0. If not exclusive, the increment only takes place if the file is not exclusively open.
DecFileUse:
PROC [file: File.Capability];
... decrements # of users of a given file, raising DecFileUseError if the initial count = 0.
DecFileUseError: ERROR;
FileUseCount:
PROC [file: File.Capability]
RETURNS [count:
INT, exclusive:
BOOL];
... returns # of users of a given file, and whether the file is open exclusively.
IsFileUsed:
PROC [file: File.Capability]
RETURNS [
BOOL];
... equivalent to FileUseCount[file] > 0
END.