Interface AbstractDomain<Concrete, Abstract, Top, Bot, Lift>

An abstract domain as complete lattice with a widening operator, narrowing operator, concretization function, and abstraction function.

interface AbstractDomain<
    Concrete,
    Abstract,
    Top = typeof Top,
    Bot = typeof Bottom,
    Lift extends Abstract | Top | Bot = Abstract | Top | Bot,
> {
    abstract(
        concrete: typeof Top | ReadonlySet<Concrete>,
    ): AbstractDomain<Concrete, Abstract, Top, Bot>;
    bottom(): Lattice<Abstract, Top, Bot, Bot>;
    concretize(limit?: number): typeof Top | ReadonlySet<Concrete>;
    equals(other: Lattice<Abstract, Top, Bot>): boolean;
    isBottom(): this is Lattice<Abstract, Top, Bot, Bot>;
    isTop(): this is Lattice<Abstract, Top, Bot, Top>;
    isValue(): this is Lattice<Abstract, Top, Bot, Abstract>;
    join(
        ...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[],
    ): Lattice<Abstract, Top, Bot>;
    leq(other: Lattice<Abstract, Top, Bot>): boolean;
    meet(
        ...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[],
    ): Lattice<Abstract, Top, Bot>;
    narrow(
        other: AbstractDomain<Concrete, Abstract, Top, Bot>,
    ): AbstractDomain<Concrete, Abstract, Top, Bot>;
    top(): Lattice<Abstract, Top, Bot, Top>;
    toString(): string;
    get value(): Lift;
    widen(
        other: AbstractDomain<Concrete, Abstract, Top, Bot>,
    ): AbstractDomain<Concrete, Abstract, Top, Bot>;
}

Type Parameters

Concrete
Type of an concrete element of the concrete domain for the abstract domain
Abstract
Type of an abstract element of the abstract domain representing possible elements (may exclude Top and Bot)
Top = typeof Top
Type of the Top element of the abstract domain representing all possible elements (defaults to Top)
Bot = typeof Bottom
Type of the Bottom element of the abstract domain representing no possible elements (defaults to Bottom)
Lift extends Abstract | Top | Bot = Abstract | Top | Bot
Type of the abstract elements of the abstract domain (defaults to Abstract or Top or Bot)

Hierarchy (View Summary)

Lattice<Abstract, Top, Bot, Lift>
- AbstractDomain

Implemented by

Hierarchy-Diagram

Index

Accessors

value

Methods

abstract bottom concretize equals isBottom isTop isValue join leq meet narrow top toString widen

Accessors

value

get value(): Lift
The current abstract value of the lattice.

Returns Lift
Inherited from Lattice.value
- Defined in src/abstract-interpretation/domains/lattice.ts:22

Methods

abstract

abstract(
concrete: typeof Top | ReadonlySet<Concrete>,
): AbstractDomain<Concrete, Abstract, Top, Bot>
Maps a set of possible concrete values into an abstract value as abstraction function of the abstract domain (should additionally be provided as static function).
Parameters
- concrete: typeof Top | ReadonlySet<Concrete>
Returns AbstractDomain<Concrete, Abstract, Top, Bot>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:37

bottom

bottom(): Lattice<Abstract, Top, Bot, Bot>
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

Returns Lattice<Abstract, Top, Bot, Bot>
Inherited from Lattice.bottom
- Defined in src/abstract-interpretation/domains/lattice.ts:32

concretize

concretize(limit?: number): typeof Top | ReadonlySet<Concrete>
Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain. The result should be Top if the number of concrete values would reach the limit or the resulting set would have infinite many elements.
Parameters
- Optionallimit: number
Returns typeof Top | ReadonlySet<Concrete>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:32

equals

equals(other: Lattice<Abstract, Top, Bot>): boolean
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: Lattice<Abstract, Top, Bot>
Returns boolean
Inherited from Lattice.equals
- Defined in src/abstract-interpretation/domains/lattice.ts:37

isBottom

isBottom(): this is Lattice<Abstract, Top, Bot, Bot>
Checks whether the current abstract value is the Bottom element of the complete lattice.

Returns this is Lattice<Abstract, Top, Bot, Bot>
Inherited from Lattice.isBottom
- Defined in src/abstract-interpretation/domains/lattice.ts:67

isTop

