Comparing the Galois Connection and Widening Narrowing Approaches

-

English
29 Pages
Read an excerpt
Gain access to the library to view online
Learn more

Description

Niveau: Supérieur
Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation Patrick Cousot1 and Radhia Cousot2 1 LIENS, DMI, École Normale Supérieure, 45, rue d'Ulm, 75230 Paris cedex 05 (France) 2 LIX, École Polytechnique, 91128 Palaiseau cedex (France) Abstract. The use of infinite abstract domains with widening and - narrowing for accelerating the convergence of abstract interpretations is shown to be more powerful than the Galois connection approach re? stricted to finite lattices (or lattices satisfying the chain condition). 1 Introduction A widely-held opinion is that finite lattices (or lattices satisfying the chain condi? tion, i.e., such that all strictly increasing chains are finite) can be used instead of widenings and narrowings to ensure the termination of abstract interpretations of programs on infinite lattices. We show that, in general, this can only be to the detriment of precision and prove that the use of infinite abstract domains with widenings and narrowings is more powerful than the Galois connection approach for finite lattices (or lattices satisfying the chain condition). By way of example, various widenings are suggested for solving non-convergence problems left open in the literature. 2 Upper Approximation of the Collecting Semantics Following [CC76,CC77a,CC79b] , the abstract interpretation of a program can be formalized as the e?ective computation of an upper approximation A of the collecting semantics of the program.

  • abstract interpretation

  • con?? ?

  • precise than

  • strictly nec?

  • approximation relation

  • no strictly

  • galois connection

  • upper approximation


Subjects

Informations

Published by
Reads 21
Language English
Report a problem

