Safety Property: NoWritingFiles

property NoWritingFiles {
  requires FileNames;
  precode RFileSystem.openOverwrite (file: RFile), 
          RFileSystem.openCreate (file: RFile),
          RFileSystem.openAppend (file: RFile) {
    violation ("Attempt to write file: " + file.getName ());
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science