ЭБ Коллекция: кафедра ТП, 6 семестркафедра ТП, 6 семестрhttps://elib.bsu.by:443/handle/123456789/3357492026-04-21T05:34:38Z2026-04-21T05:34:38ZФормальная семантика и верификация программ: учебная программа учреждения образования по учебной дисциплине для специальности: 6-05-0533-10 Информатика Профилизация: Технологии разработки сложных информационных систем. Регистрационный № 4428/б.Курбацкий, А. Н.Винник, В. Ю.https://elib.bsu.by:443/handle/123456789/3435492026-03-14T03:56:31Z2025-09-29T00:00:00ZЗаглавие документа: Формальная семантика и верификация программ: учебная программа учреждения образования по учебной дисциплине для специальности: 6-05-0533-10 Информатика Профилизация: Технологии разработки сложных информационных систем. Регистрационный № 4428/б.
Авторы: Курбацкий, А. Н.; Винник, В. Ю.
Аннотация: ПОЯСНИТЕЛЬНАЯ ЗАПИСКА
Цели и задачи учебной дисциплины
Цель учебной дисциплины – формирование у студентов систематических
знаний в области формальных методов спецификации, семантики и верификации
программ, а также практических навыков применения этих методов для
доказательства корректности алгоритмов. необходимых им в дальнейшем для
успешной профессиональной деятельности в области промышленной
разработки.
Задачи учебной дисциплины:
1. Изучить основные формальные модели семантики программ
(операциональную, денотационную, аксиоматическую).
2. Освоить базовые методы верификации программ: метод Хоара и метод
слабейших предусловий Дейкстры.
3. Познакомиться с объединяющей теорией программирования Хоара
(Unifying Theories of Programming).
4. Получить базовые представления о теории категорий как об
универсальном языке для формализации семантики;
5. Сформировать умение строить формальные спецификации программ и
доказывать их свойства.
Место учебной дисциплины в системе подготовки специалиста с высшим
образованием.
Учебная дисциплина относится к дисциплинам профилизации компонента
учреждения образования модуля «Технологии разработки сложных
информационных систем».
Учебная программа по дисциплине профилизации «Формальная семантика
и верификация программ» разработана в соответствии с учебным планом и
образовательным стандартом общего высшего образования по специальности 6-
05-0533-10 Информатика.
Современная разработка критически важного и высоконадёжного
программного обеспечения требует применения строгих математических
методов для спецификации и проверки корректности программ. Без
теоретических знаний и практических навыков в области формальной семантики
и верификации специалисту по разработке программного обеспечения
невозможно эффективно решать профессиональные задачи в таких областях, как
авионика, космонавтика, медицина, атомная энергетика и финансы. Наиболее
востребованными навыками являются формальная спецификация требований,
доказательство корректности алгоритмов, анализ программ на соответствие
заданным свойствам.
Основой для изучения методологий, технологий программирования
являются следующие дисциплины: «Промышленное программирование»,
«Дискретная математика и математическая логика», «Операционные системы».
Учебная дисциплина «Формальная семантика и верификация программ»
непосредственно связана с параллельно изучаемыми учебными дисциплинами:
«Методы оптимизации» модуля «Математические модули принятия решений»
компонента учреждения высшего образования, «Технологии
программирования» модуля «Программирование» государственного
компонента.2025-09-29T00:00:00Z