Верификация программ методом инвариантов

Излагается метод инвариантов для доказательства правильности компьютерных программ. Основные концепции, связанные с этим методом, иллюстрированы примерами верификации последовательных и параллельных программ.