Class SetRangeDomain<T, Value>

constructor

• new SetRangeDomain<T, Value extends SetRangeLift<T> = SetRangeLift<T>>(
      value: Value | ArrayRangeValue<T>,
      limit?: number | SetRangeLimit,
      setType?: typeof Set,
  ): SetRangeDomain<T, Value>

  Type Parameters

  • T
  • Value extends SetRangeLift<T> = SetRangeLift<T>

  Parameters

  • value: Value | ArrayRangeValue<T>
  • limit: number | SetRangeLimit = DefaultLimit

    A limit for the maximum number of elements to store in the minimum set and maximum set before over-approximation
  • setType: typeof Set = Set

  Returns SetRangeDomain<T, Value>

Readonlylimit

Staticabstract

• abstract<T>(
      concrete: typeof Top | ReadonlySet<ReadonlySet<T>>,
      limit?: number | SetRangeLimit,
      setType?: typeof Set,
  ): SetRangeDomain<T>

  Type Parameters

  • T

  Parameters

  • concrete: typeof Top | ReadonlySet<ReadonlySet<T>>
  • Optionallimit: number | SetRangeLimit
  • OptionalsetType: typeof Set

  Returns SetRangeDomain<T>

Staticbottom

• bottom<T>(
      limit?: number | SetRangeLimit,
      setType?: typeof Set,
  ): SetRangeDomain<T, typeof Bottom>

  Type Parameters

  • T

  Parameters

  • Optionallimit: number | SetRangeLimit
  • OptionalsetType: typeof Set

  Returns SetRangeDomain<T, typeof Bottom>

Statictop

• top<T>(
      limit?: number | SetRangeLimit,
      setType?: typeof Set,
  ): SetRangeDomain<T, { min: Set<never>; range: typeof Top }>

  Type Parameters

  • T

  Parameters

  • Optionallimit: number | SetRangeLimit
  • OptionalsetType: typeof Set

  Returns SetRangeDomain<T, { min: Set<never>; range: typeof Top }>

abstract

• abstract(concrete: typeof Top | ReadonlySet<ReadonlySet<T>>): 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<ReadonlySet<T>>

  Returns this

bottom

• bottom(): SetRangeDomain<T, Value> & SetRangeDomain<T, typeof Bottom>

  Gets the Bottom element (least element) of the complete lattice (should additionally be provided as static function).

  Returns SetRangeDomain<T, Value> & SetRangeDomain<T, typeof Bottom>

concretize

• concretize(limit: number): typeof Top | ReadonlySet<ReadonlySet<T>>

  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<ReadonlySet<T>>

create

• create(value: SetRangeLift<T> | ArrayRangeValue<T>): this

  Creates an abstract value of the lattice for a given value.

  Parameters

  • value: SetRangeLift<T> | ArrayRangeValue<T>

  Returns this

equals

• equals(other: this): boolean

  Checks whether the current abstract value equals to another abstract value.

  Parameters

  • other: this

  Returns boolean

intersect

• intersect(
      other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>,
  ): this

  Creates the intersection of this abstract value and another abstract value by creating the intersection of the minimum and maximum set, respectively.

  Parameters

  • other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>

  Returns this

isBottom

• isBottom(): this is SetRangeDomain<T, typeof Bottom>

  Checks whether the current abstract value is the Bottom element of the complete lattice.

  Returns this is SetRangeDomain<T, typeof Bottom>

isTop

• isTop(): this is SetRangeDomain<T, { min: Set<never>; range: typeof Top }>

  Checks whether the current abstract value is the Top element of the complete lattice.

  Returns this is SetRangeDomain<T, { min: Set<never>; range: typeof Top }>

isValue

• isValue(): this is SetRangeDomain<T, SetRangeValue<T>>

  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 SetRangeDomain<T, SetRangeValue<T>>

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
• join(other: SetRangeLift<T> | ArrayRangeValue<T>): this

  Parameters

  • other: SetRangeLift<T> | ArrayRangeValue<T>

  Returns this

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

lower

• lower(): typeof Bottom | ReadonlySet<T>

  The minimum set (lower bound) of the set range representing all values that must exist (subset of upper).

  Returns typeof Bottom | ReadonlySet<T>

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
• meet(other: SetRangeLift<T> | ArrayRangeValue<T>): this

  Parameters

  • other: SetRangeLift<T> | ArrayRangeValue<T>

  Returns this

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

satisfies

• satisfies(set: ReadonlySet<T> | T[], comparator?: SetComparator): Ternary

  Checks whether the current abstract value satisfies a concrete value (i.e. includes a concrete value).

  Parameters

  • set: ReadonlySet<T> | T[]
  • comparator: SetComparator = SetComparator.Equal

  Returns Ternary

  See

  Ternary for the returned satisfiability result

subtract

• subtract(
      other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>,
  ): this

  Subtracts another abstract value from the current abstract value by removing all elements of the other abstract value from the current abstract value.

  Parameters

  • other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>

  Returns this

toJson

• toJson(): unknown

  Converts the lattice into a JSON serializable value.

  Returns unknown

top

• top(): SetRangeDomain<T, Value> & SetRangeDomain<
      T,
      { min: Set<never>; range: typeof Top },
  >

  Gets the Top element (greatest element) of the complete lattice (should additionally be provided as static function).

  Returns SetRangeDomain<T, Value> & SetRangeDomain<
      T,
      { min: Set<never>; range: typeof Top },
  >

toString

• toString(): string

  Converts the lattice into a human-readable string.

  Returns string

union

• union(
      other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>,
  ): this

  Creates the union of this abstract value and another abstract value by creating the union of the minimum and maximum set, respectively.

  Parameters

  • other: SetRangeLift<T> | SetRangeDomain<T, Value> | ArrayRangeValue<T>

  Returns this

upper

• upper(): typeof Top | typeof Bottom | ReadonlySet<T>

  The maximum set (upper bound) of the set range representing all values that can possibly exist (union of lower and range).

  Returns typeof Top | typeof Bottom | ReadonlySet<T>

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

widenDown

• widenDown(): this

  Extends the minimum set of the current abstract value down to the empty set.

  Returns this

widenUp

• widenUp(): this

  Extends the maximum set of the current abstract value up to Top.

  Returns this