Формальная семантика и верификация программ: учебная программа учреждения образования по учебной дисциплине для специальности: 6-05-0533-10 Информатика Профилизация: Технологии разработки сложных информационных систем. Регистрационный № 4428/б.

Abstract

ПОЯСНИТЕЛЬНАЯ ЗАПИСКА Цели и задачи учебной дисциплины Цель учебной дисциплины – формирование у студентов систематических знаний в области формальных методов спецификации, семантики и верификации программ, а также практических навыков применения этих методов для доказательства корректности алгоритмов. необходимых им в дальнейшем для успешной профессиональной деятельности в области промышленной разработки. Задачи учебной дисциплины: 1. Изучить основные формальные модели семантики программ (операциональную, денотационную, аксиоматическую). 2. Освоить базовые методы верификации программ: метод Хоара и метод слабейших предусловий Дейкстры. 3. Познакомиться с объединяющей теорией программирования Хоара (Unifying Theories of Programming). 4. Получить базовые представления о теории категорий как об универсальном языке для формализации семантики; 5. Сформировать умение строить формальные спецификации программ и доказывать их свойства. Место учебной дисциплины в системе подготовки специалиста с высшим образованием. Учебная дисциплина относится к дисциплинам профилизации компонента учреждения образования модуля «Технологии разработки сложных информационных систем». Учебная программа по дисциплине профилизации «Формальная семантика и верификация программ» разработана в соответствии с учебным планом и образовательным стандартом общего высшего образования по специальности 6- 05-0533-10 Информатика. Современная разработка критически важного и высоконадёжного программного обеспечения требует применения строгих математических методов для спецификации и проверки корректности программ. Без теоретических знаний и практических навыков в области формальной семантики и верификации специалисту по разработке программного обеспечения невозможно эффективно решать профессиональные задачи в таких областях, как авионика, космонавтика, медицина, атомная энергетика и финансы. Наиболее востребованными навыками являются формальная спецификация требований, доказательство корректности алгоритмов, анализ программ на соответствие заданным свойствам. Основой для изучения методологий, технологий программирования являются следующие дисциплины: «Промышленное программирование», «Дискретная математика и математическая логика», «Операционные системы». Учебная дисциплина «Формальная семантика и верификация программ» непосредственно связана с параллельно изучаемыми учебными дисциплинами: «Методы оптимизации» модуля «Математические модули принятия решений» компонента учреждения высшего образования, «Технологии программирования» модуля «Программирование» государственного компонента.