Аннотация: Доказательство корректности программ

Данная книга учит формально рассуждать о компьютерных программах, используя последовательный подход и язык программирования Dafny, поддерживающий верификацию. Показано, как писать спецификации для программ, как удовлетворить требования этих спецификаций и как писать доказательства корректности программ относительно спецификаций. Автор сначала представляет теоретические предпосылки, лежащие в основе рассуждений о программном коде, а затем постепенно переходит к реальным примерам, использующих объекты, структуры данных и нетривиальную рекурсию. Книга написана простым и понятным языком, содержит множество забавных иллюстраций и практических упражнении. Издание будет полезно студентам вузов, преподавателям, исследователям в области формальной верификации, а также сотрудникам компаний, применяющих дедуктивную верификацию на практике.

Издательство	ДМК
Автор/составитель	Лейно К. Рустан. М.
Год выпуска	2024
Кол-во страниц	530
ISBN	978-5-93700-199-3
Обложка	Пер
Вес	951г
Формат	17 x 25 cm
Тираж	100
Возрастная категория	16+