Semantic Hierarchy Refactoring by Abstract Interpretation
Tino Cortesi · 2006
Semantics An abstraction of C can be obtained by considering the abstract counterpart for the concrete semantics equation. The best approximation for the initial states of the class is α(S0) = S0. The best approximation in P of the forward collecting method semantics of m of C is m ∈ [P → P ] defined as m (S) = α ◦ > m ◦ γ(S). The equation system becomes: S = S0 ⊔ m∈M Sm Sm = m (S) m ∈ M. (3) The above equations are monotonic and, by the Tarski fixpoint theorem, there exists a least solution 〈S, S0, {m : Sm}〉. Univ. Ca’ Foscari di Venezia, march 02, 2006 p. 16/32 Semantic Hierarchy Refactoring by Abstract Interpretation Tino Cortesi The abstract preconditions can be obtained by considering the best approximation of the backward collecting method semantics m ∈ [P → P ] defined as m (S) = α ◦ < m ◦ γ(S) The method abstract preconditions are obtained by projecting m (Sm) respectively on the method input values and the instance fields: Vm = πin( m (Sm)) and Bm = πF( m (Sm)). To sum up, the triple C = 〈S, S0, {m : 〈Vm, Bm〉 → Sm}〉 belongs to the domain of observables, and it is the best sound approximation of the semantics of C, w.r.t the properties encoded by the abstract domain 〈P, 〉. Theorem Let 〈P, 〉 be an abstract domain and let the observable of a class C w.r.t. the property encoded by 〈P, 〉 be C = 〈S, S0, {m : 〈Vm, Bm〉 → Sm}〉. Then αo( C ) o C . Univ. Ca’ Foscari di Venezia, march 02, 2006 p. 17/32 Semantic Hierarchy Refactoring by Abstract Interpretation Tino Cortesi Example Let us instantiate 〈P, 〉 with Con, the abstract domain of equalities of linear congruences. The elements of such a domain have the form x = amod b, where x is a program variable and a and b are integers. The representation function γc ∈ [Con → P(Σ)] is defined as γc(x = amod b) = {σ ∈ Σ | ∃k ∈ N. σ(x) = a+ k · b}. Let us consider the classes Even and MultEight above, and let e be the property x = 0 mod 2, d the property x = 1 mod 2 and u be the property x = 0 mod 8 . Then the observables of Even and MultEight w.r.t. Con are Even = 〈e, e, {add : 〈⊥, e〉 → e, sub : 〈⊥, e〉 → e}〉 Odd = 〈d, d, {add : 〈⊥, d〉 → d, sub : 〈⊥, d〉 → d}〉 MultEight = 〈u, u, {add : 〈⊥, u〉 → u, sub : 〈⊥, u〉 → u}〉. Univ. Ca’ Foscari di Venezia, march 02, 2006 p. 18/32 Semantic Hierarchy Refactoring by Abstract Interpretation Tino Cortesi Syntactic Subclassing The intuition behind the syntactic subclassing relation is inspired by the Smalltalk approach to inheritance: a subclass must answer to all the messages sent to its superclass. Stated otherwise, the syntactic subclassing relation is defined in terms of inclusion of class interfaces: Let A and B be two classes, and the interface operator ι(·). Then the syntactic subclass relation is defined as A B ⇐⇒ ι(A) ⊇ ι(B). Univ. Ca’ Foscari di Venezia, march 02, 2006 p. 19/32 Semantic Hierarchy Refactoring by Abstract Interpretation Tino Cortesi Semantic Subclassing Let 〈O, o〉 be an abstract domain of observables and let A and B be two classes. Then the semantic subclassing relation with respect to O is defined as A O B ⇐⇒ A o B . The semantic subclassing relation formalizes the intuition that up-to a given property, a class A behaves like a class B. For example, if the property of interest is the type of the class, then A is a semantic subclass of B if its type is a subtype of B. In our framework, semantic subclassing can be defined in terms of the preservation of observables. In fact, as o is the abstract counterpart for the logical implication then A o B means that A preserves the semantics of B, when a given property of interest is observed. Univ. Ca’ Foscari di Venezia, march 02, 2006 p. 20/32 Semantic Hierarchy Refactoring by Abstract Interpretation Tino Cortesi Semantic subclass relation B Semantics B Abstract Semantics B