Discussion :

[Piotrek]

Ce serait intéressant que tu expliques un peu plus de quoi il s'agit, en particulier en expliquant les termes que tu emploies. (J'ai visité les deux pages de Wikipedia que tu cites; elles restent elles-mêmes assez floues sur les concepts qu'elles sont sensées définir.)

Effectivement c'est imprécis:
- J'ai toujours eu des difficultés a définir précisement quelque chose
- Je n'ai malheureusment pas la connaissance de votre grammaire (mathematique, theorique etc)
- Le méchanisme de validation de preuve n'est pas quelque chose que je cherchais a créer, c'est un effet d'une partie du sytème de ce que j'ai crée (qui est totalement deterministe)

Du coup en me concentrant sur la preuve (oublions la grammaire un instant), imaginons que nous souhaitions prouver le bon fonctionnement d'une application de gestion par exemple, la TVA.

La TVA est définie:
- C'est un nombre
- Qui ne peut être inferieur a zero
- Qui ne peut être superieur a 100, rarement superieur a 70
- Qui doit etre calcule a des moment précis en fonction de formules précies

En ayant défini le reste de ce que gere l'application de gestion (le prix, la quantité etc) on se retrouve avec des ensembles d'états a des moments precis.
A un état, correspond un certain nombre de variables, leurs contraintes et leurs formules associées. On peut tenter de prouver l'état, trouver les situations possibles ou il y a risque d'erreur (une division par zero) et y remédier en definissant des règles additionnelles pour l'etat lui même.

Je suppose que tu entends par méta-données des données qui vont servir à générer des programmes. Est-ce bien cela ?

Dans mon cas, je ne considere la génération que comme un mal nécessaire (masquer des definitions sophistiquées comme les règles d'attribution d'un crédit par une banque par exemple) ou tout simplement pour des raisons de performances. Le systeme est conçu pour interpréter les règles pendant l'execution, en temps réel.

Nous avons donc un domaine (l'application de gestion) avec son vocabulaire (Tva, prix quantite...) et sa grammaire (l'ensemble des regles, actions, réactions). L'originalité du systeme est qu'il peut gerer l'interaction entre des domaines.

Cependant votre methode reste la meilleure,
- mon "moteur" devant être prouvé (prouver qu'une demarche de recherche preuve marche )
- votre solution ne pouvant etre pervertie (dans la mienne on peut se mettre les arrondis de TVA dans la poche).

[DrTopos]

Le systeme est conçu pour interpréter les règles pendant l'execution, en temps réel.

Peux-tu (sans pour autant dévoiler ce que tu ne désires pas dévoiler) donner un exemple précis de règle utilisée par ton système ? Je pense que cela permettrait de mieux comprendre.

[Piotrek]

Sans entrer dans le détail il existe plusieurs types de domaines

Par exemple pour les objets métier, il existe plusieurs déclancheurs de règles qui interviennent tout au long de la vie de chaque objet: déclanchement au chargement, a l'affichage, avant la tentative de modification d'une de ses propriétés, apres la modification d'une de ses propriétés, avant la sauvegarde, apres la sauvegarde... et j'en oublie
Si il existe une règle a un moment precis pour la cible de la modification (l'objet lui-meme ou une de ses propriétés), les règles sont appliquées dans l'ordre specifié.

L'application de la règle consiste a parcourir un arbre décisionnel composé de:
- regles (mathematiques si le type ciblé est numerique) produisant un resultat
- d'actions sur l'environnement (sous forme de metadonnee par exemple)

Si tout se passe bien, l'objet est considére comme valide.
Bien sur je ne vous ai pas donne tous les détails mais il y a un mode transactionnel portant sur la modification de plusieurs objet, ou lorsque l'ecriture de celui-ci n'est pas homogène...

Voilà pour ce qui est du domaine de l'objet métier a proprement dit, une facture avec une TVA par exemple.
Ai-je repondu a votre question?

[DrTopos]

J'ai l'impression que ton système est un système expert. En général, ce genre de système n'apporte pas de preuve (encore que cela puisse arriver dans certains cas). Il apporte plutôt (comme son nom l'indique) une expertise, c'est-à-dire un avis qui peut être plus ou moins pertinent suivant la qualité du système expert.

Si tout se passe bien, l'objet est considére comme valide.

Considéré. Il s'agit donc bien d'un avis. Je ne penses pas qu'on puisse parler de preuve dans ce cas. A moins bien sûr que les règles (l'arbre décisionnel) soient faites de telle façon qu'il n'y ait jamais aucun doute sur les décisions à prendre.

