Abstract
We investigate Jacobs and Langen's Sharing domain, introduced for the analysis of variable sharing in logic programs, and show that it is isomorphic to Marriott and Søndergaard's Pos domain, introduced for the analysis of groundness dependencies. Our key idea is to view the sets of variables in a Sharing domain element as the models of a corresponding Boolean function. This leads to a recasting of sharing analysis in terms of the property of "not being affected by the binding of a single variable." Such an "unaffectedness dependency" analysis has close connections with groundness dependency analysis using positive Boolean functions. This new view improves our understanding of sharing analysis, and leads to an elegant expression of its combination with groundness dependency analysis based on the reduced product of Sharing and Pos. It also opens up new avenues for the efficient implementation of sharing analysis, for example using reduced order binary decision diagrams, as well as efficient implementation of the reduced product, using domain factorizations.
Original language | English |
---|---|
Pages (from-to) | 948-976 |
Number of pages | 29 |
Journal | ACM Transactions on Programming Languages and Systems |
Volume | 21 |
Issue number | 5 |
DOIs | |
Publication status | Published - 1 Jan 1999 |
Externally published | Yes |
Keywords
- Abstract interpretation
- Boolean functions
- Dataflow analysis
- Global analysis
- Invariants
- Languages
- Logic programming
- Logics of programs
- Optimization
- Processors - compilers
- Specifying and Verifying and Reasoning about Programs - assertions
- Theory