La sémantique relationnelle des boucles

Cette séance de cours couvre la sémantique relationnelle des boucles, y compris la traduction des opérations de ravage, lécriture de spécifications en utilisant des ravages et assumer, le raffinement et léquivalence des programmes, la méthodologie de raffinement par étapes, la monotonie par rapport au raffinement, lélimination heuristique des quantificateurs de formules, la signification des boucles dans les programmes, et la sémantique mathématique des boucles.