Safety Property: JavaAppletProperties

property JavaAppletProperties {
   requires JavaAppletInitialized;

   check RSystem.observeAllProperties () {
     violation ("Cannot observe all properties!");
   }

   check RSystem.observeProperty (key: String) {
     if (isJavaInitialized) {
       String prop = System.getProperty (key + ".applet");
       boolean allow = new Boolean(prop).booleanValue();
       
       if (!allow) {
         violation ("Cannot observe property: " + key);
       }
     }
   }
}

About this file

Naccio Home Page
David Evans
University of Virginia, Computer Science