Abstract list domain

Question

The abstract list domain is as shown: {empty, some, [d₁], [d₂],[ d₁, d₂], [d₂, d₁], all}.

A) empty represents empty lists.

B) some represents lists with only other values.

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

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

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

F) [d₂, d₁] 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 d₁ and d₂are 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.