DRAKON.SU https://forum.drakon.su/ |
|
Вопросы по курсу "Формальные методы в программной инженерии" https://forum.drakon.su/viewtopic.php?f=140&t=5915 |
Страница 1 из 1 |
Автор: | Владимир Шелехов [ Среда, 12 Октябрь, 2016 07:36 ] |
Заголовок сообщения: | Вопросы по курсу "Формальные методы в программной инженерии" |
Данная рубрика предназначена для вопросов, замечаний и предложений по магистерскому курсу Видеолекции курса находятся на сайте: В настоящий момент в Новосибирском Государственном Университете прочитаны две лекции по второму разделу курса "Спецификация и верификация программ в предикатном и автоматном программировании". В ближайшее время они будут выложены на сайт. Лекции первого раздела по SMT-решателям, а также вводные лекции по курсу доступны на сайте. |
Автор: | Владислав Жаринов [ Вторник, 09 Январь, 2018 14:51 ] | ||||
Заголовок сообщения: | Возможности дополнения корпуса источников | ||||
Вот какие предложения возникают (с позиции предметника, не теоретика программирования). А) Добавил бы в дополнительные источники работу Агафонова (описана в прилагаемой понятийной карточке) - как подводку к языковому базису ФМПИ. Ну и монографию (и/или пособия) Зверева - для сведения о подходе к формальным методам (попытался пояснить своё понимание в аннотации на Пойа, так что прилагаю тоже). Вероятно, как классическое неформальное введение можно и Пойа - но на него, возможно, и так обращается внимание в других курсах по специальности. Б) Наверное, неплохо было бы (скорее всего, где-то в Разделе 4) обратить внимание на наглядные представления спецификаций и дать соответствующие источники. Аргументацию за подобное можно, ессно, найти на этом же сайте - прежде всего для алгоритмических структур управления. К этому для полноты добавляется для структур данных и исполнителей. Некий вариант связки - как описано у Фути и Судзуки: (структурно-временные диаграммы задействования трактов Катана- исполнителя при прохождении данных по алгоритмам команд) - но удобно и по отдельности.
Возможно, проверка данных была ненаглядной - допустим, выводят для персонала (стартового в том числе) как сводки символьно. Если бы те же значения визуализировались (адекватно их смыслам; понятно, что на внешнем технологическом АРМ, а не скромными ресурсами бортовых), то что-то было бы проще "отловить". Конкретно эти данные - наложить на карту как точку - трудно предположить, что у стартовика, готовящего блок для запуска с Восточного, не вызвало бы вопросов положение исходной точки на Байконуре. Кое-что есть в верификаторах - Spin, допустим, визуализирует модель (найденный контрпример). Кстати, обзор графических средств описания деятельности для программирования есть в монографии Тюгашева (представлена в карточках Ист с Тюгашевым*) - может, достаточно на неё и сослаться. В) Ну и основные результаты школы, к которой принадлежит Тюгашев, можно упомянуть в списке. Имеется в виду исчисление УА РВ. Как по-своему вводящее формальные методы в программную инженерию. Есть монография (там же как /23/). Кстати, один из результатов - логико-временные модели - имеет формальное графическое представление, реализованное в среде ГРАФКОНТ-ГЕОЗ. Но уж тут специалистам разбираться, какой где уровень формальности методов.
|
Автор: | Владимир Шелехов [ Суббота, 05 Сентябрь, 2020 13:46 ] |
Заголовок сообщения: | Видеокурс по системе автоматического доказательства Why3 |
Многие хотели бы начать работать на какой-нибудь системе автоматического доказательства. Но непонятно, какую выбрать. Их много. И все они такие сложные. Рекомендую систему Why3. Ее проще освоить по сравнению с другими, такими как PVS и Coq. Язык функционального программирования WhyML, используемый для спецификаций и программирования, обладает высокой выразительностью. Имеется больший набор (~20) разнообразных автоматических мощных решателей. Последняя версия Why3 оснащена универсальной и простой системой интерактивного доказательства, позволяющая "руками" провести любое доказательство. На системе Why3 выполнены десятки серьезных производственных проектов. В прошлом году я верифицировал на Why3 семь нетривиальных программ из библиотеки ядра ОС Linux. В этом году появился курс в Новосибирском Государственном университете:
Видеолекции доступны на сайте: Формальные методы в программной инженерии, Раздел 4. Имеется также дистрибутив Why3 с набором инструментов доказательства: alt-ergo 2.3.0, cvc3 2.4.1, cvc4 1.7, z3 4.8.6, coq 8.9.0. http://wasp.iis.nsk.su/pres/why3-1.3.1-deb.zip В системе Windows ставится на версии VirtualBox, не ниже 6.1.6. Пользователь user, пароль: 123. Нужно будет настроить связь через Windows-директорию (с общим доступом) вашего компьютера. Запуск Why3 реализуется нажатием на файл с расширением mlw |
Автор: | Владимир Паронджанов [ Суббота, 05 Сентябрь, 2020 19:42 ] |
Заголовок сообщения: | Re: Вопросы по курсу "Формальные методы в программной инжене |
Владимир Иванович, спасибо. https://forum.oberoncore.ru/viewtopic.p ... 71#p112471 |
Страница 1 из 1 | Часовой пояс: UTC + 3 часа |
Powered by phpBB® Forum Software © phpBB Group https://www.phpbb.com/ |