--%>

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 : Define the term Module Module : It is a

    Module: It is a group of program components, usually with restricted visibility to program components in other modules. Java employs packages to implement this perception.

  • Q : Define Finite State Machines Finite

    Finite State Machines : A Finite State Machine (FSM) is one of the most suitable models for formal checks, especially for concurrent systems. However, FSMs can have problems with inheritance (the state model can change in derived classes) if state asp

  • Q : Define the Binding of Instructions and

    Define the Binding of Instructions and Data to Memory?

  • Q : What is Actual argument Actual argument

    Actual argument: The value of an argument enacted to a method from exterior to the method. Whenever a method is called, the real argument values are copied into analogous formal arguments. The kinds of the actual arguments should be compatible with th

  • Q : What is Cursor Cursor : This is a

    Cursor: This is a visual representation of the existing position of the mouse on the user's virtual desktop. Cursor shapes are frequently set to symbolize the current state of a program – utilizing an hour glass shape to point out that the user

  • Q : Explain main quality of unsuitable life

    What are the main quality consequences of selecting an unsuitable life cycle model for a software project?

  • Q : What is Left shift operator Left shift

    Left shift operator: Left shift operator (<<) is the bit manipulation operator. This moves the bits in its left operand zero or additional positions to the left, according to the value of its right operand. The zero bits are added up to the righ

  • Q : Explain the important thing to HTML

    Explain the important thing to HTML document authors.

  • Q : What is SLAM SLAM is a Microsoft

    SLAM is a Microsoft project that blurs the line between static analysis and model checking and deductive reasoning. The main goal of SLAM is to check temporal safety properties of C programs (it actually checks that a program correctly uses the interf

  • Q : Write a program to print out ten random

    Write a program to print out ten random numbers from the following sets: a) {0, 1, 2, 3, 4, 5, ...99, 100} b) {1, 2, 3, 4, 5, 6} c) (10, 20, 30, 40, 50,...990, 1000} d) {-5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5} e) {1.5, 2.0, 2.5, 3.0, 3.5}