isTop(): this is Lattice<Abstract, Top, Bot, Top>
Checks whether the current abstract value is the Top element of the complete lattice.

Returns this is Lattice<Abstract, Top, Bot, Top>
Inherited from Lattice.isTop
- Defined in src/abstract-interpretation/domains/lattice.ts:62

isValue

isValue(): this is Lattice<Abstract, Top, Bot, Abstract>
Checks whether the current abstract value is an actual value of the complete lattice (this may include the Top or Bottom element if they are also values and no separate symbols, for example).

Returns this is Lattice<Abstract, Top, Bot, Abstract>
Inherited from Lattice.isValue
- Defined in src/abstract-interpretation/domains/lattice.ts:73

join

join(
...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[],
): Lattice<Abstract, Top, Bot>
Joins the current abstract value with other abstract values by creating the least upper bound (LUB) in the lattice.
Parameters
- ...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[]
Returns Lattice<Abstract, Top, Bot>
Inherited from Lattice.join
- Defined in src/abstract-interpretation/domains/lattice.ts:47

leq

leq(other: Lattice<Abstract, Top, Bot>): boolean
Checks whether the current abstract value is less than or equal to another abstract value with respect to the partial order of the lattice.
Parameters
- other: Lattice<Abstract, Top, Bot>
Returns boolean
Inherited from Lattice.leq
- Defined in src/abstract-interpretation/domains/lattice.ts:42

meet

meet(
...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[],
): Lattice<Abstract, Top, Bot>
Meets the current abstract value with other abstract values by creating the greatest lower bound (GLB) in the lattice.
Parameters
- ...values: Lattice<Abstract, Top, Bot, Abstract | Top | Bot>[]
Returns Lattice<Abstract, Top, Bot>
Inherited from Lattice.meet
- Defined in src/abstract-interpretation/domains/lattice.ts:52

narrow

narrow(
other: AbstractDomain<Concrete, Abstract, Top, Bot>,
): AbstractDomain<Concrete, Abstract, Top, Bot>
Narrows the current abstract value with another abstract value as a sound over-approximation of the meet (greatest lower bound) to refine the value after widening.
Parameters
- other: AbstractDomain<Concrete, Abstract, Top, Bot>
Returns AbstractDomain<Concrete, Abstract, Top, Bot>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:26

top

top(): Lattice<Abstract, Top, Bot, Top>
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).

Returns Lattice<Abstract, Top, Bot, Top>
Inherited from Lattice.top
- Defined in src/abstract-interpretation/domains/lattice.ts:27

toString

toString(): string
Converts the lattice into a human-readable string.

Returns string
Inherited from Lattice.toString
- Defined in src/abstract-interpretation/domains/lattice.ts:57

widen

widen(
other: AbstractDomain<Concrete, Abstract, Top, Bot>,
): AbstractDomain<Concrete, Abstract, Top, Bot>
Widens the current abstract value with another abstract value as a sound over-approximation of the join (least upper bound) for fixpoint iteration acceleration.
Parameters
- other: AbstractDomain<Concrete, Abstract, Top, Bot>
Returns AbstractDomain<Concrete, Abstract, Top, Bot>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:21

Interface AbstractDomain<Concrete, Abstract, Top, Bot, Lift>

Type Parameters

Hierarchy (View Summary)

Implemented by

Hierarchy-Diagram

Index

Accessors

Methods

Accessors

value

Returns Lift

Methods

abstract

Parameters

Returns AbstractDomain<Concrete, Abstract, Top, Bot>

bottom

Returns Lattice<Abstract, Top, Bot, Bot>

concretize

Parameters

Returns typeof Top | ReadonlySet<Concrete>

equals

Parameters

Returns boolean

isBottom

Returns this is Lattice<Abstract, Top, Bot, Bot>

isTop

Returns this is Lattice<Abstract, Top, Bot, Top>

isValue

Returns this is Lattice<Abstract, Top, Bot, Abstract>

join

Parameters

Returns Lattice<Abstract, Top, Bot>

leq

Parameters

Returns boolean

meet

Parameters

Returns Lattice<Abstract, Top, Bot>

narrow

Parameters

Returns AbstractDomain<Concrete, Abstract, Top, Bot>

top

Returns Lattice<Abstract, Top, Bot, Top>

toString

Returns string

widen

Parameters

Returns AbstractDomain<Concrete, Abstract, Top, Bot>

Settings

On This Page