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