4.9.3 Domain

4.9.3.1 Description

A constant from a finite domain of constants.

4.9.3.2 Top value

flat_top (undefined)

4.9.3.3 Bottom value

flat_bot (undefined)

4.9.3.4 Greatest lower bound operation

The greatest lower bound of two values A and B yields:

• B if A is top
• A if B is top
• A if A and B are equal
• bottom otherwise

4.9.3.5 Example

Here is an example domain type definition including the constants constant_1, constant_2 and constant_3:

     deftype "domain" {constant_1 constant_2 constant_3}