[ДМК] Доказательство корректности программ [К. Рустан М. Лейно]

[Kevin]

[ДМК] **Доказательство корректности программ** *Автор: К. Рустан М. Лейно*

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

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

**Особенности книги:**
- Написана простым и понятным языком;
- Постепенно вводит все более сложные понятия;
- Наглядно демонстрирует, как писать доказательства и верифицировать функциональные и императивные программы;
- Приводит примеры программного кода на реальном языке программирования, а не псевдокоде;
- Содержит забавные иллюстрации и обучающие упражнения.

Издание будет полезно студентам вузов, преподавателям, исследователям в области формальной верификации, а также сотрудникам компаний, применяющих дедуктивную верификацию на практике.

**Информация об издании:**
- **Издание:** Черно-белое
- **Оригинальное название:** Program Proofs
- **Оригинальный правообладатель:** MIT Press
- **Научный редактор:** Кондратьев Д.
- **Объем, стр:** 522
- **ISBN:** 978-5-97060-199-3
- **Формат:** PDF
- **Стоимость:** 1600

Для просмотра скрытого содержимого вы должны зарегистрироваться