C'est très (trop?) rigide mais au moins si ta spec est correcte, ton truc sera bon du premier coup - du moins en théorie, et probablement dans la pratique avec beaucoup d'expérience.
En fait, si tu réalise vraiment un développement formel (un complet), ton logiciel correspond aux spec par preuve. Bon, ce qui arrive souvent par contre, c'est que tu fasses une spec, que tu commence les preuves, que tu t'aperçoives qu'elles sont impossibles/ignobles, tu cherches une manière plus élégante de construire ta spec, etc. Le cycle se fait plus à ce niveau. Et pour ce qui est de la rigidité, j'appelerais plutôt cela de la rigueur : tu as un modèle et ton programme y correspond exactement.
[^] # Re: Balèse?
Posté par Fanf . En réponse à la dépêche Prologin Edition 2005. Évalué à 2.
En fait, si tu réalise vraiment un développement formel (un complet), ton logiciel correspond aux spec par preuve. Bon, ce qui arrive souvent par contre, c'est que tu fasses une spec, que tu commence les preuves, que tu t'aperçoives qu'elles sont impossibles/ignobles, tu cherches une manière plus élégante de construire ta spec, etc. Le cycle se fait plus à ce niveau. Et pour ce qui est de la rigidité, j'appelerais plutôt cela de la rigueur : tu as un modèle et ton programme y correspond exactement.