[<<][staapl][>>][..]Fri Sep 18 19:09:10 CEST 2009

While intuitively, abstract interpretation for staging (symbolic computation) is quite straightforward to do, the mathematical definition relies on order-preserving functions on lattices. A canonical example of a lattice is the set of subsets of a set, together with union and intersection (a boolean lattice[1]). I.e. arithmetic can be approximated over the lattice made up of the subsets of {+,0,-}. {+} add {+} -> {+} {-} add {+} -> {+,0,-} = T x mul {0} -> {0} ... So.. The missing links and terminology seem to come from denotational semantics[2]. As far as I get it now, an abstract semantics is related to a full denotational semantics in some structure-preserving way. Attempt: In the following diagram L and L' are lattices, f is a concrete function, f' an abstract function, a : L->L' is the abstraction function and c : L'->L is the concretization function. The a and c are ``semi-inverses'' in that they preserve order: they form a Galois Connection[5]. The abstraction is sound when whenever c acts as a ``semi-homomorphism'' f . c < c . f' respecting the order relation instead of an equivalence, i.e. the following diagram commutes: f L ---------> L ^ ^ | | | c | c | | | | f' L' ---------> L' In other words, soundness means that for any concrete operation forall x, f x = y, if x \in c(x') then y \in c(f' x') meaning that for all x, if x' is an abstraction of x and f' is an abstraction of f then f'x' is an abstraction of y. It's convenient to picture the original semantics L as the powerset of some set |L (i.e. the natural numbers |N): already containing all approximations. In this case the abstract representation L' is related to |L by mapping elements l' to subsets of |L. The order relation in L represents ``level of abstraction''. I.e. the element + in L' could map to the element {0,1,2,...} in L. Now, from the first lecture of Cousot[7], we find: Abstract interpretation is considering an abstract semantics that is a _superset_ of the concrete semantics of the program, hence it covers all possible concrete cases. This leads to the requirements: 1. sound (cover all cases) 2. precise (avoid false alarms) and 3. simple (avoid combinatorial explosion). So, conclusions: what I'm doing at the moment is a combination of several techniques: it produces a trace (abstract evaluation of the interpretation step function) + approximates values by values U variables / expressions. It would be interesting to try to formalize this. Soundness seems ``obvious'' in my case, so te proof shouldn't be too difficult (probably trivial once there's a formal model). In general however, it does seem like a good idea to try to keep the theory in mind next time I need to do some analysis, and use specific applications as an example. [1] http://en.wikipedia.org/wiki/Boolean_lattice [2] http://en.wikipedia.org/wiki/Denotational_semantics [3] http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk1p.pdf [4] http://santos.cis.ksu.edu/schmidt/Escuela03/home.html [5] http://en.wikipedia.org/wiki/Galois_connection [6] http://santos.cis.ksu.edu/schmidt/Escuela03/WSSA/talk3p.pdf [7] http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/

[Reply][About]

[<<][staapl][>>][..]