# Abstract interpretation

Use interval summaries to enclose concrete values, and distinguish containment from exact sets.

## Definitions

- **Concrete state set**: The actual values attainable from the declared input domain.
- **Interval abstraction**: A lower and upper bound enclosing concrete values.
- **Sound transfer**: An abstract operation that contains every concrete output.

## Acceptance procedure

1. Start from every integer in the initial interval.
2. Apply each affine transform to the concrete set.
3. Apply endpoint arithmetic to the interval, reordering endpoints for negative scales.
4. Check every concrete value remains enclosed and the final bounds are tight.

## Complexity

With a concrete interval of k integers and t transformations, this finite replay costs O(kt). Abstract endpoint propagation alone costs O(t).

## Common failure

A tight interval can include unattainable interior values; it is not necessarily an exact concrete set.

## Extensions

Add control-flow joins, fixed points, widening, and overflow-specific abstractions.

## Instances

- KL-FCS-037: A positive affine transfer — Sound enclosure: yes; Tight interval bounds: yes
- KL-FCS-038: Negative scaling reverses bounds — Sound enclosure: yes; Tight interval bounds: yes
- KL-FCS-039: Compose three abstract transfers — Sound enclosure: yes; Tight interval bounds: yes

## References

- https://www.di.ens.fr/~cousot/AI/