Dans les faits, une spec ne couvre jamais entièrement tous les comportements, il y a toujours un paquet de troues que l'on voit (ou pas) lors d'une implémentation.
Une preuve formelle automatique, a besoin d'avoir la spec entière, ce qui peut être plus difficile à faire qu'un code correct. Souvent, on a juste besoin que le code ne plante jamais (pas d'exception), ni que les données soient corrompues.
[^] # Re: On verra
Posté par Nicolas Boulay (site web personnel) . En réponse à la dépêche Core Infrastructure Initiative. Évalué à 2.
Dans les faits, une spec ne couvre jamais entièrement tous les comportements, il y a toujours un paquet de troues que l'on voit (ou pas) lors d'une implémentation.
Une preuve formelle automatique, a besoin d'avoir la spec entière, ce qui peut être plus difficile à faire qu'un code correct. Souvent, on a juste besoin que le code ne plante jamais (pas d'exception), ni que les données soient corrompues.
"La première sécurité est la liberté"