summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 21 Sep 2011 02:38:53 +0200 | |

changeset 45018 | 020e460b6644 |

parent 45017 | 07a0638c351a |

child 45019 | 4e3b999c62fa |

refined comment

--- a/src/HOL/IMP/AbsInt2.thy Wed Sep 21 09:17:01 2011 +1000 +++ b/src/HOL/IMP/AbsInt2.thy Wed Sep 21 02:38:53 2011 +0200 @@ -6,9 +6,18 @@ subsection "Widening and Narrowing" -text{* The assumptions about widen and narrow are merely sanity checks. They -are only needed in case we want to prove termination of the fixedpoint -iteration, which we do not --- we limit the number of iterations as before. *} +text{* The assumptions about widen and narrow are merely sanity checks for +us. Normaly, they serve two purposes. Together with a further assumption that +certain chains become stationary, they permit to prove termination of the +fixed point iteration, which we do not --- we limit the number of iterations +as before. The second purpose of the narrowing assumptions is to prove that +the narrowing iteration keeps on producing post-fixed points and that it goes +down. However, this requires the function being iterated to be +monotone. Unfortunately, abstract interpretation with widening is not +monotone. Hence the (recursive) abstract interpretation of a loop body that +again contains a loop may result in a non-monotone function. Therefore our +narrowing interation needs to check at every step that a post-fixed point is +maintained, and we cannot prove that the precision increases. *} class WN = SL_top + fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)