--%>
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 : Describe the term Context Switch

    Describe the term Context Switch.

    		•
  • Q : Define Zip file Zip file : It is a file

    Zip file: It is a file employed to store compressed versions of the files. In connection with Java bytecode files, such have mostly been superseded by the Java Archive (abbreviated as JAR) files.

    		•
  • Q : Explain Twos-complement notation

    Twos-complement notation: In twos-complement notation, the most noteworthy bit in an integer value is employed as the sign bit. A 1 bit points out a negative number, and a 0 bit points out a positive number. The positive number can be transformed to i

    		•
  • Q : Explain why java is so important for

    The internet aided java to the forefront of programming. And java consequently has had a deep effect on the internet. The reason for this is highly simple: java uses the universe of objects that can travel freely in cyber space. In a network, two broad categories of

    		•
  • Q : Define Thread Thread : It is a

    Thread: It is a lightweight procedure which is managed by the Java Virtual Machine (abbreviated as JVM). Support for threads is given by the Thread class in java.lang package.

    		•
  • Q : Use Finite-State Space Abstractions Use

    Use Finite-State Space Abstractions: In order to successfully apply explicit-state model checking, defects must be detectable in a sufficiently small state space. This can be achieved either by means of heuristics that constrain the way the state spac

    		•
  • Q : Write a program that prints out all

    Write a program that prints out all prime numbers between 1 and 1000. Print the values out ten per line, with digits lined in proper columns.

    		•
  • Q : Explain Swing Swing : The Swing classes

    Swing: The Swing classes are portion of a wider collection termed as the Java Foundation Classes (abbreviated as JFC). The swing classes are stated in the javax.swing packages. They give a further set of components which extend the capabilities of Abs

    		•
  • Q : State HyperText Transfer Protocol

    HyperText Transfer Protocol: The HyperText Transfer Protocol (abbreviated as HTTP) is a set of rules stated to enable a Web client (that is, browser) to interact with the Web server.

    		•
  • Q : Define the term Manifest file Define

    Define the term Manifest file: It is a file which is held in a Java Archive (JAR) file, explaining the contents of the archive.

    		•