Comparing the Galois Connection
and Widening/Narrowing Approaches
to Abstract Interpretation
1 2PatrickCousot andRadhiaCousot
1 LIENS,DMI,ÉcoleNormaleSupérieure,45,rued’Ulm,75230Pariscedex05
(France)
cousot@dmi.ens.fr
2 LIX,ÉcolePolytechnique,91128Palaiseaucedex(France)
radhia@polytechnique.fr
Abstract. The use of infinite abstract domains with widening and -
narrowing for accelerating the convergence of abstract interpretations
is shown to be more powerful than the Galois connection approach re­
stricted to finite lattices (or lattices satisfying the chain condition).
1 Introduction
Awidely-heldopinionisthatfinitelattices(orlatticessatisfyingthechaincondi­
tion,i.e.,suchthatallstrictlyincreasingchainsarefinite)canbeusedinsteadof
wideningsandnarrowingstoensuretheterminationofabstractinterpretations
ofprogramsoninfinitelattices.Weshowthat,ingeneral,thiscanonlybetothe
detrimentofprecisionandprovethattheuseofinfiniteabstractdomainswith
wideningsandnarrowingsismorepowerfulthantheGaloisconnectionapproach
forfinitelattices(orlatticessatisfyingthechaincondition).Bywayofexample,
variouswideningsaresuggestedforsolvingnon-convergenceproblemsleftopen
intheliterature.
2 Upper Approximation of the Collecting Semantics
Following[CC76,CC77a,CC79b],theabstractinterpretationofaprogramcan
beformalizedastheeffectivecomputationofanupperapproximationAofthe
collecting semanticsoftheprogram.
This collecting semantics can often be specified as the least fixed point
con1lfp (F) of a continuous operator F ∈ L −→ L on a cpo L(, )greater⊥-
2thana basis⊥- satisfying⊥- F(⊥-).ByKleenefixpointtheorem(Prop. 23in
nthe appendix), lfp (F) is the least upper bound F (⊥-)ofthe iterates⊥- n∈IN
def defn 0 n+1 nF (⊥-)definedbyF (x)= xandF (x)= F(F (x))forallx∈L.
This work was supported in part by Esprit BRA action 3124 “Sémantique”.
1 Monotony is sufficient by considering transfinite iterations [CC79a].
2 -The basis⊥ is often the infimum⊥ of the cpo, in which case lfp F is written lfpF.⊥-270
3ThisapproximationAmustbe soundinthesensethatlfp(F)A .
Example 1 ((Imperative programs)). Assumethatthecollectingsemanticsofthe
following Pascalprogram:
program P;
var I : integer ;
begin
I := 1;
while I <= 100 do
begin
{I ∈ [1, 100] }
I := I + 1;
end;
{I=101 }
end.
isthesetofpossiblevaluesofintegervariable Iwhenstartingexecutionofthe
loopbody.Itistheleastfixedpointlfp(F)=lfp (F)={i∈ZZ|1≤i≤100}∅
ofthecontinuous(andevenadditive)operator:
con .F ∈L −→L = λX ({1}∪{i+1|i∈X})∩{i∈ZZ|i≤100} (1)
onthecompletelatticeL=℘(ZZ)(⊆,∅,ZZ,∩,∪)whereZZisthesetofintegers
and℘(S)isthepowersetofthesetS.
Asound upper approximationisthe loopinvariantA= {i ∈ ZZ | i ≥0}
specifyingthat Iisnon-negative.
Example 2 ((Logic programs)). Let Pbealogicprogram(containingatleast
none constant), B be its Herbrand universe over a family F = F ofP n∈IN
nn-ary functors f∈F and ground(P) be the set of all ground instances of
con
clausesin P.The immediate consequence operator is T ∈℘(B ) −→℘(B )P P P
suchthat:
.T =λX {A |A←B,...,B ∈ground(P)∧∀i=1,...,n:B ∈X} .P 1 n i
A modelofPisasetI⊆B ,suchthatT (I)⊆I.ThecharacterizationtheoremP P
ofvanEmdenandKowalski[vEK76]showsthatP hasaleastmodelM intheP n
completelattice℘(B )(⊆,∅,∪)suchthatM =lfp T = T (∅). P P P P∅ n∈IN
Example 3 ((Functional programs)). Following [CC92c], the relational seman­
ticsofthefunctionalfactorialprogram:
f(n) ≡ if n = 0 then 1 else n ∗ f(n − 1);
def
isf ∈℘(IN ×IN ),whereIN =IN∪{⊥}and⊥representsnon-termination,⊥ ⊥ ⊥
suchthat:f ={ ⊥ , ⊥ }∪{ n, ⊥ | n<0}∪{ n, n! | n≥0}.Itistheleast
con
fixpointlfp F ofF ∈℘(IN ×IN ) −→℘(IN ×IN )suchthat:⊥ ⊥ ⊥ ⊥⊥-
F(f)={ ⊥ ,⊥ }∪{ 0,1 }∪{ n,n∗ρ | n−1,ρ ∈ f}
3 Although commonly satisfied, these hypotheses on the definition of the collecting
semantics and the specification of the approximation are stronger than strictly nec­
essary, see a discussion of various weaker hypotheses in [CC92b].
271
where⊥−ρ=ρ−⊥=⊥and⊥∗ρ=ρ∗⊥=⊥.Thesemanticdomain℘(IN ×⊥
-IN )(,⊥-,,)isacompletelattice,where:⊥
def
⊥- =IN ×{⊥}⊥
def-=IN ×IN⊥
def - -f f =(f∩ )⊆(f ∩ ) ∧ (f∩⊥-)⊇(f ∩⊥-)
def - f = ∪ (f ∩ )∪∩ (f ∩⊥-) .i∈ i i∈ i i∈ i
Observethatff ifandonlyiff producesmoreoutputresultsinINthatf
foragiventerminatingornon-terminatingargumentinIN andf terminates⊥
morefrequentlythanf.
3TheGaloisConnectionApproachtoAbstract
Interpretation
Principle ofthe Approach. TheGalois connectionapproachtoabstractinter­
pretation[CC76,CC77a]formalizestheideathattheequationX =F(X)can
mon
befirstsimplifiedintoX=F(X),whereF ∈L −→LandL(,)isaposet,
-andthensolvediterativelystartingfromthebasis ⊥.Thetechniqueconsistsin
understandingLasadiscreteapproximationofLandinextendingthisnotion
ofapproximation,invariousways,tosemanticdomainssuchasproductsL×L,
powersets℘(L)andfunctionspacesL −→L[CC77b,CC79b].
Galois Connection. ThecorrespondencebetweenthesemanticdomainLandits
abstractversionLcanbeformalizedbyaGaloisconnection(alsocalled pair of
adjoined functions).
Definition 4.*IfL()andL()areposets,thenα,γisa Galois connec­
γ
−tion,writtenL−L,ifandonlyifα∈L −→Landγ∈L −→Larefunctionsα
suchthat:
∀x∈L,y∈L: α(x)y ⇐⇒ (xγ(y)) . (2)
α(x)isthe abstractionofx,i.e.,themostpreciseapproximationofx∈LinL.
γ(y)isthe concretizationofy,i.e.,themostimpreciseelementofLwhichcan
besoundlyapproximatedbyy∈L.
Example 5 ((Intervals)). In[CC76],℘(ZZ)orderedby⊆isapproximatedusing
the abstract lattice of intervals L = {⊥}∪{[ , u ] | ∈ ZZ∪{−∞}∧u ∈
ZZ∪{+∞}∧≤u}orderedby,suchthat:
def
⊥ [ ,u ] =true
(3)def
[,u ][,u ] = ≤ ≤u ≤u .0 0 1 1 1 0 0 1
ThisapproximationisformalizedbytheGaloisconnectiondefinedby:
γ(⊥)=∅ α(∅)=⊥
γ([ ,u ])={x∈ZZ|≤x≤u} α(X)=[minX,maxX] .
Forexampletheset{1,2,5}∈℘(ZZ)issoundlyapproximatedby[1,5]∈L. 272
Soundness and Precision. Here,theconcreteandabstractnotionsofsoundness
andprecisionareformalizedinthesameway,bytherespectivepartialorders
on Land on L. x y is interpretedas “y is asound approximationof
x”, “xisamorepreciseconcreteassertionthany”or“xlogicallyimplies y”.
Thesamewayxy z meansthaty andz aresoundapproximationsofx
butyismoreprecisethanz.Wemayhavexyandxzbutneitheryz
nor z y in which case y and z are non-comparable sound approximations
of x.Equation(2)statesthattheconcreteandabstractnotionsofsoundness
andprecisioncoincide,uptoanapproximation,whichconsistsinrepresenting
severalconcreteassertions{x|α(x)=x}bythesameabstractassertionx.
Example 6 ((Intervals, continued)). For intervalsconsidered in Ex.5, the con­
creteapproximationrelationissubsetinclusion ⊆whereastheabstractap­
proximationrelation is definedby(3).For example, {1,2,5}⊆{i ∈ ZZ |
i≥1}and{1,2,5}⊆{i∈ZZ|i≤5}sincetheassertionthatthevalueofa
variablecanonlybe1,2or5duringexecutionismoreprecisethansayingthat
itisstrictlypositive.Theseassertionsarerespectivelyabstractedby[1,5][1,
+∞]and[1,5][−∞,5]buttheseapproximationsarenotcomparablesince
[1,+∞][−∞,5]and[−∞,5][1,+∞].[1,5]isthebestpossibleabstract
approximationoftheconcreteassertion{1,2,5}.
Extension to Function Spaces.Theconcreteapproximationrelation ∈ ℘(L×L)
defcan be extended to the function space L −→ L pointwise, i.e., F F =
∀x∈L:F(x)F (x).TheintuitionisthatF ismoreprecisethanF ifand
onlyifF alwaysyieldsmorepreciseresultsthanF .
Then,theapproximationofLbyLcanbeextendedtotheapproximationof
thefunctionspaceL −→LbyL −→Lusingthefunctionalabstractionαand
concretizationγdefined,asin[CC77b],by:
α∈(L −→L) −→(L −→L) γ∈(L −→L) −→(L −→L)
(4)def def
◦ ◦ ◦ ◦α(ϕ)=α ϕ γ γ(ϕ)=γ ϕ α
suchthat,byProp.25intheappendix:
γmon mon−(L −→L)−(L −→L) . (5)
α
γ
−Intuitively,α(F)istheabstractimageofF uptotheGaloisconnectionL−L.α
con
Itfollows,byProp.30intheappendix,thatifL(,)isaposet,F ∈L −→L,
and⊥- isα(⊥-),thenlfp (F)γ lfp (α(F)) .Otherwisestated,thefixpoint-⊥ ⊥-
operatorlfppreservesthesoundnessoftheapproximation[CC77b].
Functional Abstraction. Inpracticeα(F)maynotbeeasytoprogram.Inthis
casewecanuseanupperapproximationF.Moreprecisely,F ∈(L −→L)isan
con
abstractionofF ∈(L −→L)ifandonlyifα(F)For,equivalently,F γ(F).
Diagrammatically:
273
F F
L ✲ L L ✲ L

