--%>

Explain Primitive Type Abstractions

Primitive Type Abstractions: An effective way to reduce the state space of a program is to replace the primitive types with the corresponding abstractions that encapsulate all the possible operations that are performed on these types.

These abstractions allow us to replace the actual primitive variables or the operations involving those with the non-deterministic choices with restricted range of values. This can cut down the number of states that has to be covered by the model checker dramatically.

As an example, consider the following class which encapsulates different operations that can be carried out on doubles.

964_primitive abs1.jpg

Here is the implementation for the operator==() which implements the real behavior of the operator:

2156_primitive abs2.jpg

With this abstraction it would be easy to reduce the potentially infinite state space required to model check the equality operator “==” with a binary choice (true or false)—just replace the “m_value == value” with “chooseBoolean()” in the body of the method.

   Related Questions in Programming Languages

  • Q : What is an Import statement Import

    Import statement: A statement which makes the names of one or more interfaces or classes accessible in a different package from the one in which they are stated. Import statements pursue any package declaration {package!declaration}, and precede any i

  • Q : Define the term Peripheral devices

    Define the term Peripheral devices: It is the devices attached to a computer, like disk drives, printers, mice, and so forth.

  • Q : Describe IEEE 754 IEEE 754 : The

    IEEE 754: The standard 754-1985 issued by Institute of Electrical and Electronic Engineers for the binary floating point arithmetic. It is the standard to which Java's arithmetic matches.

  • Q : Define HyperText Markup Language

    HyperText Markup Language: The HyperText Markup Language (abbreviated as HTML) is a simple presentation language employed to markup the content of the Web pages. Its tags appear frequently in pairs to mark sections of text which must be represented in

  • Q : Explain the computer process Explain

    Explain the computer process.

  • Q : Define Method header Method header : It

    Method header: It is the header of a method, comprising of the method name, its outcome type, formal arguments and any exceptions thrown. Also termed as a method signature.

  • Q : Define the term CPU Scheduler Define

    Define the term CPU Scheduler?

  • Q : What does WSDL stand for What does WSDL

    What does WSDL stand for?

  • Q : Explain Return statement Return

    Return statement: It is a statement employed to terminate the execution of the method. The method with void return type might only have return statements of the form as: return;

  • Q : Explain Try statement Try statement :

    Try statement: The try statement performs as an exception handler - a position where exception objects are caught and dealt with. In its most common form, it comprises of a try clause, one or more catch clauses and the finally clause.