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.

View Complete Question

Related Questions in Programming Languages

Q : Write a program and estimate pi using

Consider a dartboard of radius 1. Since the area of the board will be π r2 = π * 1 *1, it's clear the area of the dartboard is exactly π. The area of a square surrounding the board (circumscribing it) would be 2*2 = 4, sin

Q : How can Corba application has call back

Describe how can Corba application has call back?

Q : Define Interpretational inner class

Interpretational inner class: It is an inner class whose role is to give a view or interpretation of data belongs to its enclosing class, however independent of the data's real representation.

Q : Define the term Interface inheritance

Interface inheritance: Whenever a class implements an interface, the interface inheritance relationship exists among them. The class inherits no implementation from interface, just method signatures and static variables. It is as well possible for one

Q : Explain Right shift operator Right

Right shift operator: Right shift operator (>>) is the bit manipulation operator. It shifts the bits in its left operand zero (0) or many places to the right, according to the value of its accurate operand. The most important bit from before the

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 : Explain Decrement operator Decrement

Decrement operator: It is an operator (--) which adds one to its operand. This has two forms: pre-decrement (--x) and post-decrement (x--). In its pre-decrement form, the outcome of the expression is the value of its argument subsequent to the decreme

Discover Q & A

Leading Solution Library

Avail More Than 1436900 Solved problems, classrooms assignments, textbook's solutions, for quick Downloads

No hassle, Instant Access

Start Discovering

18,76,764

1958879
Asked

3,689

Active Tutors

1436900

Questions
Answered

Start Excelling in your courses, Ask an Expert and get answers for your homework and assignments!!

Submit Assignment