SYSTEMATIC REALIZATION OF CONTROL-FLOW-ANALYSES FOR CML

We present a methodology for the systematic realisation of control flo w analyses and illustrate it for Concurrent ML. We start with an abstr act specification of the analysis that is next proved semantically sou nd with respect to a traditional small-step operational semantics; thi s result holds for terminating as well as non-terminating programs. Th e analysis is defined coinductively and it is shown that all programs have a least analysis result (that is indeed the best one). To realise the analysis we massage the specification in three stages: (i) to exp licitly record reachability of subexpressions, (ii) to be defined in a syntax-directed manner, and (iii) to generate a set of constraints th at subsequently can be solved by standard techniques. We prove equival ence results between the different versions of the analysis; in partic ular it follows that the least solution to the constraints generated w ill be the least analysis result also to the initial specification.