γ
γ ✻ ⇐⇒ α
α ❄
F F
L❄ ✲ L L✲ L .
Intuitively,F(x)isanapproximationofF(x)whenappliedtoanapproximation
xofx.
- -Definition 7. *L, ⊥, Fisan abstract interpretation ofL, ⊥,F,written
γ γ
4− −L,⊥-,F−L,⊥-,F,ifandonlyifL−L,α(⊥-) ⊥- andα(F)F .α α
γ−If L, ⊥-,F−L, ⊥-, Fand Ais anupperboundoftheabstractiteratesαn
5F (⊥-),n∈ IN, then lfp (F)γ(A),asshownbyProp.31intheappendix .⊥-
Otherwisestatedanyupperboundoftheabstractiteratesisasoundapproxi­
mationofthecollectingsemantics.
Example 8 ((Intervals, continued)). GiventheintervalabstractionofEx.5,the
approximateequationX=F(X)correspondingto(1)forprogram Pisdefined
by:
mon .F ∈L −→L=λX ([1,1](X⊕[1,1]))[−∞,100]
where⊥ X =X ⊥ =X,[ ,u ][ ,u ]=[min( , ),max(u ,u )],0 0 1 1 0 1 0 1
⊥ X =X ⊥ = ⊥,[ ,u ][ ,u ]=ifmax( , )>min(u ,u)then0 0 1 1 0 1 0 1
⊥else[max( , ),min(u ,u )],⊥⊕X=X⊕⊥=⊥and[ ,u ]⊕[ ,u ]0 1 0 1 0 0 1 1
=[ + ,u +u].Itcanbesolvediterativelystartingfromtheinfimum ⊥.0 1 0 1
Thesuccessiveiteratesare⊥,[1,1],[1,2],...,[1,100].Thissequencemight
beinfiniteandstrictlyincreasing(e.g.fornonterminatingprograms).
n
Inpractice,finiteconvergenceoftheabstractiteratesF (⊥-),n∈INmustbe
n
ensured.ThisleadstohypothesesonLandFsuchas,e.g.,LisfiniteorF (⊥-),
n∈INisanincreasingchainandnostrictlyincreasingchaininLcanbeinfinite
(i.e. Lsatisfiestheso-called ascending chain condition). Observethatvarious
n
-hypothesesensurethatF (⊥),n∈INisanincreasingchain.Forexample,F
-mightbe extensive(i.e.,∀x∈L:xF(x))or⊥maybea prefixpointofF (i.e.,
mon
- -⊥F(⊥))andF ∈L −→Lmaybemonotone.Formoredetailsorequivalent
approaches,see[CC79b],[Cou78,chapter4]and[CC92a].
Example 9 ((Descriptive types)). InPrologtypeanalysisofBruynoogheetal.
[BJCD87,JB92],asetofgroundterms isapproximatedbya type graph such
asthefollowingone(whereaandbareconstantsofarity0andf isabinary
functor):
4 α(⊥-) ⊥- is equivalent to⊥- γ(⊥-)andα(F)F is equivalent to F ◦γγ ◦F or
to α◦F F ◦α (see Prop.26 in the appendix), so that we can dispense with either
α or γ,[CC92b].
5 which is the case for A=lfp F whenever this least fixpoint exists.⊥-274
❄❜✛ ✟

