On commence par un modèle abstrait général qui pose le but a atteindre.
On prouve qu'il est cohérent
On écrit un modèle qui raffine le premier en rajouter des detail, par exemple la forme générale de l'implémentation.
On prouve qu'il raffine le premier modèle, c'est à dire qu'il fait la même chose. On prouve qu'il est cohérent.
Et ansi de suite jusqu'a obtenir un modèle avec la precision souhaitée.
Si on le souhaite on peut aller jusqu'a la précision requise pour une implémentation. Dans ce cas on peut générer le code automatiquement. Le code est assez crade en effet, mais ce n'est pas très grave vu qu'il est correcte par contruction pas besoin de le débugger.
Mais il ne faut pas réver, trouver une preuve est un problème indécidable. Il y a un prouveur dans les outils qui arrive faire les plus faciles mais il faut faire les plus complexes à la main. Au final il faut s'accrocher et le temps pour faire tout cela est long mais on arrive a un logiciel 100% certifié.
Pour info cette méthode a déjà été utilisée dans l'industrie, par exemple pour réaliser le logiciel qui pilote le metro parisien METEOR
[^] # Re: qques questions sur Lissac et... Ruby, Java, Caml...
Posté par Joris R (site web personnel, Mastodon) . En réponse à la dépêche 23 mars: Conférence au LORIA sur Lisaac, un nouveau langage. Évalué à 1.
On commence par un modèle abstrait général qui pose le but a atteindre.
On prouve qu'il est cohérent
On écrit un modèle qui raffine le premier en rajouter des detail, par exemple la forme générale de l'implémentation.
On prouve qu'il raffine le premier modèle, c'est à dire qu'il fait la même chose. On prouve qu'il est cohérent.
Et ansi de suite jusqu'a obtenir un modèle avec la precision souhaitée.
Si on le souhaite on peut aller jusqu'a la précision requise pour une implémentation. Dans ce cas on peut générer le code automatiquement. Le code est assez crade en effet, mais ce n'est pas très grave vu qu'il est correcte par contruction pas besoin de le débugger.
Mais il ne faut pas réver, trouver une preuve est un problème indécidable. Il y a un prouveur dans les outils qui arrive faire les plus faciles mais il faut faire les plus complexes à la main. Au final il faut s'accrocher et le temps pour faire tout cela est long mais on arrive a un logiciel 100% certifié.
Pour info cette méthode a déjà été utilisée dans l'industrie, par exemple pour réaliser le logiciel qui pilote le metro parisien METEOR