En fait, on doit pouvoir mesurer la pertinence d'un système expert au pourcentage de reponses correctes qu'il apporte. Mais même si ce pourcentage est de 100%, je ne pense pas qu'on puisse parler de preuve, car une fois de plus ce genre de mesure ne repose que sur des tests.

En tout cas, je suis très admiratif à l'égard de tous les gens qui se lancent dans des projets de cette envergure.

[Piotrek]

Effectivement, pas de preuve possible. A moins, d'effectuer une demonstration mathématique dans un ensemble de valeurs fini, lors de la conception de la règle, et comme c'est pas toujours possible...

Cependant comme je considère aussi le language de programmation dudit systeme comme un ensemble de domaines, avec grammaires, vocabulaires et règles, je vais tres serieusement considerer la generation de code sous Anubis!

Pour les autres curieux, je metterais ce que j'ai fait en ligne dans... heu assez longtemps

Merci a vous DrTopos

[DrTopos]

Cependant comme je considère aussi le language de programmation dudit systeme comme un ensemble de domaines, avec grammaires, vocabulaires et règles, je vais tres serieusement considerer la generation de code sous Anubis!

Pour les autres curieux, je metterais ce que j'ai fait en ligne dans... heu assez longtemps

Ce sera aussi un excellent test pour Anubis lui-même.

On peut bien sûr mettre en ligne sur DVP. Toutefois je signale qu'il est prévu (ce n'est pas encore fait, mais ça ne saurait tarder) une série de pages spéciales sur le site d'Anubis pour le partage des source (un peu dans le style 'The Code Project').

A bientôt donc et bon courage.

[Rafy]

Un des trucs les plus important pour éviter le plus possible les bugs est la clareté :
Du code mal indenté, voir pas indenté.
Des noms de variable sans sens.
Et tant d'autre petites choses altère très facilement la compréhension du code et donc la facilité du deboggage.
Donc avec un code lisible, je pense qu'il est facile déjà d'éviter pas mal de bugs....

[DrTopos]

Un des trucs les plus important pour éviter le plus possible les bugs est la clareté :
Du code mal indenté, voir pas indenté.
Des noms de variable sans sens.
Et tant d'autre petites choses altère très facilement la compréhension du code ....

Tout à fait d'accord, et ceci même si le programme est formellement prouvé, car formellement correct ne veut pas forcément dire compréhensible et clair (pour l'humain), ni même que les intentions du programme (ce pour quoi il a été fait) sont les bonnes.

[outs]

Merci pour ces précisions. Si j'ai dit 'en particulier dans le train' c'est parce que je savais qu'ils utilisent B pour le train, mais je ne savais pas que c'était exclusif.

ha! ca c'est pas très gentil pour toutes la communauté des utilisateurs de B. En particulier je peux citer Citroen dans la liste des utilisateur de la méthode. Mais elle est utilisé par beaucoup (facon de parler) d'industriel de manière ponctuelle. Par exemple pour formaliser les appareillage de mesures de la qualité du signal de la TNT (télévision numérique terrestre) ou alors j'ai un autre exemple pour la conception d'un controleur numérique sur une presse industrielle (les énormes machin qui travaillent du métal).

Mais seul la RATP et ces fournisseurs l'utilise de manière aussi intensive et systèmatique, de plus le projet Meteor a une place importante dans l'histoire et la génèse de la méthode B. Pour info les partenaire comme alstom quand il concoivent une machine comme le metro automatique météor écrivent des modèles B. Ensuite la RATP reprend tout ces modèle et refait la preuves pour valider le travail réalisé. D'ailleur l'utilisation de méthodes formelles pour les dispositifs informatiques ayant trait aux transport de personne est obligatoire (ou fortement recommandé je ne sais plus) d'un point de vue légal.

Maintenant, quand tu dis que c'est 'pour une raison de coût', tu veux bien dire que l'utilisation de B diminue les coûts, ou bien tu veux dire le contraire ? Ce n'est pas clair d'après ta réponse. Ce serait bien de préciser.

