Les Tests Ne Prouveront Jamais Que Deux Fonctions Sont Équivalentes. Voici Ce Qui Le Peut.
La programmation N-version part du principe que vos implémentations sont d'accord. Nous voyons pourquoi les tests ne suffisent pas, comment les solveurs SMT peuvent prouver l'équivalence, et où tracer la ligne entre 'suffisamment bon' et 'formellement vérifié'.
Vous avez construit un système N-version. Trois implémentations indépendantes de la même fonction critique, un votant qui choisit le résultat majoritaire, et…