2 ❅✠❘
a f ✠
1
✠❜

b
AtypegraphG∈Gisafinitebipartitegraph,consistingof:
1. AfinitesetN oftypenodes(marked◦indiagrams),t
n2. AfinitesetN offunctornodesm,labeledwithn-aryfunctorsf(m)∈F ,f
andsuchthatN ∩N =∅,t f
3. Arootr∈N suchthatthereisapathfromrtoanynodeofG,t
4. AsetA∈℘(N ×N )∪℘(N ×IN×N)ofarcs,suchthat:t f f t
(a) Alltypenodesk∈N haveatleastoneoutgoingarcandalloutgoingt
arcsk, mgotofunctorsnodesm∈N withdistinctlabelsf(m),f
n(b) Allfunctorsnodesm∈N labeledwithafunctorf(m)∈F ofarityf
in∈ IN havenoutgoingarcsm, i, k,1≤i≤n(sothatthereisno
outgoingarcwhenn=0).
1 n nWewritek:g(k ,...,k )for∃m∈N :k,m ∈ A∧f(m)=g∈F ∧∀i∈[1,f
i 1 nn]:m,i,k ∈ Aandsaythattypenodesk ,...,k arethe sonsofnodek.A
groundtermt∈B issaidto fold on type nodek oftype graph G,ifandonlyP
if:
01. t=c∈F andk:c,
1 n2. t=g(t,...,t ),k:g(k ,...,k )andeachgroundtermt,1≤i≤nfolds1 n i
iontypenodek ofgraphG.
Theconcretizationfunctionisdefinedby:
γ(G)={t∈B |tfoldsontherootof G}P
For the type graphGabove,wehaveγ(G)= {a,f(b,a),f(b,f(b,a)), f(b,
f(b,f(b,a))),...}.
DefinetheequivalencerelationG≡G byγ(G)=γ(G).Thepartialorder
relationon L=G/ isdefinedbyGG ifandonlyif γ(G)⊆γ(G).We≡
haveGG ifandonlyifallpathsinGexistinG,whichcanbecheckedby
path-findingalgorithms.
Example 10 ((Strictness analysis)). InMycroft’sstrictnessanalysis[Myc80],a
mon
relationf ∈℘(IN ×IN )isapproximatedbyafunctionf ∈{0,1} −→{0,1}⊥ ⊥

