property LimitBytesWrittenSimple (limit: int) {
requires TrackTotalBytesWritten;
check RFileSystem.preWrite (file: RFile, n: int) {
if (bytes_written + n > limit) {
violation
("Attempt to write more than " + limit +
" bytes. Writing " + n + ".");
}
}
}
Naccio Home Page
University of Virginia, Computer Science