Safety Property: LimitOpenFiles

property LimitOpenFiles (n: int) { // no more than n files may be open
   requires TrackOpenFiles, FileNames;
   check RFileSystem.openRead (file: RFile), 
         RFileSystem.openCreate (file: RFile),
         RFileSystem.openOverwrite (file: RFile), 
         RFileSystem.openAppend (file: RFile) {
     if (openFiles > n) {
       violation ("File open limit reached.  Attempt to open more than " + n +
                  " files.  Opening " + file.getName () + ".");
     }
   }    
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science