Optimality in goal-dependent Analysis of Sharing

We cope with the problem of correctness and optimality for logic programs analysis by abstract interpretation. We refine the goal-dependent framework appeared in [CF99] by fixing a result of correctness and introducing two specialized operators for forward and backward unification. We provide the best correct abstractions of the concrete operators in the case of set-sharing analysis. We show that the precision of the overall analysis is strictly improved and that, in some cases, we gain precision w.r.t. more complex domains involving linearity and freeness information.