--%>

Abstract list domain

The abstract list domain is as shown: {empty, some, [d1], [d2],[ d1, d2], [d2, d1], all}.

A) empty represents empty lists.

B) some represents lists with only other values.

C) [d1] represents lists that contain d1 mixed with zero or more other values.

D) [d2] represents lists that contain d2 mixed with zero or more other values.

E) [d1, d2] represents lists that contain d1 and d2 in this order, plus zero or more other values.

F) [d2, d1] represents lists that contain d2 and d1 in this order, plus zero or more other values.

G) all represents lists that contain multiple d1 and d2 elements.

Using this abstraction, you can check ordering properties—for example, that if d1 and d2are inserted in this order in a list, and then they are removed, they are removed in the same order. Similar abstractions have been used for checking ordering properties of protocols and memories.

   Related Questions in Programming Languages

  • Q : Advantage of wrapping database calls in

    What is the advantage of wrapping database calls in MTS transactions?

  • Q : Modeling Language for SPIN-Promela

    Modeling Language: The modeling language used for SPIN is called Promela (Process Meta Language). In fact, the name SPIN stands for Simple Promela Interpreter. Promela is a powerful C-like specification language with a variety of synchronization primi

  • Q : Business Process Management Describe

    Describe what is Business Process Management (or BPM) in brief.

  • Q : Describe Data type Data type : It is a

    Data type: It is a specifier to build memory block of some particular size and kind. C++ provides two kinds of data types: A) Fundamental type: That is not composed

  • Q : Define Implements clause Implements

    Implements clause: That part of a class header which points out which interfaces are applied by the class. A class might implement for more than one interface.

  • Q : Explain If-else statement If-else

    If-else statement: It is a control structure employed to select between performing one of two alternative events.     if(boolean-expression){        // Statem

  • Q : Explain Java Virtual Machine Java

    Java Virtual Machine (JVM): It is an idealized machine whose instruction set comprises of bytecodes. Java program is compiled to an equal bytecode form and performed on an interpreter that implements the JVM.

  • Q : What is an Anonymous array Anonymous

    Anonymous array: It is an array formed without an identifier. The anonymous array is generally formed as an actual argument, for example:// generate an anonymous array of integers.    YearlyRainfall y2k = new YearlyRai

  • Q : Define Deprecated Deprecated : Somewhat

    Deprecated: Somewhat that has been made superseded by later on versions of the API. Deprecated methods must not be employed as there is no guarantee that they will carry on to subsist in the future versions.

  • Q : Define Compiler Compiler : A program

    Compiler: A program that executes a process of compilation on a program written in the high level programming language.