Safety Property: NetLimitOpenConnections

property NetLimitOpenConnections (n: int) {
  requires GlobalNetworkOpenState;
  check RNetwork.preOpenConnection (connection: RNetConnection) {
    if (openConnections.size () >= n) {
      violation ("Too many open connections.  Only " +
                 n + " open connections allowed.");
    }
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science