Spécificationvérification, optimisation
Previous: Formalisation de l'implantation
La distribution et l'ajout des opérations de communication 
ne
modifient pas l'ordre partiel D du graphe algorithme.
Sur chaque processeur, un ordonnancement des opérations de calculs est un ordre
total 
qui inclut l'ordre partiel restreint à 
c'est-à-dire
.
De même sur chaque liaison de communication, un ordonnancement des opérations
de communication est un ordre total 
qui inclut l'ordre
partiel restreint à 
.
La transformation globale 
est la composition des quatre
transformations :
