Property Specification in Java PathFinder: In Java PathFinder, properties are specified in Java. JPF can check a number of properties out of the box:
- No Deadlocks
- No Assertion Violation
- No Uncaught Exceptions (i.e., no exceptions that are not handled inside the application)
- No Race conditions
For assertion violations, you must add Java assert statements to the source code. Java PathFinder then reports when those assertions are not satisfied. For other types of default properties, no special annotations are necessary. All that is needed is that they are activated through configuration options.
JPF also allows you to add new properties through a well-defined interface. This interface lets you access not only the state of the program under analysis but also the state of the model checker itself.
The same interface can also be used to implement temporal properties, but it is your responsibility to write the code (e.g., an automaton) to keep track of successive states used to verify the property.
All the properties can be activated and deactivated as required through configuration options.