Safety Property: NoObserveProperty

property NoObserveProperty (s: String) {
  check RSystem.observeProperty (key: String) { 
    if (key.equals (s)) {
      violation ("Attempt to observe property " + s + 
                 " violates NoObserveProperty.");
    }
  }

  check RSystem.observeAllProperties () {
    violation 
      ("Attempt to observe all properties prohibitied by NoObservePolicy (" +
       s + ")");
  }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science