Class AbstractDomain<Concrete, Abstract, Top, Bot, Value>`Abstract`

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

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 (excludes Top and Bot)
Top
Type of the Top element of the abstract domain representing all possible elements
Bot
Type of the Bottom element of the abstract domain representing no possible elements
Value 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)

AbstractDomain

Implements

Lattice<Abstract, Top, Bot, Value>

Hierarchy-Diagram

Index

Constructors

constructor

new AbstractDomain<Concrete, Abstract, Top, Bot, Value = Abstract | Top | Bot>(
value: Value,
): AbstractDomain<Concrete, Abstract, Top, Bot, Value>
Type Parameters
- Concrete
- Abstract
- Top
- Bot
- Value = Abstract | Top | Bot
Parameters
- value: Value
Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:22

Properties

`Protected` `Readonly`_value

_value: Value

Accessors

value

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

Returns Value
Implementation of Lattice.value
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:26

Methods

`Static`joinAll

joinAll<Domain extends AnyAbstractDomain>(values: Domain[]): Domain
Joins an array of abstract values by joining the first abstract value with the other values in the array. The provided array of abstract values cannot be empty!
Type Parameters
- Domain extends AnyAbstractDomain
Parameters
- values: Domain[]
Returns Domain
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:103

`Static`meetAll

meetAll<Domain extends AnyAbstractDomain>(values: Domain[]): Domain
Meets an array of abstract values by meeting the first abstract value with the other values in the array. The provided array of abstract values cannot be empty!
Type Parameters
- Domain extends AnyAbstractDomain
Parameters
- values: Domain[]
Returns Domain
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:112

`Abstract`abstract

abstract(concrete: typeof Top | ReadonlySet<Concrete>): this
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 this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:87

`Abstract`bottom

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

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain<
    Concrete,
    Abstract,
    Top,
    Bot,
    Bot,
>
Implementation of Lattice.bottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:34

`Abstract`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
- limit: number
Returns typeof Top | ReadonlySet<Concrete>
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:82

`Abstract`create

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

`Abstract`equals

equals(other: this): boolean
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
Implementation of Lattice.equals
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:36

`Abstract`isBottom

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

Returns this is AbstractDomain<Concrete, Abstract, Top, Bot, Bot>
Implementation of Lattice.isBottom
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:95

`Abstract`isTop

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

Returns this is AbstractDomain<Concrete, Abstract, Top, Bot, Top>
Implementation of Lattice.isTop
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:93

`Abstract`isValue

isValue(): this is AbstractDomain<Concrete, 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 AbstractDomain<Concrete, Abstract, Top, Bot, Abstract>
Implementation of Lattice.isValue
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:97

`Abstract`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
Implementation of Lattice.join
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:40

joinAll

joinAll(
values: readonly AbstractDomain<Concrete, Abstract, Top, Bot, Value>[],
): this
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly AbstractDomain<Concrete, Abstract, Top, Bot, Value>[]
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:45

`Abstract`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
Implementation of Lattice.leq
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:38

`Abstract`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
Implementation of Lattice.meet
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:54

meetAll

meetAll(
values: readonly AbstractDomain<Concrete, Abstract, Top, Bot, Value>[],
): this
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly AbstractDomain<Concrete, Abstract, Top, Bot, Value>[]
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:59

`Abstract`narrow

narrow(other: this): this
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: this
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:76

`Abstract`toJson

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

Returns unknown
Implementation of Lattice.toJson
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:89

`Abstract`top

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

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain<
    Concrete,
    Abstract,
    Top,
    Bot,
    Top,
>
Implementation of Lattice.top
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:32

`Abstract`toString

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

Returns string
Implementation of Lattice.toString
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:91

`Abstract`widen

widen(other: this): this
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: this
Returns this
- Defined in src/abstract-interpretation/domains/abstract-domain.ts:71

Class AbstractDomain<Concrete, Abstract, Top, Bot, Value>Abstract

Type Parameters

Hierarchy (View Summary)

Implements

Hierarchy-Diagram

Index

Constructors

Properties

Accessors

Methods

Constructors

constructor

Type Parameters

Parameters

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value>

Properties

Protected Readonly_value

Accessors

value

Returns Value

Methods

StaticjoinAll

Type Parameters

Parameters

Returns Domain

StaticmeetAll

Type Parameters

Parameters

Returns Domain

Abstractabstract

Parameters

Returns this

Abstractbottom

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain< Concrete, Abstract, Top, Bot, Bot,>

Abstractconcretize

Parameters

Returns typeof Top | ReadonlySet<Concrete>

Abstractcreate

Parameters

Returns this

Abstractequals

Parameters

Returns boolean

AbstractisBottom

Returns this is AbstractDomain<Concrete, Abstract, Top, Bot, Bot>

AbstractisTop

Returns this is AbstractDomain<Concrete, Abstract, Top, Bot, Top>

AbstractisValue

Returns this is AbstractDomain<Concrete, Abstract, Top, Bot, Abstract>

Abstractjoin

Parameters

Returns this

joinAll

Parameters

Returns this

Abstractleq

Parameters

Returns boolean

Abstractmeet

Parameters

Returns this

meetAll

Parameters

Returns this

Abstractnarrow

Parameters

Returns this

AbstracttoJson

Returns unknown

Abstracttop

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain< Concrete, Abstract, Top, Bot, Top,>

AbstracttoString

Returns string

Abstractwiden

Parameters

Returns this

Settings

On This Page

Class AbstractDomain<Concrete, Abstract, Top, Bot, Value>`Abstract`

`Protected` `Readonly`_value

`Static`joinAll

`Static`meetAll

`Abstract`abstract

`Abstract`bottom

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain<
Concrete,
Abstract,
Top,
Bot,
Bot,
>

`Abstract`concretize

`Abstract`create

`Abstract`equals

`Abstract`isBottom

`Abstract`isTop

`Abstract`isValue

`Abstract`join

`Abstract`leq

`Abstract`meet

`Abstract`narrow

`Abstract`toJson

`Abstract`top

Returns AbstractDomain<Concrete, Abstract, Top, Bot, Value> & AbstractDomain<
Concrete,
Abstract,
Top,
Bot,
Top,
>

`Abstract`toString

`Abstract`widen