suchthat01andf (0)=0onlyiff is strict,thatis:∀ρ∈IN : ⊥,ρ ∈ f⊥
=⇒ρ=⊥.ThisapproximationisformalizedbytheGaloisconnectiondefined
by:
. .γ(λx 0)=IN ×{⊥} α(f)=λx0if f=IN ×{⊥}⊥ ⊥
. .γ(λx x)={ ⊥ ,⊥ }∪ IN×IN α(f)=λx x if ⊥,ρ ∈ f=⇒ρ=⊥⊥
. .γ(λx 1)=IN ×IN α(f)=λx1otherwise .⊥ ⊥275
Thisabstractinterpretationcanbeliftedtohigher-orderfunctionsusing(4).
4 The Widening/Narrowing Approach to Abstract
Interpretation
Anothermethod[CC76,CC77a]forenforcingterminationoftheabstractinter­
%pretationconsistsinusinga widening ∈L×L −→Lsuchthat:
%∀x,y∈L:x x y (6)
%∀x,y∈L:y x y (7)
0 1for all increasing chains x x ..., the increasing chain (8)
0 0 i+1 i i+1%defined by y = x ,..., y = y x , ... is not strictly
increasing .
It follows, as shown by Prop.33 in the appendix, that the upward iteration
sequence with widening:
0ˆX =⊥-
i+1 i i iˆ ˆ ˆ ˆ (9)X =X if F(X)X
i iˆ ˆ%=X F(X)otherwise
ˆis ultimately stationary and its limit A is a sound upper approximation of
6lfp (F).ObservethatifLisajoin-semi-lattice(theleastupperboundxy⊥-
exists for all x, y ∈ L) satisfying the ascending chain condition, then is a
widening.
Thisapproximationcanthenbeimprovedusinga narrowingoperator ∈
L×L −→Lsuchthat:
∀x,y∈L:(yx)=⇒ (y(x&y)x) (10)
0 1for all decreasing chains x ' x ' ..., the decreasing chain (11)
0 0 i+1 i i+1defined by y = x ,..., y = y &x , ... is not strictly
decreasing .
It follows,as shownby Prop.34in the appendix, thatthe downward abstract
iteration sequence with narrowing:
0ˇ ˆX =A
(12)
i+1 i iˇ ˇ ˇX =X &F(X)
iˇ ˇisultimatelystationaryanditslimitAaswellaseachtermX ofthisdecreasing
i iˇ ˇchainisasoundupperapproximationoflfp (F).ObservethatifF(X)=X⊥-
6 Numerous variants are possible. For example, we might assume x y in (6)and
i+1 i i iˆ ˆ ˆ ˆ(7), and use X =X (X F X ) in (9), or use a different widening for each
iterate (as in [Cou81]) or even have a widening which depends upon all previous
iterates.276
i+1 iˇ ˇ ˆthen X = X so that if the approximation A of lfp F is a fixpoint of F⊥-
thenitcannotbeimprovedby(12).ObservealsothatifLisameet-semi-lattice
(thegreatestlowerboundxyexistsforallx,y∈L)satisfyingthe descending
chain condition (nostrictlydecreasingchaininLcanbeinfinite),thenisa
narrowing.
Example 11 ((Widening and narrowing for intervals)). The widening and nar­
rowingintroducedin[CC76]forthelatticeofintervalsL={⊥}∪{[ , u ]|∈
ZZ∪{−∞}∧u∈ZZ∪{+∞}∧≤u}aredefinedasfollows:
%⊥ X=X (13)
%X ⊥=X
%[,u ] [,u ]=[if < then −∞else ,0 0 1 1 1 0 0
if u >u then +∞elseu ] .1 0 0
The widening(13) extrapolatesunstable bounds toinfinity. Observethat the
%widening(13)isnotmonotone.Forexample[0,1][0,2]but[0,1] [0,2]=
%[0,+∞][0,2]=[0,2] [0,2].
Thenarrowingintroducedin[CC76]forthelatticeofintervalsL={⊥}∪{[,
u]|∈ZZ∪{−∞}∧u∈ZZ∪{+∞}∧≤u}isdefinedby:
⊥ X=⊥ (14)
X ⊥ =⊥
[,u ]&[,u]=[if =−∞then else ,0 0 1 1 0 1 0
if u =+∞thenu elseu ] .0 1 0
Thenarrowing(14)improvesinfiniteboundsonly.
Resolutionoftheequation:
X=F(X)=([1,1](X⊕[1,1]))[−∞,100]
consideredinEx.8startswiththefollowingincreasingiterates:
0ˆX =⊥
1 0 0ˆ ˆ ˆ%X =X [1,1](X ⊕[1,1]) [−∞,100]

