Class IntervalDomain<Value>
Type Parameters
- Value extends IntervalLift = IntervalLift
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Hierarchy (View Summary)
- AbstractDomain<number, IntervalValue, IntervalTop, IntervalBottom, Value>
- IntervalDomain
Implements
- SatisfiableDomain<number>
Hierarchy-Diagram
Constructors
constructor
- new IntervalDomain<Value extends IntervalLift = IntervalLift>(
value: Value,
): IntervalDomain<Value>Type Parameters
- Value extends IntervalLift = IntervalLift
Parameters
- value: Value
Returns IntervalDomain<Value>
Methods
Staticabstract
Parameters
- concrete: typeof Top | ReadonlySet<number>
Returns IntervalDomain
Staticbottom
Returns IntervalDomain<typeof Bottom>
Staticjoin
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
Staticmeet
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
Statictop
Returns IntervalDomain<IntervalValue>
abstract
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<number>
Returns this
add
Adds another abstract value to the current abstract value by adding the two lower and upper bounds, respectively.
Parameters
- other: IntervalLift | IntervalDomain<Value>
Returns this
bottom
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
Returns IntervalDomain<Value> & IntervalDomain<typeof Bottom>
concretize
Maps the current abstract value into a set of possible concrete values as concretization function of the abstract domain. The result should be
Topif the number of concrete values would reach thelimitor the resulting set would have infinite many elements.Parameters
- limit: number
Returns typeof Top | ReadonlySet<number>
create
Creates an abstract value of the lattice for a given value.
Parameters
- value: IntervalLift
Returns this
equals
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
extend
Extends the lower bound of the current abstract value down to -∞.
Returns this
extend
Extends the upper bound of the current abstract value up to +∞.
Returns this
is
Checks whether the current abstract value is the Bottom element of the complete lattice.
Returns this is IntervalDomain<typeof Bottom>
is
Checks whether the current abstract value is the Top element of the complete lattice.
Returns this is IntervalDomain<IntervalValue>
is
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 IntervalDomain<IntervalValue>
join
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other: this
Returns this
Parameters
- other: IntervalLift
Returns this
join
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly IntervalDomain<Value>[]
Returns this
leq
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
max
Creates the maximum between the current abstract value and another abstract value by creating the maximum of the two lower and upper bounds, respectively.
Parameters
- other: IntervalLift | IntervalDomain<Value>
Returns this
meet
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: this
Returns this
Parameters
- other: IntervalLift
Returns this
meet
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly IntervalDomain<Value>[]
Returns this
min
Creates the minimum between the current abstract value and another abstract value by creating the minimum of the two lower and upper bounds, respectively.
Parameters
- other: IntervalLift | IntervalDomain<Value>
Returns this
narrow
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
satisfies
Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value).
Parameters
- value: number
- comparator: NumericalComparator = NumericalComparator.Equal
Returns Ternary
See
Ternary for the returned satisfiability result
subtract
Subtracts another abstract value from the current abstract value by subtracting the two lower and upper bounds from each other, respectively.
Parameters
- other: IntervalLift | IntervalDomain<Value>
Returns this
to
Converts the lattice into a JSON serializable value.
Returns unknown
top
Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).
Returns IntervalDomain<Value> & IntervalDomain<IntervalValue>
to
Converts the lattice into a human-readable string.
Returns string
widen
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
The interval abstract domain as intervals with possibly infinite bounds representing possible numeric values. The Bottom element is defined as Bottom symbol and the Top element is defined as the interval [-∞, +∞].