SCADE est souvent utilisé dans les fadec, mais il n'y a aucune "preuve". Le langage est formel dans le sens ou il ne > comporte pas d’ambigüité. Et le compilo est certifié.
Tout ce que tu dis est vrai (et pour cause !), je préciserais simplement que "ne pas comporter d'ambigüité" veut dire qu'on peut donner au langage une sémantique formelle claire. Ça va aussi avec un certain nombre d'articles de recherche présentant le langage et diverses techniques de compilation de façon très propre. Un compilateur prouvé correct en Coq pour une version très antérieure de SCADE, Lustre, a d'ailleurs été récemment présenté à la conférence PLDI.
[^] # Re: Le cerveau n'est pas logique
Posté par auve . En réponse au journal Pourquoi la recherche en langages de programmation ?. Évalué à 3.
Tout ce que tu dis est vrai (et pour cause !), je préciserais simplement que "ne pas comporter d'ambigüité" veut dire qu'on peut donner au langage une sémantique formelle claire. Ça va aussi avec un certain nombre d'articles de recherche présentant le langage et diverses techniques de compilation de façon très propre. Un compilateur prouvé correct en Coq pour une version très antérieure de SCADE, Lustre, a d'ailleurs été récemment présenté à la conférence PLDI.