Зиборов К.В. - Формальная семантика и верификация ПО - Семинар 9. Механизм локалей в Isabelle

Механизм локалей в Isabelle. Примеры практического применения инструмента 00:00:15 Локали. Синтаксис локалей 00:04:39 Полезные команды. Дополнение локали 00:11:30 Блоки локальных контекстов. Зависимости между локалями. Импорт локалей 00:16:20 Интерпретация локалей. Команда sublocale 00:21:43 Инерпретация локалей. Команда interpretation. Ключевое слово rewrites. Команда interpret 00:29:10 Верификация алгоритма stablecoin 00:54:56 Верификация функционального алгоритма сортировки вставками Курс: Формальная семантика и верификация программного обеспечения Ссылка на плейлист: #мгу #мехмат #миронов #формальнаясемантикапо #верификацияпо