Зиборов К.В. - Формальная семантика и верификация ПО - Семинар 6. Объявление типов в Isabelle/HOL

Объявление типов в Isabelle/HOL. Рекурсивные функции. Индукция. 00:15 Задание типов в Isabelle. Структурная индукция (повторение) 13:37 Функция, которая переворачивает список (доказательство свойств) 31:55 Ограничения на структурную индукцию 34:31 Задание рекурсивных типов (дерево) 38:21 Функция, которая переворачивает первый список и объединяет его со вторым списком (доказательство свойств) 43:36 Функция, которая подсчитывает сумму элементов списка из натуральных чисел (доказательство свойств) 01:03:28 Доказательство утверждений с заданными типами и функциями с помощью индукции (подведение итогов лекции) Курс: Формальная семантика и верификация программного обеспечения Ссылка на плейлист: #мгу #мехмат #миронов #формальнаясемантикапо #верификацияпо