Là aussi, il serait intéressant que tu donnes quelques précisions. Je ne connais pas les résultats dont tu parles (je ne suis sans doute pas le seul). En particulier ce serait bien que tu expliques clairement le lien avec l'utilisation du B (ou autre système à preuve) et le coût.

Il faut comprendre un truc :
-si vous utilisez la méthode B sur un logiciel classique cela va évidement augmenter les couts : dificulté de trouver quelqu'un de qualifié, difficulté intrinseque de la démarche donc lenteur, cout des outils supportant les méthode etc.
-mais si vous utiliser la méthode pour un travail comportant des difficulté pour tester votre software comme par exemple du matériel electronique, un logiciel embarqué dans un moyen de transport comme un train ou un avion alors les phases de test peuvent couter très très cher (dégradation du matériel, frais de remboursement du client, difficulté des test en grandeur nature). Dans cette optique les méthode formelles font economiser de l'argent.

Par exemple quand ils ont testé le pilote automatique du métro, ils ont mis le courant de la rame et cela a marché du premier coup. Les portes se sont ouvertes, fermée, le train est partit et il s'est arreté tout seul. Et cela directement sans bug gràce à l'utilisation du développement prouvé.

PS: Je suis en train de parcourir le fil de discussion. Et une chose ma choqué : il faut absolument dissocier les preuves de programmes informatique (aka les méthodes formelles) et les programmes en eux même. L'activité de validation ou de développement prouvé n'a rien a voir avec le fait d'utiliser des noms de variables explicites ou d'autres bonnes pratiques de programmation.

[DrTopos]

-mais si vous utiliser la méthode pour un travail comportant des difficulté pour tester votre software comme par exemple du matériel electronique, un logiciel embarqué dans un moyen de transport comme un train ou un avion alors les phases de test peuvent couter très très cher (dégradation du matériel, frais de remboursement du client, difficulté des test en grandeur nature). Dans cette optique les méthode formelles font economiser de l'argent.

Ceci confirme le message que je voulais faire passer: mieux vaut prévenir que guérir (et en plus cela peut couter moins cher).

Par exemple quand ils ont testé le pilote automatique du métro, ils ont mis le courant de la rame et cela a marché du premier coup. Les portes se sont ouvertes, fermée, le train est partit et il s'est arreté tout seul. Et cela directement sans bug gràce à l'utilisation du développement prouvé.

Moi, je trouve ça super.

PS: Je suis en train de parcourir le fil de discussion. Et une chose ma choqué : il faut absolument dissocier les preuves de programmes informatique (aka les méthodes formelles) et les programmes en eux même. L'activité de validation ou de développement prouvé n'a rien a voir avec le fait d'utiliser des noms de variables explicites ou d'autres bonnes pratiques de programmation.

Sans doute. Malgré tout il y a quand même un lien entre preuves et programmes. Avec la méthode B, les preuves ne produisent pas de programme. Elles servent seulement à s'assurer que les programmes sont corrects (satisfont leurs spécifications). Par contre, il y des systèmes dans lesquels les preuves (celles qui sont constructives) peuvent être éventuellement transformées en programmes. En ce sens, il y a quand même un lien.

Ceci-dit, le sujet de ce fil était largement ouvert. C'est pourquoi on a aussi discuté des moyens d'éviter les bugs quels que soient ces moyens.

Merci pour ta contribution qui nous éclaire sur le système B. Toute nouvelle précision sur le B ou son histoire est bien venue. C'est un système très intéressant, et en même temps très bien en phase avec la réalité.

[outs]

Ben en fait les preuves B (étant classique) ne peuvent pas produire de code mais les modèles une fois qu'ils sont déterministes et suffisament détaillés peuvent être traduit automatiquement en C ou en ADA. D'ailleur le résultat est loin d'être lisible mais il est certifié.

Par contre, il y des systèmes dans lesquels les preuves (celles qui sont constructives) peuvent être éventuellement transformées en programmes. En ce sens, il y a quand même un lien.

