L'arithmétique des ordinateurs et sa formalisation