JavaMOP Web Interface

Here we provide a web-based interface to try JavaMOP online. One can click on any of the following examples, upload testing programs to see the result using the form below, or click here to paste testing code. Check here for the syntax of the JavaMOP specification.

 Related projects: Monitoring-Oriented Programming; JavaMOP; MOP logic repository

Upload Testing Programs

Please use the following form to upload the testing program. The uploaded program will be displayed in a new window for further editing. If one wants to copy and paste or type in the testing code directly, please click here to open the editing window.

Examples

All the examples listed below are organized according to the logic formalisms that they use.

Extended Regular Expression(ERE) Based Specifications

• File.java: advanced logging behavior
• HasNext.mop: a call to Iterator.next() should always follow a call to Iterator.hasNext()
• ListenerPattern.mop: an MOP specification to implement the listener pattern in JHotDraw
• SafeEnum.mop: the elements of a collection should not be changed when an enumeration is used to iterate the elements
• SafeIterator.mop: the elements of a vector should not be changed when an iterator is used to iterate the elements
• HashMap.mop: the hashcode of a object should not be changed if the object is used as the key in a hashmap
• Hashtable.mop: the hashcode of a object should not be changed if the object is used as the key in a hashtable
• HashSet.mop: the hashcode of a object should not be changed if the object is stored in a HashSet
• NullChecker.mop: keep track of those fields who are assigned to null and use this information to help diagnose NullPointerException
• LeakingSync.mop: if a synchronized wrapper is created for a collection/map, it should be used afterwards instead of the original object
• ClosedReader.mop: a reader should not be read from if the underlying input stream has been closed
• ClosedWriter.mop: a writer should not be written on if the underlying output stream has been closed

Note: the last nine properties are parametric; all properties above, except for the File logging, are taken over and adapted from the benchmark set of Tracematches

New Past Time Linear Temporal Logic(PTLTL) Based Specifications

• ptHasNext.mop: a call to Iterator.next() should always follow a call to Iterator.hasNext()
• ptSafeIterator.mop: the elements of a vector should not be changed when an iterator is used to iterate the elements

Past Time Linear Temporal Logic(PTLTL) Based Specifications

• Resource.java: enforcing a simple security policy of resource access

Future Time Linear Temporal Logic(FTLTL) Based Specifications

• CarController.java: implementing the cruise control system by specifying the desired property
• CarController2.java: more complicated cruise control system

Java Modeling Language (JML) Based Specifications

• Controller.java: simple fault-tolerant mechanism
• Point.java: efficient display redrawing behavior