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/galois-connectionsGalois Connections
7. Exercise 3: Galois Connections (Optional, 16 tests)
This exercise is optional. It covers the theoretical foundations of abstract interpretation (Galois connections, adjunction, monotonicity). Completing it will deepen your understanding but is not required for Exercise 4 or the lab. Skip to Exercise 4 if you prefer.
Goal: Formalize the alpha/gamma pair for the sign domain and verify soundness properties (adjunction, monotonicity).
Time: ~25 minutes
File to edit: exercises/galois-connections/starter/galois.ml
Also read: exercises/galois-connections/starter/worksheet.md (guided
questions — fill in on paper or in the file)
Key ideas
-
alpha (abstraction): maps a set of integers to the best sign
alpha({1, 2, 3}) = Posalpha({-1, 0, 5}) = Topalpha({}) = Bot
-
gamma (concretization): maps a sign to a representative set
gamma(Zero) = {0}(exact)gamma(Pos) = {1, 2, 3, ...}(representative, not exhaustive)
-
Adjunction:
alpha(c) ⊑ aiffc ⊆ gamma(a)
What to implement
| # | Function | Hint |
|---|---|---|
| 1 | sign_leq a b | Same as Exercise 1's leq |
| 2 | sign_equal a b | Structural equality |
| 3 | sign_to_string | Same as Exercise 1 |
| 4 | alpha_int n | Single integer → sign |
| 5 | alpha set | Fold over the set, joining signs. Empty set → Bot |
| 6 | gamma_repr sign | Return (representative_set, is_exact). Bot → ({}, true), Zero → ({0}, true), Pos → ({1,2,3}, false) |
| 7 | in_gamma n sign | Is concrete value n in the concretization of sign? |
| 8 | verify_adjunction set sign | Check: sign_leq (alpha set) sign iff IntSet.subset set (gamma_set sign) — but gamma is infinite, so use in_gamma for each element |
| 9 | verify_alpha_monotone s1 s2 | If s1 ⊆ s2 then alpha(s1) ⊑ alpha(s2) |
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/galois-connections/
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/galois-connectionsGalois Connections
7. Exercise 3: Galois Connections (Optional, 16 tests)
This exercise is optional. It covers the theoretical foundations of abstract interpretation (Galois connections, adjunction, monotonicity). Completing it will deepen your understanding but is not required for Exercise 4 or the lab. Skip to Exercise 4 if you prefer.
Goal: Formalize the alpha/gamma pair for the sign domain and verify soundness properties (adjunction, monotonicity).
Time: ~25 minutes
File to edit: exercises/galois-connections/starter/galois.ml
Also read: exercises/galois-connections/starter/worksheet.md (guided
questions — fill in on paper or in the file)
Key ideas
-
alpha (abstraction): maps a set of integers to the best sign
alpha({1, 2, 3}) = Posalpha({-1, 0, 5}) = Topalpha({}) = Bot
-
gamma (concretization): maps a sign to a representative set
gamma(Zero) = {0}(exact)gamma(Pos) = {1, 2, 3, ...}(representative, not exhaustive)
-
Adjunction:
alpha(c) ⊑ aiffc ⊆ gamma(a)
What to implement
| # | Function | Hint |
|---|---|---|
| 1 | sign_leq a b | Same as Exercise 1's leq |
| 2 | sign_equal a b | Structural equality |
| 3 | sign_to_string | Same as Exercise 1 |
| 4 | alpha_int n | Single integer → sign |
| 5 | alpha set | Fold over the set, joining signs. Empty set → Bot |
| 6 | gamma_repr sign | Return (representative_set, is_exact). Bot → ({}, true), Zero → ({0}, true), Pos → ({1,2,3}, false) |
| 7 | in_gamma n sign | Is concrete value n in the concretization of sign? |
| 8 | verify_adjunction set sign | Check: sign_leq (alpha set) sign iff IntSet.subset set (gamma_set sign) — but gamma is infinite, so use in_gamma for each element |
| 9 | verify_alpha_monotone s1 s2 | If s1 ⊆ s2 then alpha(s1) ⊑ alpha(s2) |
Run tests
dune runtest modules/module4-abstract-interpretation/exercises/galois-connections/