Safety Property: ReportNetworkUsage

property ReportNetworkUsage {
   requires GlobalNetworkByteCount;

   postcode RNetwork.terminate () {
     if (bytesSent > 0) {
       statusMessage ("Network Bytes Sent: " + bytesSent);
     } 
    
    if (bytesReceived > 0) {
      statusMessage ("Network Bytes Received: " + bytesReceived);
    } 
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science