Si le programme est suffisament simple (pas d'allocation dynamique de mémoire, pas d'appels récursifs non bornés, ...), on peut s'en sortir en modélisant le système par un automate, et les techniques de model-checking + interprétation abstraite marchent plutôt bien. Il y a pas mal de code de ce genre dans Airbus par exemple. Dans ce cas, c'est tout automatique, mais les algos sont toujours exponentiels dans le pire cas, donc, des fois, il faut 10^42 années et 10^21 peta octets de RAM pour avoir la réponse, ... L'avantage pour les systèmes matériels, c'est qu'on est toujours dans ce cas là. (t'as déjà vu une puce de silicium faire de l'allocation dynamique de mémoire ?)
Pour des programmes plus complexes, avec structures de données dynamiques, là, il n'y a pas d'algorithme qui puisse prouver le système, et on a même démontré qu'il ne pouvait pas y en avoir (c'est indécidable). Dans ce cas, on peut tenter un peu d'interpétation abstraite (polyspace fait ça par exemple, M$ a un outil comme ça en interne), qui permet de trouver certaines erreurs et de montrer qu'il n'y aura pas d'erreurs à certains endroits, mais il y a toujours des cas ou on ne peut rien dire de façon automatique. Donc, si on veut tout prouver, en effet, il faut tout faire à la main. Au niveau industriel, c'est surtout l'atelier B (ou plutôt une variante au niveau de l'interface -- basé sur Emacs ;-) -- la balbulette) qui domine, mais on peut aussi citer PVS (malheureusement réputé pour être buggé, ce qui est un comble), coq (moins de bac+12, s'abstenir. Il faut déjà pas mal de théorie pour comprendre comment démontrer que 0 != 1 ...), ... Dans tous les cas, les preuves de théorèmes, c'est très long et très chiant. J'ai passé plus d'une journée à prouver un algo de tri de tableau par insertion par exemple (bon, un mec expérimenté ira plus vite, mais y'a pas mal de boulot en tous cas.)
[^] # Re: Plex86 (ex-FreeMWare) sort en v0.1
Posté par Matthieu Moy (site web personnel) . En réponse à la dépêche Plex86 (ex-FreeMWare) sort en v0.1. Évalué à 4.
Pour des programmes plus complexes, avec structures de données dynamiques, là, il n'y a pas d'algorithme qui puisse prouver le système, et on a même démontré qu'il ne pouvait pas y en avoir (c'est indécidable). Dans ce cas, on peut tenter un peu d'interpétation abstraite (polyspace fait ça par exemple, M$ a un outil comme ça en interne), qui permet de trouver certaines erreurs et de montrer qu'il n'y aura pas d'erreurs à certains endroits, mais il y a toujours des cas ou on ne peut rien dire de façon automatique. Donc, si on veut tout prouver, en effet, il faut tout faire à la main. Au niveau industriel, c'est surtout l'atelier B (ou plutôt une variante au niveau de l'interface -- basé sur Emacs ;-) -- la balbulette) qui domine, mais on peut aussi citer PVS (malheureusement réputé pour être buggé, ce qui est un comble), coq (moins de bac+12, s'abstenir. Il faut déjà pas mal de théorie pour comprendre comment démontrer que 0 != 1 ...), ... Dans tous les cas, les preuves de théorèmes, c'est très long et très chiant. J'ai passé plus d'une journée à prouver un algo de tri de tableau par insertion par exemple (bon, un mec expérimenté ira plus vite, mais y'a pas mal de boulot en tous cas.)