Si la propriété est une spécification (totale) alors spec est déjà en quelque sorte le programme en lui-même. Si cette spec était "exécutée", par une machine, son comportement serait le même que celui du programme à vérifier.
Je comprends bien. D'où la recherche de l'écriture de spec exécutable (est ce que tu connais Scade ? c'est l'argument des LLR executable pour le vendre).
Mais il existe toujours un moment il faut spécifier ce que tu mets dans la spec. Il y a toujours une spec de spec en cascade.
Donc, il y a toujours à un moment l'écriture de quelques choses de non ambigüe et l'écriture du code final. Ce qui revient à avoir 2 "modèles", non ?
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . En réponse au journal La preuve de programme : où en est-on ?. Évalué à 2.
Je comprends bien. D'où la recherche de l'écriture de spec exécutable (est ce que tu connais Scade ? c'est l'argument des LLR executable pour le vendre).
Mais il existe toujours un moment il faut spécifier ce que tu mets dans la spec. Il y a toujours une spec de spec en cascade.
Donc, il y a toujours à un moment l'écriture de quelques choses de non ambigüe et l'écriture du code final. Ce qui revient à avoir 2 "modèles", non ?
"La première sécurité est la liberté"