--%>
Assignment Help - homework help

Environment Modeling in Java Pathfinder

Environment Modeling: In JPF, Java class files can be processed in two different ways:

A) As ordinary Java classes managed and executed by the host JVM (e.g., standard Java library classes, JPF implementation classes)

B) As “modeled” classes managed and processed (verified) by JPF

We have to clearly distinguish between these two modes. In particular, JPF’s “Model” layer has its own class and object model, which is completely different than and incompatible with the hidden class and object models of the underlying host JVM executing JPF.

Each standard JVM supports a Java Native Interface (JNI), that is used to delegate execution from the JVM-controlled bytecode down into the platform-dependent native layer (machine code). This is normally used to interface certain functionalities such as I/O or graphics to the platform OS and architecture. JPF provides an analogous mechanism to lower the “execution” level in JPF from JPF-controlled bytecode into JVM-controlled bytecode. This mechanism is called Model Java Interface (MJI). It supports the creation of dedicated classes to be executed by the underlying JVM rather than JPF. Such classes are not model checked by JPF.

   Related Questions in Programming Languages

  • Q : Explain Fully qualified class name

    Fully qualified class name: The name of a class, comprising any package name and including class name. The class outline is as follows:     package oddments;    class Outer

    		•
  • Q : Define Divide and conquer Divide and

    Divide and conquer: An approach to trouble solving which attempts to decrease an overall single big trouble into multiple simpler troubles.

    		•
  • Q : Explain Synchronized statement

    Synchronized statement: It is a statement in which an object-lock should be obtained for the target object prior to the body of the statement and can be entered. Employed to enclose a critical section in order to save a race hazard.

    		•
  • Q : What is Bridging method Bridging method

    Bridging method: A method which offers a bridge between methods of a class's public interface and its private implementation. Bridging methods will usually contain non-public visibility.

    		•
  • Q : Describe Throw an exception Throw an

    Throw an exception: Whenever an exceptional circumstance occurs in a program - frequently as an outcome of a logical error and exception object is formed and thrown. When the exception is not caught by an exception handler, the program will finish wit

    		•
  • Q : What is Parsing Parsing : Generally

    Parsing: Generally applied to the action of a compiler in examining a program source file for syntax errors. This is too employed more broadly to mean the analysis of the structure of input.

    		•
  • Q : ERD What is the meaning ofDerive the

    What is the meaning ofDerive the department and staff relations from the following ERD.

    		•
  • Q : What is Behavior Behavior : It is the

    Behavior: It is the methods of a class which implement its behavior. A particular object's behavior is a mixture of the method definitions of its class and the present state of the object.

    		•
  • Q : Explain VeriSoft VeriSoft (Godefroid,

    VeriSoft (Godefroid, 2005) is a model checker for C and C++; other languages can be used, but components in other languages are treated as black boxes. VeriSoft has been used to find defects in very large telecommunications programs (Chandra, Godefroi

    		•
  • Q : What are the difference between XSLT

    What are the difference between XSLT and XPath?

    		•