Je confirme, « l’inspection de code formel » de McConnell n'a rien à voir avec les analyses statiques et notamment les méthodes formelles. Le « formel » dans l'inspection de code, c'est qu'on suit une procédure codifiée.
Côté analyses statiques, on distingue les approches non formelles, les bug finders et les approches formelles comme Astrée, Frama-C, la Méthode B, SPARK, etc. Les deux sont utiles, les bug finders sont plus facile à utiliser mais pouvant donner des faux positifs ou des faux négatifs. Les approches formelles donnent des garanties plus fortes (si pas d'alarme alors le logiciel est garanti sans un certain type de fautes) mais sont plus difficiles à utiliser (mais largement utilisables pour certains).
Pour ceux que ça intéresse, je maintiens une liste de tous les outils libres formels. Il y a de tout, de logiciels ultra spécialisés à des environnements de développement et preuve pour une approche particulière : gulliver.eu.org/free_software_for_formal_verification.
PS : Je ne vois pas le graphe, pourtant j'ai installé le certificat. Je vois bien les avatars.
[^] # Re: Méthodes formelles
Posté par David Mentré (site web personnel) . En réponse à la dépêche [code] Trouver les erreurs. Évalué à 6.
Je confirme, « l’inspection de code formel » de McConnell n'a rien à voir avec les analyses statiques et notamment les méthodes formelles. Le « formel » dans l'inspection de code, c'est qu'on suit une procédure codifiée.
Côté analyses statiques, on distingue les approches non formelles, les bug finders et les approches formelles comme Astrée, Frama-C, la Méthode B, SPARK, etc. Les deux sont utiles, les bug finders sont plus facile à utiliser mais pouvant donner des faux positifs ou des faux négatifs. Les approches formelles donnent des garanties plus fortes (si pas d'alarme alors le logiciel est garanti sans un certain type de fautes) mais sont plus difficiles à utiliser (mais largement utilisables pour certains).
Pour ceux que ça intéresse, je maintiens une liste de tous les outils libres formels. Il y a de tout, de logiciels ultra spécialisés à des environnements de développement et preuve pour une approche particulière : gulliver.eu.org/free_software_for_formal_verification.
PS : Je ne vois pas le graphe, pourtant j'ai installé le certificat. Je vois bien les avatars.