Le dernier aspect, celui de l'implémentabilité, est le plus drole. On peut le résumer ainsi : "Machine de Turing complète". En d'autres termes si on fait fi du temps d'éxecution et de l'occupation mémoire on peut écrire un programme en C pour tout algorithme calculable. Au final tout est implémentable. Mais il y a un hic, aucun programme au monde ne pourra jamais prendre en entrée un n'importe quel autre programme et déterminer si oui ou non celui ci va finir. Ce problème est dit 'non décidable'. Pour résumer : pour valider de façon certaine une implémentation il faut la "prouver". Le problème de la preuve est un problème complexe, sur un OS évolué, le plus simple des programmes peut se retrouver mis continuellement en attente par des jeux d'interruptions, de priorités et de blocages de ressources qui font qu'il ne se terminera jamais. Donc l'implémentation du plus simple des programmes Linux est fausse.
Un algorithme complexe et nouveau vient souvent avec sa preuve decidabilite sur un modele d'execution abstrait. Pour les systemes critiques, on peut avoir des preuves plus formelles, voir des preuves vis-a-vis du materiel sous-jacent. Ca me parait etre une condition suffisante de son implementabilite. Surtout si en plus une implementation effective est donnee (voire avec ses parties critiques prouvees formellement).
[^] # Re: Il va falloir arreter les anneries très vite.
Posté par Burps . En réponse à la dépêche Lettre du président de la FSF Europe à l'EICTA au sujet des brevets logiciels. Évalué à 2.
Un algorithme complexe et nouveau vient souvent avec sa preuve decidabilite sur un modele d'execution abstrait. Pour les systemes critiques, on peut avoir des preuves plus formelles, voir des preuves vis-a-vis du materiel sous-jacent. Ca me parait etre une condition suffisante de son implementabilite. Surtout si en plus une implementation effective est donnee (voire avec ses parties critiques prouvees formellement).