Add a section on data-flow convergence

This commit is contained in:
Camelid 2020-11-10 16:22:45 -08:00 committed by Joshua Nelson
parent 4b00bfb892
commit 6a4c0ee05f
1 changed files with 15 additions and 1 deletions

View File

@ -89,7 +89,21 @@ statement must be considered separately from the left-hand side.
### Convergence
TODO
Your analysis must converge to "fixpoint", otherwise it will run forever.
Converging to fixpoint is just another way of saying "reaching equilibrium".
In order to reach equilibrium, your analysis must obey some laws. One of the
laws it must obey is that the bottom value joined with some other value equals
the second value. Or, as an equation:
> *bottom* join *x* = *x*
Another law is that your analysis must have a "top value" such that
> *top* join *x* = *top*
Having a top value ensures that your semilattice has a finite height, and the
law state above ensures that once the dataflow state reaches top, it will no
longer change (the fixpoint will be top).
## Inspecting the Results of a Dataflow Analysis