Interface Lattice<Value, Top, Bot, Lift>

A complete lattice with a partially ordered set, join operator (LUB), meet operator (GLB), top element, and bottom element (e.g. for abstract domains).

interface Lattice<
    Value,
    Top,
    Bot,
    Lift extends Value | Top | Bot = Value | Top | Bot,
> {
    bottom(): Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Bot>;
    create(value: Value | Top | Bot): this;
    equals(other: this): boolean;
    isBottom(): this is Lattice<Value, Top, Bot, Bot>;
    isTop(): this is Lattice<Value, Top, Bot, Top>;
    isValue(): this is Lattice<Value, Top, Bot, Value>;
    join(other: this): this;
    leq(other: this): boolean;
    meet(other: this): this;
    toJson(): unknown;
    top(): Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Top>;
    toString(): string;
    get value(): Lift;
}

Type Parameters

Value
Type of a lattice element representing a value (may exclude Top and Bot)
Top
Type of the Top element (greatest element) of the complete lattice
Bot
Type of the Bottom element (least element) of the complete lattice
Lift extends Value | Top | Bot = Value | Top | Bot
Type of the lattice elements (defaults to Value or Top or Bot)

Implemented by

AbstractDomain

Index

Accessors

value

Methods

bottom create equals isBottom isTop isValue join leq meet toJson top toString

Accessors

value

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

Returns Lift
- Defined in src/abstract-interpretation/domains/lattice.ts:22

Methods

bottom

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

Returns Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Bot>
- Defined in src/abstract-interpretation/domains/lattice.ts:37

create

create(value: Value | Top | Bot): this
Creates an abstract value of the lattice for a given value.
Parameters
- value: Value | Top | Bot
Returns this
- Defined in src/abstract-interpretation/domains/lattice.ts:27

equals

equals(other: this): boolean
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
- Defined in src/abstract-interpretation/domains/lattice.ts:42

isBottom

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

Returns this is Lattice<Value, Top, Bot, Bot>
- Defined in src/abstract-interpretation/domains/lattice.ts:77

isTop

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

Returns this is Lattice<Value, Top, Bot, Top>
- Defined in src/abstract-interpretation/domains/lattice.ts:72

isValue

isValue(): this is Lattice<Value, Top, Bot, Value>
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<Value, Top, Bot, Value>
- Defined in src/abstract-interpretation/domains/lattice.ts:83

join

join(other: this): this
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other: this
Returns this
- Defined in src/abstract-interpretation/domains/lattice.ts:52

leq

leq(other: this): 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: this
Returns boolean
- Defined in src/abstract-interpretation/domains/lattice.ts:47

meet

meet(other: this): this
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: this
Returns this
- Defined in src/abstract-interpretation/domains/lattice.ts:57

toJson

toJson(): unknown
Converts the lattice into a JSON serializable value.

Returns unknown
- Defined in src/abstract-interpretation/domains/lattice.ts:62

top

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

Returns Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Top>
- Defined in src/abstract-interpretation/domains/lattice.ts:32

toString

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

Returns string
- Defined in src/abstract-interpretation/domains/lattice.ts:67

Interface Lattice<Value, Top, Bot, Lift>

Type Parameters

Implemented by

Index

Accessors

Methods

Accessors

value

Returns Lift

Methods

bottom

Returns Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Bot>

create

Parameters

Returns this

equals

Parameters

Returns boolean

isBottom

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

isTop

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

isValue

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

join

Parameters

Returns this

leq

Parameters

Returns boolean

meet

Parameters

Returns this

toJson

Returns unknown

top

Returns Lattice<Value, Top, Bot, Lift> & Lattice<Value, Top, Bot, Top>

toString

Returns string

Settings

On This Page