Work on this exercise locally
This web app is a reference guide — you can read instructions, browse starter code, and view tests here. To actually complete the exercise, you need to work in your local development environment.
git clone https://github.com/weihaoqu/program-analysis-bootcamp-studentfailwith "TODO" with your implementation.dune runtest modules/module4-abstract-interpretation/exercises/interval-domainInterval Domain
8. Exercise 4: Interval Domain (28 tests)
Goal: Implement an infinite-height domain with widening for guaranteed termination.
Time: ~30 minutes
Files to edit:
exercises/interval-domain/starter/interval_domain.ml— the domainexercises/interval-domain/starter/interval_eval.ml— expression evaluator
The interval type
type bound = NegInf | Finite of int | PosInf
type interval = Bot | Interval of bound * bound
What to implement
In interval_domain.ml:
| # | Function | Hint |
|---|---|---|
| 1–4 | add_bound, neg_bound, min_bound, max_bound | Helper functions for bound arithmetic. Handle NegInf/PosInf cases carefully |
| 5 | bottom, top | Bot and Interval(NegInf, PosInf) |
| 6 | join | [min(a,c), max(b,d)] — the smallest interval containing both |
| 7 | meet | [max(a,c), min(b,d)] — the overlap; Bot if empty |
| 8 | leq | [a,b] ⊑ [c,d] iff c ≤ a and b ≤ d |
| 9 | widen | Key function! If the new bound exceeds the old, jump to ±∞ |
| 10 | contains_zero, is_non_negative | Range queries |
| 11–15 | abstract_add, abstract_sub, abstract_neg, abstract_mul, abstract_div | Interval arithmetic (mul needs all 4 corners) |
In interval_eval.ml:
| # | Function | Hint |
|---|---|---|
| 1 | eval_expr env expr | Same pattern as constant_eval, but using interval operations |
The widening rule (most important function!)
widen([a, b], [c, d]) =
lower = if c < a then NegInf else a
upper = if d > b then PosInf else b
If the bounds grow → jump to infinity. If they shrink or stay → keep.
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/interval-domain/
Starter Files
Test Files
Work on this exercise locally
This web app is a reference guide — you can read instructions, browse starter code, and view tests here. To actually complete the exercise, you need to work in your local development environment.
git clone https://github.com/weihaoqu/program-analysis-bootcamp-studentfailwith "TODO" with your implementation.dune runtest modules/module4-abstract-interpretation/exercises/interval-domainInterval Domain
8. Exercise 4: Interval Domain (28 tests)
Goal: Implement an infinite-height domain with widening for guaranteed termination.
Time: ~30 minutes
Files to edit:
exercises/interval-domain/starter/interval_domain.ml— the domainexercises/interval-domain/starter/interval_eval.ml— expression evaluator
The interval type
type bound = NegInf | Finite of int | PosInf
type interval = Bot | Interval of bound * bound
What to implement
In interval_domain.ml:
| # | Function | Hint |
|---|---|---|
| 1–4 | add_bound, neg_bound, min_bound, max_bound | Helper functions for bound arithmetic. Handle NegInf/PosInf cases carefully |
| 5 | bottom, top | Bot and Interval(NegInf, PosInf) |
| 6 | join | [min(a,c), max(b,d)] — the smallest interval containing both |
| 7 | meet | [max(a,c), min(b,d)] — the overlap; Bot if empty |
| 8 | leq | [a,b] ⊑ [c,d] iff c ≤ a and b ≤ d |
| 9 | widen | Key function! If the new bound exceeds the old, jump to ±∞ |
| 10 | contains_zero, is_non_negative | Range queries |
| 11–15 | abstract_add, abstract_sub, abstract_neg, abstract_mul, abstract_div | Interval arithmetic (mul needs all 4 corners) |
In interval_eval.ml:
| # | Function | Hint |
|---|---|---|
| 1 | eval_expr env expr | Same pattern as constant_eval, but using interval operations |
The widening rule (most important function!)
widen([a, b], [c, d]) =
lower = if c < a then NegInf else a
upper = if d > b then PosInf else b
If the bounds grow → jump to infinity. If they shrink or stay → keep.
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/interval-domain/