DRAKON.SU
https://forum.drakon.su/

Формальные методы. Ликбез
https://forum.drakon.su/viewtopic.php?f=140&t=5568		 Страница 2 из 3
Автор:  ilovb [ Среда, 25 Ноябрь, 2015 10:27 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Заглянул сейчас в "Автоматное программирование". Ну он там пишет про МТ ровно то же самое, что написал я.
Автор:  Info21 [ Среда, 25 Ноябрь, 2015 22:39 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
У Шалыто не конечные автоматы.

Лучше называть это как-то вроде "фактор-автоматов", чтобы не было путаницы (там есть некая аналогия с фактор-множествами по отношениям эквивалентности).

Пример: модуль In -- похож на конечный автомат, но таковым является.
Автор:  ilovb [ Среда, 25 Ноябрь, 2015 23:34 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Цитата:
У Шалыто не конечные автоматы.


Это и сам Шалыто утверждает. Вот только это очень странное утверждение.
Понятно, что у него не конечный автомат, а конечный автомат с памятью. А конечный автомат с памятью - это МТ. А МТ можно крутить и вертеть как душе угодно. Одна лента, две... двухмерные ленты, трехмерные... да хоть переменные используй с массивами и структурами.
Это один хрен будет МТ. (т.е. конечный автомат с потенциально бесконечной памятью).

Допускаю, что я чего-то не понял. Есть пример кода чтобы вот сразу прозреть?
Автор:  albobin [ Четверг, 26 Ноябрь, 2015 08:42 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
... автомат с памятью.
вовсе не обязательно с памятью. Про конечнось/неконечность (см.мнение info21) промолчу, для осмысления надо вспомнить всё, что успешно забыто или было незнаемо :)
Автор:  ilovb [ Четверг, 26 Ноябрь, 2015 09:52 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Да это все игра с терминами.
На самом деле любой конечный автомат имеет память.
А еще любое реальное дискретное устройство - это конечный автомат (ибо деталей в устройстве конечное число).

У нас в этом плане и выбора то нет.

Единственное, что является существенным - это какой именно конечный автомат мы используем.
Так вот МТ представляет интерес с практической точки зрения. Т.к. при реализации МТ в виде реального устройства нам придется отказаться от бесконечности ленты.
А конечная лента моделируется конечным автоматом! Т.е. МТ - это два конечных автомата, соединенных вместе. Один выступает в роли процессора, а другой в роли памяти. Из этого следует, что МТ (точнее УМТ) - это модель цифрового компьютера (того самого, за которым вы сидите).
Автор:  albobin [ Четверг, 26 Ноябрь, 2015 10:15 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
А еще любое реальное дискретное устройство - это конечный автомат (ибо деталей в устройстве конечное число).
А вот такое дискретное устройство, которое преобразует входящие символы в виде материальных объектов в детали самого автомата - это конечный автомат? :)
Автор:  ilovb [ Четверг, 26 Ноябрь, 2015 10:29 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Если я правильно понял о чем речь, то да.

https://ru.wikipedia.org/wiki/Автомат_фон_Неймана
Автор:  albobin [ Четверг, 26 Ноябрь, 2015 12:09 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Пора, похоже, взять паузу и ждать продолжения непосредственно по сабжу.
Автор:  TAU [ Пятница, 27 Ноябрь, 2015 12:15 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
Цитата:
В статье есть примеры и обзорная часть, в которой имеется такая информация. Но статья, к сожалению, для специалистов.

Полистал, почитал ... А есть примеры из реальных задач? В статье уж совсем детские.
К примеру нужно поставить программистам задачу на разработку форума типа того, на котором мы тут пишем. Как это сделать по вашей методике? Как описать систему "форум" формально, понятно и достаточно полно? Тут 5-10 состояний автомата не прокатит.

Видите ли, в этом и состоит главная проблема формальных методов. Они сложны. Для реальных задач с "настоящей" размерностью .

Это обуславливает скепсис критиков формальных методов - якобы трудоемкость превосходит трудоемкость разработки самой программы.

Другое дело, что я, например - сторонник применения формальных методов, где это возможно, без огульного их отрицания по вышеприведенным причинам.
Автор:  ilovb [ Пятница, 27 Ноябрь, 2015 12:56 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Согласен. У меня колебания по тем же причинам.
Автор:  Rifat [ Пятница, 27 Ноябрь, 2015 13:43 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
К формальным методам много что относится. И многие даже применяли формальные методы сами, хотя могут об этом не догадываться :)
Например, использование EBNF при описании грамматики какого-нибудь языка (например, Оберона) - это использование формальных методов. Использование теории вероятности, при определении асимптотической сложности алгоритмов, хотя здесь многие пользуются только готовыми результатами, например, знают что сортировка Хоара в среднем сортирует за O(n*log(n)), а сортировка выбором за O(n^2).
К формальным методом относятся и следующие методы:
- использование логических предикатов при верификации методом Хоара;
- использование алгебраических спецификаций для описания абстрактных типов данных;
- различные конечные автоматы
и многие другие методы.
Формальные методы широко используются в узких кругах :)
Недавно читал про фирму Amazon, которая использует язык TLA+, для описания распреденных параллельных систем, затем проверяет созданную модель с помощью специальной программы проверки моделей (TLC model checker), и иногда находят очень трудно уловимые ошибки, которые человек наврятли бы нашел.
http://glat.info/pdf/formal-methods-amazon-2014-11.pdf
Автор:  Владимир Шелехов [ Пятница, 27 Ноябрь, 2015 21:35 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
Цитата:
В статье есть примеры и обзорная часть ...
Полистал, почитал ... А есть примеры из реальных задач? В статье уж совсем детские.
И Вы уверены что запросто смогли бы решить самую простую из этих детских задач?
Цитата:
К примеру нужно поставить программистам задачу на разработку форума типа того, на котором мы тут пишем. Как это сделать по вашей методике? Как описать систему "форум" формально, понятно и достаточно полно?

Давайте не будем замахиваться на полную функциональность системы "Форум". Рассмотрим задачу попроще. Допустим, требуется перенести все сообщения данной темы после 20 ноября по 26 ноября в другую тему "Дискуссия по формальным методам и инженерии требований". Понятно, что это частный случай более общей задачи, которую для начала я предлагаю Вам сформулировать в виде содержательного описания требований. Возможно, к этому процессу захотят присоединиться другие. Дерзайте!!! Посмотрим, что получится, сколько подводных камней встретится на нашем пути. Думаю, в конце появится Администратор, знающий систему изнутри, и скажет, что все мы ничего не понимаем в этой жизни.

Дальнейшую дискуссию предлагаю продолжить в другой теме.
Автор:  albobin [ Пятница, 27 Ноябрь, 2015 22:25 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Если Ilov или кто еще напишет здесь содержательные требования Вам придётся идти в соавторы, иначе хозяева форума могут проигнорировать исходящее не от автора темы :)
Автор:  ilovb [ Пятница, 27 Ноябрь, 2015 23:21 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Владимир Шелехов писал(а):
И Вы уверены что запросто смогли бы решить самую простую из этих детских задач?

Я на хлеб зарабатываю ежедневным решением задач. Занимаюсь этим давно и успешно.
Будильник, лифт и банкомат... Если это сложные задачи, то вы видимо просто не сталкивались со сложными задачами.
Автор:  albobin [ Пятница, 27 Ноябрь, 2015 23:43 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Уважаемые администраторы, ради продолжения дискуссии, пожалуйста,
update там_где_надо
set тема=5581
where форум=140 and тема=5568 and сообщение>=93926 and сообщение<=94062
:)
Автор:  ilovb [ Пятница, 27 Ноябрь, 2015 23:50 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Не пугайте Владимира сложным кодом :D
Автор:  Info21 [ Воскресенье, 29 Ноябрь, 2015 15:40 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
TAU писал(а):
Видите ли, в этом и состоит главная проблема формальных методов. Они сложны. Для реальных задач с "настоящей" размерностью .

Это обуславливает скепсис критиков формальных методов - якобы трудоемкость превосходит трудоемкость разработки самой программы.

Штука ещё в том, что чем сложнее задача, тем она хуже понята и поставлена.
Сам процесс решения есть процесс прояснения её постановки, в том числе формальных требований.

Другими словами, формальные методы нельзя отделить от неформальных и им противопоставить.
Автор:  TAU [ Понедельник, 30 Ноябрь, 2015 02:30 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
Цитата:
У Шалыто не конечные автоматы.

Это и сам Шалыто утверждает. Вот только это очень странное утверждение...
Допускаю, что я чего-то не понял

Мне у него спросить? :wink:
Автор:  ilovb [ Понедельник, 30 Ноябрь, 2015 09:43 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
Спросите. Ликбез же :)
Автор:  TAU [ Пятница, 11 Декабрь, 2015 10:29 ]
Заголовок сообщения:  Re: Формальные методы. Ликбез
ilovb писал(а):
Цитата:
У Шалыто не конечные автоматы.


Это и сам Шалыто утверждает. Вот только это очень странное утверждение.
Понятно, что у него не конечный автомат, а конечный автомат с памятью. А конечный автомат с памятью - это МТ. А МТ можно крутить и вертеть как душе угодно. Одна лента, две... двухмерные ленты, трехмерные... да хоть переменные используй с массивами и структурами.
Это один хрен будет МТ. (т.е. конечный автомат с потенциально бесконечной памятью).

Допускаю, что я чего-то не понял. Есть пример кода чтобы вот сразу прозреть?

Я поговорил с Анатолием Абрамовичем. По его личному категоричному заявлению, "самые что ни на есть конечные автоматы, детерминированные, без памяти в смысле доп.лент, не машина Тьюринга". Время тоже вынесено "наружу". Истечение временного интервала - событие.
Страница 2 из 3 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/