span.fullpost {display:none;} span.fullpost {display:inline;}

среда, 18 января 2012 г.

Список тем лекций

Советую, как минимум, иметь представление по каждому из вопросов из следующего списка (это краткий план материала лекций этого года), а лучше и знать формулировки и определения по каждому из вопросов. Фактически этот список можно воспринимать как список тем для теоретических вопросов на экзамене.




  1. Что такое формальные спецификации. Абстракция, строгость (rigour), систематичность. Верификация и валидация программ и требований.
  2. Формальные методы разработки программ. Уточнение программ. Принцип подстановки Лисков. Функция абстракции. Диаграмма коммутативности. Design by Contract.
  3. Полнота спецификаций. Непротиворечивость спецификаций.
  4. Методы VDM и RAISE.
  5. Алгебраические спецификации.
  6. Моделеориентированные спецификации: явные и неявные.
  7. Исполнимые формальные спецификации: конечные автоматы, системы переходов.
  8. Языки спецификации, спецификационные расширения языков программирования (в том числе аннотации), библиотеки функций для описания свойств данных и операций в программе без расширения языка программирования. Примеры. Сравнение.
  9. Язык RSL.
  10. Использование формальных спецификаций в строгих (rigour) подходах к поиску ошибок в программах.
  11. Инструменты Spec# и Dafny. Проблема верификации программ, оперирующих с динамической памятью.
  12. Formal testing. Model-based testing.
  13. Аналитическая верификация. Понятия частичной и полной корректности.
  14. Основные понятия методов Флойда. Точки сечения, индуктивные утверждения, оценочные функции, фундированные множества.
  15. Метод индуктивных утверждений Флойда. Условия верификации и условия корректности.
  16. Метод оценочных функций Флойда. Условия корректности и завершимости.
  17. Методы Флойда для рекурсивных программ.
  18. Методы Флойда для программ с частичными функциями (в частности, с операциями обращения к элементам массива).
  19. Инструмент PVS: общая характеристика. Теоремы, вид представления доказательств, интерактивность.
  20. Язык спецификации инструмента PVS.
  21. Основные команды инструмента PVS : skolem!, flatten, split, case, induct, inst, expand, replace, lemma, assert, grind.
  22. ACSL – язык аннотаций для программ на языке Си. Инструмент Frama-C.

2 комментария:

  1. Анонимный18 января 2012 г. в 22:24

    Я правильно понимаю, что, кроме как для вопросов 9, 13-16, не существует официальных материалов?
    Ну еще частично про 1-8 написано в rslbook и методичке о RSL, про инструмены Dafny и RSL - на соответствующих сайтах. Где искать "официальный" материал, касающийся вопросов 10-12, 17-18, 22

    Конечно же, ищется материал *в дополнение к конспектам лекций*, для более полного проникновения в предмет... =)

    ОтветитьУдалить
    Ответы
    1. Eugene Kornykhin18 января 2012 г. в 22:41

      во-первых, конечно, у каждого нормального студента должны быть конспекты :) во-вторых, можно посмотреть статьи, ссылки на которые даны на http://sp.cmc.msu.ru/courses/fmsp . Ну и, в-третьих, можете попробовать посмотреть мои попытки видеозаписи лекций (http://www.youtube.com/playlist?list=PL85900B3D8F94417B), но поскольку это лишь были попытки, то и качество там неважнецкое :)

      Удалить

Подписаться на: Комментарии к сообщению (Atom)