Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
Colloque
Dans un formalisme relationnel, un programme peut être représenté par un quintuplet P = (G, S, β, ε, α) où G est le graphe de contrôle, S est le graphe sur l'ensemble des situations (une situation est une paire (s, p) où s est un état du programme et p un point de commande dans le graphe de contrôle), β est un homomorphisme surjectif de S vers G, et ε est respectivement les relations d'entrée et de sortie. Nous définissons la sémantique d'un programme P comme étant la relation entre les points d'entrée et de sortie (déterminés par ε et …
Colloque
Dans un formalisme relationnel, un programme peut être représenté par un quintuplet P = (G, S, β, ε, α) où G est le graphe de contrôle, S est le graphe sur l'ensemble des situations (une situation est une paire (s, p) où s est un état du programme et p un point de commande dans le graphe de contrôle), β est un homomorphisme surjectif de S vers G, et ε est respectivement les relations d'entrée et de sortie. Nous définissons la sémantique d'un programme P comme étant la relation entre les points d'entrée et de sortie (déterminés par ε et …
Colloque
Nous adoptons un point de vue sémantique et nous considérons les programmes et les spécifications comme des relations. Nous définissons un ordre partiel de raffinement entre les relations, qui mène à la construction de programmes totalement corrects par rapport à leur spécification. Cet ordre partiel est un demi-treillis supérieur complet, pour lequel l’opération de suprémum est déjà connue sous le nom de “suprem démoniaque”. Il existe aussi une opération de composition, connue sous le nom de “composition démoniaque”. Bien que ces opérations possèdent des propriétés intéressantes (comme l’associativité et la distributivité), la preuve directe de ces propriétés est fastidieuse. Nous …
Colloque
Nous adoptons un point de vue sémantique et nous considérons les programmes et les spécifications comme des relations. Nous définissons un ordre partiel de raffinement entre les relations, qui mène à la construction de programmes totalement corrects par rapport à leur spécification. Cet ordre partiel est un demi-treillis supérieur complet, pour lequel l’opération de suprémum est déjà connue sous le nom de “suprem démoniaque”. Il existe aussi une opération de composition, connue sous le nom de “composition démoniaque”. Bien que ces opérations possèdent des propriétés intéressantes (comme l’associativité et la distributivité), la preuve directe de ces propriétés est fastidieuse. Nous …
Colloque
La vérification d'une conjecture portant sur les graphes ou les relations se fait souvent au moyen de petits exemples traités manuellement. Le système RELVIEW, développé à l'Université des forces armées de Munich, a été conçu pour le traitement interactif d'exemples de plus grande taille. Il permet de construire les relations (sous forme de matrices booléennes) au moyen de la souris, puis de leur appliquer divers opérateurs relationnels. Nous montrons comment utiliser RELVIEW pour visualiser sous forme de matrice booléenne le treillis de Galois d'une relation binaire (treillis des rectangles maximaux); c'est une tâche manuelle complexe, même pour de petits exemples. …
