DRAKON.SU

Текущее время: Воскресенье, 01 Август, 2021 07:00

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 50 ]  На страницу Пред.  1, 2, 3  След.
Автор Сообщение
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 10:27 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Заглянул сейчас в "Автоматное программирование". Ну он там пишет про МТ ровно то же самое, что написал я.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 22:39 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 140
Откуда: Троицк, Москва
У Шалыто не конечные автоматы.

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

Пример: модуль In -- похож на конечный автомат, но таковым является.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Среда, 25 Ноябрь, 2015 23:34 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Цитата:
У Шалыто не конечные автоматы.


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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 26 Ноябрь, 2015 08:42 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
... автомат с памятью.
вовсе не обязательно с памятью. Про конечнось/неконечность (см.мнение info21) промолчу, для осмысления надо вспомнить всё, что успешно забыто или было незнаемо :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 26 Ноябрь, 2015 09:52 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Да это все игра с терминами.
На самом деле любой конечный автомат имеет память.
А еще любое реальное дискретное устройство - это конечный автомат (ибо деталей в устройстве конечное число).

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

Единственное, что является существенным - это какой именно конечный автомат мы используем.
Так вот МТ представляет интерес с практической точки зрения. Т.к. при реализации МТ в виде реального устройства нам придется отказаться от бесконечности ленты.
А конечная лента моделируется конечным автоматом! Т.е. МТ - это два конечных автомата, соединенных вместе. Один выступает в роли процессора, а другой в роли памяти. Из этого следует, что МТ (точнее УМТ) - это модель цифрового компьютера (того самого, за которым вы сидите).


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 26 Ноябрь, 2015 10:15 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
ilovb писал(а):
А еще любое реальное дискретное устройство - это конечный автомат (ибо деталей в устройстве конечное число).
А вот такое дискретное устройство, которое преобразует входящие символы в виде материальных объектов в детали самого автомата - это конечный автомат? :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 26 Ноябрь, 2015 10:29 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Если я правильно понял о чем речь, то да.

https://ru.wikipedia.org/wiki/Автомат_фон_Неймана


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Четверг, 26 Ноябрь, 2015 12:09 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
Пора, похоже, взять паузу и ждать продолжения непосредственно по сабжу.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 12:15 

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 341
ilovb писал(а):
Цитата:
В статье есть примеры и обзорная часть, в которой имеется такая информация. Но статья, к сожалению, для специалистов.

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 12:56 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Согласен. У меня колебания по тем же причинам.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 13:43 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 219
Откуда: Казань
К формальным методам много что относится. И многие даже применяли формальные методы сами, хотя могут об этом не догадываться :)
Например, использование EBNF при описании грамматики какого-нибудь языка (например, Оберона) - это использование формальных методов. Использование теории вероятности, при определении асимптотической сложности алгоритмов, хотя здесь многие пользуются только готовыми результатами, например, знают что сортировка Хоара в среднем сортирует за O(n*log(n)), а сортировка выбором за O(n^2).
К формальным методом относятся и следующие методы:
- использование логических предикатов при верификации методом Хоара;
- использование алгебраических спецификаций для описания абстрактных типов данных;
- различные конечные автоматы
и многие другие методы.
Формальные методы широко используются в узких кругах :)
Недавно читал про фирму Amazon, которая использует язык TLA+, для описания распреденных параллельных систем, затем проверяет созданную модель с помощью специальной программы проверки моделей (TLC model checker), и иногда находят очень трудно уловимые ошибки, которые человек наврятли бы нашел.
http://glat.info/pdf/formal-methods-amazon-2014-11.pdf


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 21:35 

Зарегистрирован: Вторник, 22 Сентябрь, 2015 20:43
Сообщения: 76
ilovb писал(а):
Цитата:
В статье есть примеры и обзорная часть ...
Полистал, почитал ... А есть примеры из реальных задач? В статье уж совсем детские.
И Вы уверены что запросто смогли бы решить самую простую из этих детских задач?
Цитата:
К примеру нужно поставить программистам задачу на разработку форума типа того, на котором мы тут пишем. Как это сделать по вашей методике? Как описать систему "форум" формально, понятно и достаточно полно?

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

Дальнейшую дискуссию предлагаю продолжить в другой теме.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 22:25 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
Если Ilov или кто еще напишет здесь содержательные требования Вам придётся идти в соавторы, иначе хозяева форума могут проигнорировать исходящее не от автора темы :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 23:21 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Владимир Шелехов писал(а):
И Вы уверены что запросто смогли бы решить самую простую из этих детских задач?

Я на хлеб зарабатываю ежедневным решением задач. Занимаюсь этим давно и успешно.
Будильник, лифт и банкомат... Если это сложные задачи, то вы видимо просто не сталкивались со сложными задачами.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 23:43 

Зарегистрирован: Пятница, 20 Июль, 2007 17:26
Сообщения: 105
Откуда: Псков
Уважаемые администраторы, ради продолжения дискуссии, пожалуйста,
update там_где_надо
set тема=5581
where форум=140 and тема=5568 and сообщение>=93926 and сообщение<=94062
:)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 27 Ноябрь, 2015 23:50 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Не пугайте Владимира сложным кодом :D


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Воскресенье, 29 Ноябрь, 2015 15:40 

Зарегистрирован: Пятница, 25 Ноябрь, 2005 12:02
Сообщения: 140
Откуда: Троицк, Москва
TAU писал(а):
Видите ли, в этом и состоит главная проблема формальных методов. Они сложны. Для реальных задач с "настоящей" размерностью .

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

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

Другими словами, формальные методы нельзя отделить от неформальных и им противопоставить.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Понедельник, 30 Ноябрь, 2015 02:30 

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 341
ilovb писал(а):
Цитата:
У Шалыто не конечные автоматы.

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

Мне у него спросить? :wink:


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Понедельник, 30 Ноябрь, 2015 09:43 

Зарегистрирован: Вторник, 30 Июнь, 2009 14:58
Сообщения: 101
Спросите. Ликбез же :)


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Формальные методы. Ликбез
СообщениеДобавлено: Пятница, 11 Декабрь, 2015 10:29 

Зарегистрирован: Воскресенье, 09 Март, 2008 22:38
Сообщения: 341
ilovb писал(а):
Цитата:
У Шалыто не конечные автоматы.


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

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

Я поговорил с Анатолием Абрамовичем. По его личному категоричному заявлению, "самые что ни на есть конечные автоматы, детерминированные, без памяти в смысле доп.лент, не машина Тьюринга". Время тоже вынесено "наружу". Истечение временного интервала - событие.


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 50 ]  На страницу Пред.  1, 2, 3  След.

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 2


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
cron
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2008-2021, участники конференции «DRAKON.SU», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB