Class PosIntervalDomain<Value>
Type Parameters
- Value extends PosIntervalLift = PosIntervalLift
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Hierarchy (View Summary)
- IntervalDomain<Value>
- PosIntervalDomain
Hierarchy-Diagram
Index
Constructors
Properties
Accessors
Methods
Constructors
constructor
- new PosIntervalDomain<Value extends PosIntervalLift = PosIntervalLift>(
value: Value,
): PosIntervalDomain<Value>Type Parameters
- Value extends PosIntervalLift = PosIntervalLift
Type of the constraint in the abstract domain (Top, Bottom, or an actual value)
Parameters
- value: Value
Returns PosIntervalDomain<Value>
- Value extends PosIntervalLift = PosIntervalLift
Accessors
lower
Returns IntervalBound<Value>
upper
Returns IntervalBound<Value>
value
The current abstract value of the lattice.
Returns Lift
Methods
Staticbottom
Returns PosIntervalDomain<typeof Bottom>
Staticfrom
Parameters
- ...values: number[]
Returns IntervalDomain
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 must not be empty or a default value must be provided!
Type Parameters
- Domain extends AnyAbstractDomain
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 must not be empty or a default value must be provided!
Type Parameters
- Domain extends AnyAbstractDomain
Returns Domain
Statictop
Returns PosIntervalDomain<PosIntervalValue>
Staticto
Converts an element of an abstract domain into a string.
Parameters
- this: void
- value: unknown
Returns string
add
Adds an numeric abstract value to this numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | IntervalLift
Returns this
bottom
Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).
Returns PosIntervalDomain<Value> & IntervalDomain<typeof Bottom>
create
Creates an abstract value of the lattice for a given value.
Parameters
- value: PosIntervalLift
Returns this
divide
Divides this numeric abstract value by another numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | IntervalLift
Returns this
equals
Checks whether the current abstract value equals to another abstract value.
Parameters
- other: this
Returns boolean
Protectedequals
Parameters
- this: IntervalDomain<IntervalValue>
- other: IntervalDomain<IntervalValue>
Returns boolean
from
Abstracts a list of concrete values into an abstract value of the value abstract domain.
Parameters
- ...values: number[]
Returns this
is
Checks whether the current abstract value is the Bottom element of the complete lattice.
Returns this is PosIntervalDomain<Value> & IntervalDomain<typeof Bottom>
is
Returns this is PosIntervalDomain<Value> & IntervalDomain<IntervalValue>
is
- isNotBottom(): this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
IntervalValue,
>Returns this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
IntervalValue,
>
is
- isNotTop(): this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
typeof Bottom
| IntervalValue,
>Returns this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
typeof Bottom
| IntervalValue,
>
is
- isNotValue(): this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
typeof Bottom
| IntervalValue,
>Returns this is PosIntervalDomain<Value> & AbstractDomain<
IntervalValue,
IntervalValue,
typeof Bottom,
typeof Bottom
| IntervalValue,
>
is
Checks whether the current abstract value is the Top element of the complete lattice.
Returns this is PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>
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 PosIntervalDomain<Value> & IntervalDomain<IntervalValue>
join
Joins the current abstract value with another abstract value by creating the least upper bound (LUB) in the lattice.
Parameters
- other: typeof Bottom | PosIntervalDomain<Value> | IntervalValue
Returns this
join
Joins the current abstract value with multiple other abstract values.
Parameters
- values: readonly PosIntervalDomain<Value>[]
Returns this
Protectedjoin
- joinValue(
this: PosIntervalDomain<Value> & IntervalDomain<IntervalValue>,
other: IntervalDomain<IntervalValue>,
): thisParameters
- this: PosIntervalDomain<Value> & IntervalDomain<IntervalValue>
- other: IntervalDomain<IntervalValue>
Returns this
Protectedjsonify
Returns unknown
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
Protectedleq
Parameters
- this: IntervalDomain<IntervalValue>
- other: IntervalDomain<IntervalValue>
Returns boolean
max
Gets the maximum of this numeric abstract value and another numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | IntervalLift
Returns this
meet
Meets the current abstract value with another abstract value by creating the greatest lower bound (GLB) in the lattice.
Parameters
- other: typeof Bottom | PosIntervalDomain<Value> | IntervalValue
Returns this
meet
Meets the current abstract value with multiple other abstract values.
Parameters
- values: readonly PosIntervalDomain<Value>[]
Returns this
Protectedmeet
- meetValue(
this: PosIntervalDomain<Value> & IntervalDomain<IntervalValue>,
other: IntervalDomain<IntervalValue>,
): thisParameters
- this: PosIntervalDomain<Value> & IntervalDomain<IntervalValue>
- other: IntervalDomain<IntervalValue>
Returns this
merge
- merge(
other: this,
merge: (
first: IntervalValue,
second: IntervalValue,
) => typeof Bottom | IntervalValue,
bottomDefault: (
other: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue,
topDefault: (
other: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue,
): thisParameters
- other: this
- merge: (first: IntervalValue, second: IntervalValue) => typeof Bottom | IntervalValue
- bottomDefault: (other: typeof Bottom | IntervalValue) => typeof Bottom | IntervalValue
- topDefault: (other: typeof Bottom | IntervalValue) => typeof Bottom | IntervalValue
Returns this
- merge(
other: this,
merge: (
first: IntervalValue,
second: IntervalValue,
) => typeof Bottom | IntervalValue,
bottomDefault: (
other: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue,
): thisParameters
- other: this
- merge: (first: IntervalValue, second: IntervalValue) => typeof Bottom | IntervalValue
- bottomDefault: (other: typeof Bottom | IntervalValue) => typeof Bottom | IntervalValue
Returns this
- merge(
other: this,
merge: (
first: typeof Bottom | IntervalValue,
second: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue,
): thisParameters
- other: this
- merge: (
first: typeof Bottom | IntervalValue,
second: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue
Returns this
min
Gets the minimum of this numeric abstract value and another numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | IntervalLift
Returns this
multiply
Multiplies this numeric abstract value with another numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | IntervalLift
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
Protectednarrow
- narrowValue(
this: PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>,
other: PosIntervalDomain<PosIntervalValue>,
): thisParameters
- this: PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>
- other: PosIntervalDomain<PosIntervalValue>
Returns this
negate
Negates this numeric abstract value.
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
Protectedstringify
Parameters
- this: IntervalDomain<IntervalValue>
Returns string
subtract
Subtracts an numeric abstract value from this numeric abstract value.
Parameters
- other: PosIntervalDomain<Value> | PosIntervalLift
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 PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>
to
Converts the lattice into a human-readable string.
Returns string
transform
- transform(
transform: (value: IntervalValue) => typeof Bottom | IntervalValue,
bottomDefault: typeof Bottom | IntervalValue,
topDefault: typeof Bottom | IntervalValue,
): thisParameters
- transform: (value: IntervalValue) => typeof Bottom | IntervalValue
- bottomDefault: typeof Bottom | IntervalValue
- topDefault: typeof Bottom | IntervalValue
Returns this
- transform(
transform: (value: IntervalValue) => typeof Bottom | IntervalValue,
bottomDefault: typeof Bottom | IntervalValue,
): thisParameters
- transform: (value: IntervalValue) => typeof Bottom | IntervalValue
- bottomDefault: typeof Bottom | IntervalValue
Returns this
- transform(
transform: (
value: typeof Bottom | IntervalValue,
) => typeof Bottom | IntervalValue,
): thisParameters
- transform: (value: typeof Bottom | IntervalValue) => typeof Bottom | IntervalValue
Returns this
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
widen
Extends the lower bound of the current abstract value down to 0.
Returns this
widen
Extends the upper bound of the current abstract value up to +∞.
Returns this
Protectedwiden
- widenValue(
this: PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>,
other: PosIntervalDomain<PosIntervalValue>,
): thisParameters
- this: PosIntervalDomain<Value> & PosIntervalDomain<PosIntervalValue>
- other: PosIntervalDomain<PosIntervalValue>
Returns this
The positive interval abstract domain as positive intervals with possibly zero lower bounds and infinite upper bounds representing possible numeric values. The Bottom element is defined as Bottom symbol and the Top element is defined as the interval [0, +∞].