Bien sur mais avant de pouvoir parler de l'isomorphisme de curry-howard, il va falloir bien faire comprendre ce qu'est une logique ou un spécification sinon le débat ne prendra pas, enfin tu l'a surement déjà fait dans les pages que je n'ai pas encore lu (c'est lourd a lire 6 pages ).

Sinon il y a plein de choses a citer comme
-les model checkers qui représentent l'approche la plus classique et peut être la plus mature, malgré des limitation fondamentales importantes. Utilisé un peu partout ou c'est possible, par exemple pour certaines propriétés des pilotes de matériels, ou alors des propiétés de communication ou de non blocage.
-L'interprétation abstraite qui extrait des informations pertinentes d'un programme pour en certifier un aspect. Par exemple utilisé sur le nouvel airbus pour détecter les dépassements de capacité des nombres. (mais il n'y a pas d'utilisation systèmatique de méthodes formelles a ma connaissance dans ce projet, on reste encore avec la technique des systèmes informatiques redondant concu par des équipes indépendantes)
-les approches basé sur la correspondance entre les preuves constructives et le programmes fonctionelles. Chose que tu a déjà abordé. Par contre je n'en connais pas d'applications industrielles ?
-les apporches utilisant plutot la force brutes des preuves avec des outils comme Coq. Plutôt réservé aux matématiciens/logicien avertis à cause de la difficultée et des logiques très pointues.

[siplusplus]

Bonjour,

Je ne sais pas si ce post est résolu ou pas alors en attendant
de (re)développer le sujet voici deux liens, vivement recommandés,
qui aideront à orienter la discussion.

Le premier lien concerne les rôles mathématiciens/informaticiens,
c'est un livre qui aborde la programmation python dont
l'auteur est Gerard Swinnen "Apprendre à programmer avec Python" qu'on trouve dans les cours et tutoriels Python.
La partie qui nous concerne se trouve au point 1.1 du 1er chapitre.

Le second lien concerne la question initiale.
C'est le théorème d'incomplétude de Gödel:
http://fr.wikipedia.org/wiki/Th%C3%A..._de_G%C3%B6del

Après cela je donnerai mon point de vue.
Bien que j'aie lu qu'une partie, il me faut un peu de temps pour
digérer tout ces messages .


A bientôt.

[grunt2000]

DrTopos, KilVaiDen, ainsi que de nombreux autres posteurs ont nettement contribué à cerner la question, aussi la présentation de mes propres pratiques aura nettement moins de force que tout ce que j'ai pu lire auparavant.

Je suis convaincu que les preuves de programmes aident à l'élaboration d'applications solides. Que sans celles-ci, elles ne peuvent croître très longtemps sans s'écrouler ou réclamer une maintenance corrective très élevée.

Cependant, force est de constater que dans une équipe de développement où sont représentés des domaines de compétence variés (untel plus adroit dans la réalisation d'IHM, un autre dans la sécurité, etc.), il serait vain d'essayer d'obtenir des gens qu'ils fassent des démonstrations mathématiques de la sûreté de leurs réalisations.
Si l'on est particulièrement maladroit dans la formulation de ses demandes de preuves dans son équipe de développement, on peut même provoquer un rejet total des preuves de toutes natures qu'elles soient. Et alors, on a tout perdu.

Il s'agit donc de rester suffisamment simple.
Je n'ai jamais cherché, par exemple, à mettre en place des démonstrations d'invariants de boucle basés sur des formules mathématiques à base de récurrence, comme la théorie veut parfois que cela soit fait, mais me semble à moi, un voeu pieux.
En revanche, expliquer qu'une série d'actions entreprises dans une boucle doit aboutir à la fin de chaque itération à un état donné, que l'on peut vérifier par une assertion, me semble beaucoup mieux supporté.

Eviter dans la programmation courante les mathématiques autant que possible, à cause de leur côté repoussoir, dissuasif.

On pourra s'opposer par des pré-conditions à toute levée d'exception non checkée qui pourrait advenir (pour java: de type Runtime: NullPointerException, IllegalArgumentException, IllegalStateException...).
Les autres types d'exceptions, checkées, seront traitées le plus finement possible, mais elles n'entrent pas directement dans le problème des preuves même si elles contribuent beaucoup à la justesse et à la stabilité d'un logiciel.

Par ailleurs, il me semble qu'une bonne pratique consiste à placer dans son programme des commentaires qui énoncent ce qu'en termes métiers les quelques prochaines lignes vont avoir l'intention de faire. A la fin du bloc d'instructions, en faire la démonstration par une assertion.

[Garulfo]

[...]Maintenant, un test ne constitue pas une preuve (de même qu'une expérience de physique ne saurait se substituer à une preuve mathématique), sauf peut-être dans les rares cas où il peut être complètement exhaustif (model checking).[...]

En fait, même pas. Le model checking est, littéralement, la vérification de modèle. Tu n'as donc pas prouvé que ton programme fait ce que tu veux, mais que le modèle de ton programme vérifie certaines propriétés. Si ton modèle est faux, tu as raté ce que tu voulais faire. Il existe des systèmes pour faire de la vérification de programmes (e.g. Verisoft ou pathfinder) mais on est très loin de qqs choses de vraiment fonctionnelles pour une majorité de cas. Autre problèmatique, mais qui est aussi valide dans le cas de la preuve, c'est, qu'au mieux, on établit qu'une propriété est vérifiée, mais on ne peut trouver ce qui ne va pas si ce n'est pas contradictoire avec les propriétés établies. On retourne toujours à l'ingénierie des besoins et à la spécification des besoins: éliciter correctement l'ensemble des besoins, décrire correctement les propriétés qui permettront de les rencontrer.

[gorgonite]

ce fil a l'air passionnant, même si je ne l'ai que survolé


1) je plussoie entièrement les propos de Garulfo :
De nombreux systèmes de preuves de programmes sont basés sur des modèles, et ne pourront donc pas empêcher les problèmes liés aux inadéquations du modèle avec la réalité...

2) il faut savoir que de nombreux systèmes existent, et sont utilisés sur des cas pratiques (voire même dans l'industrie)

• Lustre (techniques d'inférences de type) déjà cité par Dr Topos, utilisé pour le dataflow des systèmes réactifs
• Esterel également pour les systèmes réactifs (je ne connais pas trop la théorie sous-jacente... je crois que c'est un modèle concurrent synchrone )
• Blast (model checking)
• Astrée qui utilise de l'interprétation abstraite

je n'ai cité que quelques exemples... mais ça montre bien que cela existe réellement, et que l'on utilise dans l'industrie


3) il existe d'autres méthodes qui consistent à s'assurer de tout ce bon fonctionnement, ces preuves, etc à la compilation (donc avant les tests)... ce qui serait possible avec des langages "de description" (même si ce n'est pas exactement le terme) comme Lava (via interprétation monadique vers le système de preuves adéquat) et SystemC (via "compilation" vers ce qu'il faut)

[PINGOUIN_GEANT]

A propos du model checking sur les langages de modélisation. Notez qu'il faut à côté un générateur de code (certifiable si on a certaines contraintes ). Ce n'est pas le code Lustre qui est mis dans les calculateurs embarqués.
Le model checking a toutefois ses limites aujourd'hui (notamment les provers ne sont pas très performants) et on a toujours besoin de la simulation

Un truc comme CAVEAT est différent.

Au final, les gens te disent qu'il codent directement en assembleur pour être sûrs de ce qu'ils font

[InOCamlWeTrust]

Je n'ai pas tout lu, mais je peux dire ce que l'on fait chez Airbus.

Concernant les programmes, ils sont entièrement écrits en Lustre, langage trivial à prouver, dont le compilateur lui-même a été prouvé, car écrit en Objective Caml, le compilateur Objective Caml étant lui-même prouvé... et écrit en Objective Caml. Le programme de preuve, Coq je pense, s'est prouvé lui-même, et comme il a aussi été écrit en Objective Caml, la boucle est bouclée !

Les seules parties écrites en C dans le code embarqué concernent les entrées-sorties, que l'on ne peut pas faire en Lustre.

Concernant l'ordonnancement, on utilise des techniques sur lesquelles on a des résultats garantissant lo bon ordonnancement des processus, et parfois l'optimalité de l'ordonnancement.

Afin de connaître le temps processeur (donc le nombre de cycles d'horloges nécessaire), les ingénieurs ont à disposition des programmes reconstruisant au transistor près les processeurs sur lesquels les programmes embarqués tournent, ce qui leur permet de pouvoir simuler le programme de façon extrêmement précise : l'évaluation du temps est donc très pointue.

Au niveau des calculateurs, on en met suffisament pour que la probabilité de panne horaire soit inférieure ou égale à 10e-9 (si je me souviens bien). Ceci implique de la redondance matérielle assez sévère parfois, mais elle s'est toujours avérée nécessaire, car il s'est toujours produit des cas où la fonctionnalité concernée ne fonctionnait qu'avec un calculateur (parfois 1 sur 3).

Par exemple, les calculateurs de commande de déflection (les ELACS sur l'A320 si je me souviens bien) sont tripliqués, les capteurs sont doublés et chaque manche contient trois mêmes capteurs de mouvement.

La redondance s'exprime aussi par le fait que chaque calculateur fait tourner un programme écrit par une équipe différente (on ne sait jamais, au cas où il y aurait un bug sur l'un des calculateurs, afin de ne pas le retrouver sur les autres).

Les processeurs sont achetés en masse lors de la conception de l'avion (donc les 386 montés sur les A320 d'aujourd'hui ont été fabriqués dans les années 80), et sont conservés dans de grands hangars refroidis, à higrométrie constante, et tout le tralala...

Voilà : ça couvre un sujet un poil plus vaste que le sujet initial, mais ça permet aussi d'illustrer. Moralité : je pourrai demain soir prendre mon A320 d'Air France tranquille !


P.S.: les méthodes employées par Boeing ne reposent pas sur des langages aussi facilement prouvables que Lustre.

[InOCamlWeTrust]

2) il faut savoir que de nombreux systèmes existent, et sont utilisés sur des cas pratiques (voire même dans l'industrie)

• Lustre (techniques d'inférences de type) déjà cité par Dr Topos, utilisé pour le dataflow des systèmes réactifs
• Esterel également pour les systèmes réactifs (je ne connais pas trop la théorie sous-jacente... je crois que c'est un modèle concurrent synchrone )

Lustre et Esterel sont diamétralement opposés : Lustre est synchrone et est un langage fonctionnel de fux de données, et Esterel est asynchrone et est un langage impératif de contrôle de flux d'exécution.

[gorgonite]

Le programme de preuve, Coq je pense, s'est prouvé lui-même,

tiens, ça révolutionne ce que je connaissais de la logique... n'est-il pas impossible de prouver une théorie grâce à cette même théorie ?

Concernant l'ordonnancement, on utilise des techniques sur lesquelles on a des résultats garantissant lo bon ordonnancement des processus, et parfois l'optimalité de l'ordonnancement.

otes-moi un doute... la recherche de l'ordonnancement optimal n'est-il pas NP-complet ?

Lustre et Esterel sont diamétralement opposés

je n'ai pas dit le contraire... mais je relativiserais le diamétralement

Esterel est asynchrone et est un langage impératif de contrôle de flux d'exécution.

asynchrone... j'ai un gros doute car on nous enseigne l'Esterel dans des cours de "Systèmes Synchrones"

Esterel est un langage de programmation de haut niveau, synchrone et parallele, de style imperatif.

même s'il est possible de l'utiliser dans un contexte asynchrone (si j'en crois ce lien )
http://www.inria.fr/rrrt/rr-1139.html

[InOCamlWeTrust]

tiens, ça révolutionne ce que je connaissais de la logique... n'est-il pas impossible de prouver une théorie grâce à cette même théorie ?

On a commencé par écrire Coq, puis, une fois le programme écrit, on a prouvé son code source avec... Coq. Je ne vois pas ce qu'il y a d'hallucinant là-dedans.

otes-moi un doute... la recherche de l'ordonnancement optimal n'est-il pas NP-complet ?

Je ne vois pas vraiment ce à quoi tu fais référence, peut-être à autre chose... Il y a plusieurs types d'algorithmes : à priorité variable ou constante. Dans les deux cas, on sait trouver des algorithmes assez simples optimaux. Dans certains cas même, on sait établir des conditions nécessaires et suffisantes d'ordonnançabilité des processus.

Toujours ce putain de spectre du NP-complet... quand est-ce que l'on enseignera des choses utiles et non des conneries d'informaticiens théoriques ?

P = NP !!!

Je mourrai très certainement sans l'avoir démontré, mais j'en suis plus que convaincu !

asynchrone... j'ai un gros doute car on nous enseigne l'Esterel dans des cours de "Systèmes Synchrones"

Ben... t'as pas de bol ! Esterel est un langage ou l'on manipule des évènements pouvant arriver à n'importe quel moment (comme les signaux en C, qui sont asynchrones) : le langage en lui-même ne possède pas de notion d'horloge, dont chaque top détermine une "action" particulière à traiter. Ce n'est pas le cas en Lustre, langage qui est régi par la notion d'horloge : horloge courante, sous-échantillonnage et sur-échantillonnage sur des horloges différentes.

Ils sont pas un peu bizarres tes profs ?