<<Non, en fait il s'agirait de générer, pour un algorithme, à partir de ses contrats, une preuve en B que l'algo respecte les contrats.>>
Mmmh infaisable.
Enfin générer le modèle B à partir du code et des contrats associé ce n'est pas un probleme : le B étant très expressif.
Mais tu va te retrouver avec un modèle beaucoup trop compliqué et qui n'utilise pas le raffinement. Le prouveur automatique n'aura aucune chance de trouver les preuves.
Hors l'interet principal de B est de distribuer la complexité des preuves en créant plusieurs modèle qui se raffinent les un les autres. Mais écrire ces raffinement demande une réflexion humaine. Pas possible de la faire faire par le compilo.
Plus généralement ca fait depuis 1960-70 qu'il existe des méthodes pour certifier les programmes. Hors cela n'a pas révolutionné l'informatique. Pourquoi ? car tous ces problèmes sont indécidables. Dans certain (model checking) on peut se ramener a un problème NP-complet, mais on est quand même coincé par la complexitée du travail. Il ne faut pas s'attaquer a ca avec naiveté, sans vouloir te vexer.
[^] # Re: Comment faire un langage plus rapide que C ?
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é à 3.
Mmmh infaisable.
Enfin générer le modèle B à partir du code et des contrats associé ce n'est pas un probleme : le B étant très expressif.
Mais tu va te retrouver avec un modèle beaucoup trop compliqué et qui n'utilise pas le raffinement. Le prouveur automatique n'aura aucune chance de trouver les preuves.
Hors l'interet principal de B est de distribuer la complexité des preuves en créant plusieurs modèle qui se raffinent les un les autres. Mais écrire ces raffinement demande une réflexion humaine. Pas possible de la faire faire par le compilo.
Plus généralement ca fait depuis 1960-70 qu'il existe des méthodes pour certifier les programmes. Hors cela n'a pas révolutionné l'informatique. Pourquoi ? car tous ces problèmes sont indécidables. Dans certain (model checking) on peut se ramener a un problème NP-complet, mais on est quand même coincé par la complexitée du travail. Il ne faut pas s'attaquer a ca avec naiveté, sans vouloir te vexer.