--%>

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 : Explain the relationship between XHTML

    Explain the relationship between XHTML and SGML.

  • Q : UK assignment & homework help Need UK

    Need UK Assignment Help, UK Homework Help. Get it now! HwA provides email based and live UK assignment help and UK homework help in a variety of subjects to the students based out

  • Q : Explain Edit-compile-run cycle

    Edit-compile-run cycle: A common portion of the program development procedure. The source file is made initially and compiled. The syntax errors should be corrected in the editor before compiling it again. Once the program has been productively compil

  • Q : Describe Timers Timers: While time

    Timers: While time values usually cannot be reduced in the target system, their usage can be encapsulated as an abstraction which can be replaced easily (e.g., by a non-deterministic choice) during model checking.

  • Q : XPATH selector Normal 0 false false

    Normal 0 false false

  • Q : Uses of BYTE Write a program that shows

    Write a program that shows the uses of BYTE, WORD and DWORD?

  • Q : What are the tools require writing

    What are the tools require writing XHTML documents?

  • Q : BAT files and shell scripts Using the

    Using the Web as a resource for your investigation, find out and explain what BAT files and shell scripts contain, and what they are used for. In the light of your findings, discuss why an operating system would provide both a graphical user interface

  • Q : Use of setjmp and longjmp Use of

    Use of setjmp() and longjmp(): In C/C++, setjmp() saves the contents of the registers at a particular state in the program and longjmp() will restore that state later. In this way, longjmp() “returns” to the state of the program when setjm

  • Q : What is Bounded repetition Bounded

    Bounded repetition: The Repetition where statements within a loop's body are executed a fixed number of times and the number of times is established whenever the loop began. There is no control structure in Java which guarantees the bounded repetition