Safety Property: ReportFileUsage

property ReportFileUsage {
  requires TrackTotalBytesWritten, TrackTotalBytesRead;
  
  postcode RFileSystem.terminate () {
    if (bytes_written > 0) {
      statusMessage ("FileSystem Bytes Written: " + bytes_written);
    } 
    
    if (bytes_read > 0) {
      statusMessage ("FileSystem Bytes Read: " + bytes_read);
    } 
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science