%=⊥ [1,1](⊥⊕[1,1]) [−∞,100]
=([1,1] ⊥ )[−∞,100]
=[1,1]
2 1 1ˆ ˆ % ˆX =X [1,1](X ⊕[1,1]) [−∞,100]

%=[1,1] [1,1]([1,1]⊕[1,1]) [−∞,100]

%=[1,1] ([1,1][2,2])[−∞,100]
%=[1,1] ([1,2][−∞,100])277
%=[1,1] [1,2]
=[1, +∞]

3 2 2ˆ ˆ % ˆX =X [1,1](X ⊕[1,1]) [−∞,100]

%=[1, +∞] [1,1]([1, +∞]⊕[1,1]) [−∞,100]

%=[1, +∞] ([1,1][2, +∞])[−∞,100]
%=[1, +∞] ([1,+∞][−∞,100])
%=[1,+∞] [1,100]
=[1,+∞]
2ˆX .
Thenthedecreasingiteratesareasfollows:
0 2ˇ ˇX =X
1 0 0ˇ ˇ ˇX =X & [1,1](X ⊕[1,1]) [−∞,100]

=[1,+∞]& [1,1]([1,+∞]⊕[1,1]) [−∞,100]

=[1,+∞]& ([1,1][2, +∞])[−∞,100]
=[1,+∞]&([1,+∞][−∞,100])
=[1,+∞]&[1,100]
=[1,100]

