Jean-Raymond Abrial (inventeur de la méthode B): ” Il y a lieu d’être prudent “
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 … Lire la suite
