Доказ коректності програм. К. Рустан М. Лейно

Ця книжка вчить формально міркувати про комп'ютерні програми, використовуючи послідовний підхід і мову програмування Dafny, що підтримує верифікацію. Показано, як писати специфікації для програм, як задовольнити вимоги цих специфікацій і як писати докази коректності програм щодо специфікацій. Автор спочатку представляє теоретичні передумови, що лежать в основі міркувань про програмний код, а потім поступово переходить до реальних прикладів, що використовують об'єкти, структури даних і нетривіальну рекурсію.

Особливості книги:

• написана простою і зрозумілою мовою;
• поступово вводить дедалі складніші поняття;
• наочно демонструє, як писати докази, а також як визначати та верифікувати функціональні та імперативні програми;
• наводить приклади програмного коду реальною мовою програмування, а не псевдокодом;
• містить кумедні ілюстрації та навчальні вправи.

Видання буде корисним студентам вишів, викладачам, дослідникам у сфері формальної верифікації, а також співробітникам компаній, які застосовують дедуктивну верифікацію на практиці.