Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
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 …