ça se fait avec un AGL qui tourne entre autre sous Linux mais qui coûte super cher ...
fonctionnement : en gros tu lui donne des spécifications (très mathématique : thérories des ensemble et relations, pas trop compliqué), l'AGL essaye de prouver qu'elles sont exactes, ensuite il faut rapprocher les specs de structure plus "informatiques" : c'est l'implémentation, et une fois que l'AGL
arrive à prouver que les specs et la pseudo implémentation sont prouvées, il te pisse le code en C/ADA/... avec makefile et tout le toutim et t'as du code prouvé ... (pas besoin de faire de test)
ça c'est la thérorie....
/!\ : rien que le fait d'évoquer cet méthode va faire frémir certains d'entre vous...
[^] # Re: pas une preuve
Posté par kolter (site web personnel, Mastodon) . En réponse au journal couverture de code. Évalué à 2.
La méthode B : http://www.atelierb.societe.com/(...)
ça se fait avec un AGL qui tourne entre autre sous Linux mais qui coûte super cher ...
fonctionnement : en gros tu lui donne des spécifications (très mathématique : thérories des ensemble et relations, pas trop compliqué), l'AGL essaye de prouver qu'elles sont exactes, ensuite il faut rapprocher les specs de structure plus "informatiques" : c'est l'implémentation, et une fois que l'AGL
arrive à prouver que les specs et la pseudo implémentation sont prouvées, il te pisse le code en C/ADA/... avec makefile et tout le toutim et t'as du code prouvé ... (pas besoin de faire de test)
ça c'est la thérorie....
/!\ : rien que le fait d'évoquer cet méthode va faire frémir certains d'entre vous...
m'enfin ça me rapelle quelques souvenirs...
M.