2 1 1ˇ ˇ ˇX =X & [1,1](X ⊕[1,1]) [−∞,100]

=[1,100]& [1,1]([1,100]⊕[1,1]) [−∞,100]
=[1,100]
1ˇ=X .
Inwhatfollows,wewillconsiderthefactthatgiventwointegerconstantsn ≤1
n ,theabstractinterpreter syntox[Bou90]willanalyzetheprogram:2
program Pn n ;1 2
var I : integer ;
begin
I := n ;1
while I <= n do2
begin
{I ∈ [n , n]}1 2
I := I + 1;
end;
{I= n +1 }2
end.
bysolvingasystemoffixpointequationsequivalentto:
X=F(X)=([n,n ](X⊕[1,1]))[−∞,n ]1 1 2
andautomaticallydiscovertheloopinvariant:278
{ I ∈ [n,n ]} . 1 2
Example 12 ((Type graphs widening)). [BJCD87]havedefinedthe restrictionof
typegraphs.Itisawidening.Forexample:
% =❄ ❄ ❄❜ ❜ ❜✛ ✟
❅ ❅ ❅
2 ❅ ❅ ❅✠ ❘ ✠❘ ✠❘
a f a f a f ✠
12 12 1❅ ❅
❅ ❅ ✠❘✠❘✠❜❜ ❜❜ ❜
❄ ❄ ❄ ❄ ❄
ba bf b
12❅
❅✠ ❅❘❜❜
❄ ❄
ba
%Moreprecisely,thewidening G= G G oftwotypegraphs G and G is1 2 1 2
obtainedby:
1. InitializingGwithacopyofG andG whererootsaremerged(merging1 2
consistsinjoiningtypenodeswithoutremovinganyarc),
2. andthen,inrepeatedlyapplyingthefollowingtransformationstoG:
1 n 1 n(a) typenodeskofGwithdistinctsonsk:g(k ,...,k )andk:g(k ,...,k )1 1 2 2
i iwiththesamefunctorghavetheirsonsk andk pairwisemerged,1 2
1 n 1 n(b) distinct type nodes k : g(k,...,k)and k : g(k ,...,k)withthe1 21 1 2 2
7samefunctorgonanacyclicpathfromtherootaremerged .
Allsonsofatypenodemusthavedifferentfunctors,sothatthebreadthofa
typegraphisfinite.Noacyclicpathstartingfromtherootcancontainthesame
functortwice,sothatthedepthofawidenedtypegraphisfinite.Itfollowsthat
astrictlyincreasingchainoftypegraphsisfinite.
5 Combining the Galois Connection and
Widening/Narrowing Approaches to Abstract
Interpretation
InpracticebothGaloisconnectionandwidening/narrowingapproachesareused
simultaneously[CC76,CC77a].FirstaGaloisconnectionisusedtoobtainap­
proximateequationsX=F(X)onanabstractdomainL.Thegoalistoobtain
computer representable properties of programs. These fixpoint equations are
thensolvediteratively.WideningsandnarrowingsareusedwhenthedomainL
hasinfiniteorverylongstrictlyascendingchainsorevenwhenitisfinitebut
7 As noticed by [BJCD87], several solutions are possible.