(si il y a un problème dans le code compilé, il se trouve déjà dans le code C).
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
si le code C est propre et garanti c'est bien, mais si le compilateur introduit un bug c'est un peu couillon, tu ne crois pas ?
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
T'es sûr ? Tu faisais (ou fais) quoi comme travail chez Esterel ? Tu y appris quoi chez eux pour avoir écrit cela ?
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
T'as pas compris depuis le temps que ce tu qualifies de "industrielles", ce sont aussi des preuves de matheux ? ;-)
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
Tu devrais tout de même jeter un œil à la vidéo de Xavier Leroy dont j'ai donné le lien au-dessus, il y parle pendant une vingtaine de minutes du milieu de l'avionique et de ses exigences de certification.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
[^] # Re: Le cerveau n'est pas logique
Posté par Nicolas Boulay (site web personnel) . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 1.
Le bug peut être également dans le model. J'imagine que pour vérifier le comportement du C par rapport aux instructions assembleur, il faut modéliser ses instructions, ce qui n'est pas forcément simple.
J'adore ta condescendance, tu n'a aucune idée de comment le problème est géré actuellement dans de vrai projet, mais tu la ramènes quand même.
J'ai entre autre appris, que les spécialistes métiers ne sont pas des informaticiens et encore moins des matheux. Et que pour décrire leur système, ils ne veulent surtout pas avoir à faire à ce genre de concept. Ils veulent pouvoir décrire des problème spécifique, les exemples de why3 dont parlait mon commentaire, n'ont aucun rapport avec des problèmes industriels.
Tu n'as compris que la forme était le plus important pour travailler avec un tel outil, pour la compréhension même de ce qu'ils font d'un point de vue métier. C'est le sujet du journal.
C'est sûr, ce n'est pas comme si je n'avais pas déjà certifié 2 ou 3 logiciels.
"La première sécurité est la liberté"