Equivalence entre la sémantique dénotationelle et la sémantique opérationnelle

On prouve ici l'équivalence entre la sémantique opérationnelle et la sémantique dénotationnelle. On ne s'attardera que sur les cas les plus intéressants, typiquement la boucle while.