--%>
Assignment Help - homework help

Property Specifications of Java Pathfinder

Property Specifications: The most straightforward way to specify and check simple safety properties in JPF is to use Java assertions inside the application under analysis. This allows the specification of properties that only depend on the application data values (e.g., parameter value intervals). Violations are caught by JPF. The drawbacks of this method are that it requires access to the application sources, and that it can significantly increase the state space if the property requires evaluation state itself (e.g., for properties implemented as automatons).

The other way to specify properties is by using gov.nasa.jpf.Property or gov.nasa.jpf.GenericProperty instances to encapsulate property checks.

50_property spec.jpg

The user typically creates an instance of such a class and provides an implementation for its check() method which does the main work for checking the property. The check()method is evaluated after each transition. If it returns false and termination has been requested, the search process ends, and all violated properties are printed (which potentially includes error traces).

JPF comes with generic Property classes for the following properties:

  • No Deadlocks
  • No Assertion Violation
  • No Uncaught Exceptions (i.e., not handled inside the application)

   Related Questions in Programming Languages

  • Q : Define Applet Applet : The Applets are

    Applet: The Applets are Java programs based on the Applet or JApplet classes. They are closely related with the capability to give active content within the Web pages. They have numerous features that differentiate them from ordinary Java graphical ap

    		•
  • Q : Explain Array initializer Array

    Array initializer: This is an initializer for an array. The initializer takes the position of separate creation and initialization steps. For example, the initializer int[] pair = { 4, 2, };

    Q : Ways in which Java program is less

    Give two ways in which a Java program is less likely to be compromised than the same program written in C++.

    		•
  • Q : What is Classpath Classpath : The path

    Classpath: The path searched by interpreter and compiler for class definitions. The class path might be set by a command-line argument to either, or through an environment variable.

    		•
  • Q : Explain Functional programming

    Functional programming: It is a style of programming related with languages like Haskell. The functional programming languages are more strongly tied to a mathematical concept of `function' than imperative programming languages. This makes it simpler

    		•
  • Q : What is Filter stream Filter stream :

    Filter stream: It is an input-output class which filters or manipulates its stream of input- or output-data in some manner. Two illustrations are: DataInputStream and DataOutputStream.

    		•
  • Q : Explain Declaration and initialization

    Declaration and initialization: It is a statement in which a variable is declared and instantly given its initial value. Three illustrations of declaration and initialization are as follows:     int

    		•
  • Q : What is Avoid Redundancy Avoid

    Avoid Redundancy: While not every form of redundancy is as bad from a verification perspective as it is from a maintenance point of view, behavioral redundancy to re-create (local) state can impose problems because the model checker does not distingui

    		•
  • Q : Describe Unnamed package Unnamed

    Unnamed package: All classes defined in the files without a package declaration are placed in an unnamed package.

    		•
  • Q : Difference between the choice and list

    Illustrate the difference between the choice and list?

    		•