Taylor models and floating-point arithmetic: proof that arithmetic operations are validated in COSY

The goal of this paper is to prove that the implementation of Taylor models in COSY, based on floating-point arithmetic, computes results satisfyin- g the «containment property», i.e. guaranteed results. First, Taylor models are defined and their implementation in the COSY software by Makino and Berz is detailed. Afterwards IEEE-754 floating-point arithmetic is introduced. Then the core of this paper is given: the algorithms implemented in COSY for multiplying a Taylor model by a scalar, for adding or multiplying two Taylor models are given and are proven to return Taylor models satisfying the containment property.L'objectif de ce travail est de démontrer que l'implantation des modèles de Taylor, telle qu'elle est réalisée dans le logiciel COSY, calcule des résultats qui sont garantis, c'est à dire qu''ils satisfont la propriété d'inclusion.Tout d'abord, les modèles de Taylor sont définis et leur implantation par Makino et Berz dans le logiciel COSY est détaillée. Ensuite l'arithmétique flottante, telle qu'elle est spécifiée par la norme IEEE-754, est présentée. Enfin on arrive au cœur du sujet : les algorithmes implantés dans COSY pour la multiplication d'un modèle de Taylor par un scalaire et pour la somme et le produit de deux modèles de Taylor sont donnés; il est démontré que ces algorithmes retournent de s modèles de Taylor qui satisfont la propriété d'inclusion