Вот какие предложения возникают (с позиции предметника, не теоретика программирования).
А) Добавил бы в дополнительные источники работу Агафонова (описана в прилагаемой понятийной карточке) - как подводку к языковому базису ФМПИ. Ну и монографию (и/или пособия)
Зверева - для сведения о подходе к формальным методам (попытался пояснить своё понимание в аннотации на Пойа, так что прилагаю тоже). Вероятно, как классическое неформальное введение можно и Пойа - но на него, возможно, и так обращается внимание в других
курсах по специальности.
Б) Наверное, неплохо было бы (скорее всего, где-то в Разделе 4) обратить внимание на наглядные представления спецификаций и дать соответствующие источники. Аргументацию за
подобное можно, ессно, найти на этом же сайте - прежде всего для алгоритмических структур управления. К этому для полноты добавляется для структур данных и исполнителей. Некий
вариант связки - как описано у
Фути и Судзуки: (структурно-временные диаграммы задействования трактов Катана-
исполнителя при прохождении данных по алгоритмам команд) - но удобно и по отдельности.
Свежий пример потребности - авария на Восточном. Одна из версий - контроллер разгонного блока изначально был загружен данными о Байконуре как точке старта, а в связи с переназначением блока для применения с Восточного эти данные так и не поменяли.
Возможно, проверка данных была ненаглядной - допустим, выводят для персонала (стартового в том числе) как сводки символьно. Если бы те же значения визуализировались (адекватно
их смыслам; понятно, что на внешнем технологическом АРМ, а не скромными ресурсами бортовых), то что-то было бы проще "отловить". Конкретно эти данные - наложить на карту как
точку - трудно предположить, что у стартовика, готовящего блок для запуска с Восточного, не вызвало бы вопросов положение исходной точки на Байконуре.
Кое-что есть в верификаторах - Spin, допустим, визуализирует модель (найденный контрпример). Кстати, обзор графических средств описания деятельности для программирования есть
в монографии Тюгашева (представлена в карточках Ист с Тюгашевым*) - может, достаточно на неё и сослаться.
В) Ну и основные результаты школы, к которой принадлежит Тюгашев, можно упомянуть в списке. Имеется в виду исчисление УА РВ. Как по-своему вводящее формальные методы в
программную инженерию. Есть монография (там же как /23/). Кстати, один из результатов - логико-временные модели - имеет формальное графическое представление, реализованное в
среде ГРАФКОНТ-ГЕОЗ. Но уж тут специалистам разбираться, какой где уровень формальности методов.
Вход
FAQ
Поиск
