L’emploi de la preuve garantit qu’il n’y aura pas de distorsion entre le modèle mathématique initial, issu de la spécification écrite en français, et le modèle mathématique final, extrêmement proche du code exécutable. Mais, en deçà et au-delà, rien n’est garanti par la preuve. Si, par exemple, la spécification en français est erronée ou si le modèle mathématique initial n’est pas fidèle à cette spécification, on sort des limites de l’épure. De même, si le traducteur qui transforme le dernier modèle mathématique en code ou si le compilateur qui le traduit en code binaire sont bogués, on ne peut rien garantir. Le zéro défaut absolu n’existe pas. Mais on peut s’en approcher toujours plus. Ce que l’on peut faire avec une méthode formelle va certainement beaucoup plus loin que ce que lon peut garantir avec des tests unitaires. Mais il ne faut pas croire que le problème est résolu dans son ensemble : le retour de bâton serait terrible.
🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.
