The chronicler of 452 - noorderlicht.

Aug. 15th, 2010

08:29 pm - noorderlicht.

Previous Entry Share Next Entry

Задача:

(Полноразмерное изображение. В виде картинки из-за знаменитого почерка.)


Моё понимание computing [sic] science и программирования делится на периоды до и после моего знакомства с EWD1162, откуда я узнал, что программы и алгоритмы можно вычислять, как вычисляют неопределённые интегралы

(14 comments | Leave a comment)

Comments:

[User Picture]
From:jedal
Date:August 16th, 2010 07:46 am (UTC)

Интересно,

(Link)
а Dijkstra — автор этой задачи?

(Любопытно потому, что следующую задачу нередко дают на кружках 6-7 классу:

Инженер, работающий за городом, ежедневно приезжает поездом на одну станцию в одно и то же время. В это же время за ним приезжает машина, и он попадает на завод вовремя. Однажды инженер приехал на станцию на 35 минут раньше, и не дожидаясь машины, пошел пешком на завод. Встретив машину, он сел в нее и приехал на завод на 10 минут раньше обычного. Во сколько раз скорость инженера меньше скорости машины? (Скорости машины и инженера всегда постоянны.))
(Reply) (Thread)
[User Picture]
From:furia_krucha
Date:August 16th, 2010 08:12 am (UTC)

Re: Интересно,

(Link)
Он, по-крайней мере, один из авторов экономного способа изложения решения (см. ниже). Задача сама (в разных вариантах), конечно, достаточно известная и, скорее всего, старая.
(Reply) (Parent) (Thread)
[User Picture]
From:kamchatnov
Date:August 16th, 2010 07:49 am (UTC)
(Link)
50 минут.
(Надеюсь, что будет приведено решение, написанное тем же знаменитым почерком.)
(Reply) (Thread)
[User Picture]
From:furia_krucha
Date:August 16th, 2010 08:10 am (UTC)
(Link)
А как же.

(Reply) (Parent) (Thread)
[User Picture]
From:kamchatnov
Date:August 16th, 2010 09:16 am (UTC)
(Link)
Спасибо! Красивое рассуждение!
(Reply) (Parent) (Thread)
[User Picture]
From:jedal
Date:November 17th, 2011 08:55 am (UTC)

Видимо,

(Link)
это часть какого-то большего текста? А какого?
(Reply) (Parent) (Thread)
[User Picture]
From:furia_krucha
Date:November 17th, 2011 02:10 pm (UTC)

Re: Видимо,

(Link)
Это EWD1067, которая, насколько я понимаю, является наброском главы к какой-то книге.
(Reply) (Parent) (Thread)
[User Picture]
From:jedal
Date:November 17th, 2011 02:14 pm (UTC)

Re: Видимо,

(Link)
На картинку кликнуть я догадался, как раз :-) --- думал, м.б. Вы знаете книгу.
(Reply) (Parent) (Thread)
From:_qwerty
Date:August 16th, 2010 07:55 am (UTC)
(Link)
Мое отношение к доказательному программированию раз и навсегда изменилось после ознакомления с тремя неудачными попытками адептов формализовать стек конечной глубины.
(Reply) (Thread)
[User Picture]
From:furia_krucha
Date:August 16th, 2010 08:15 am (UTC)
(Link)
Адепты они такие. :-) Могут и про конечные автоматы не знать.
(Reply) (Parent) (Thread)
From:_qwerty
Date:August 16th, 2010 09:09 am (UTC)
(Link)
То были адепты АТД. Они честно старались в рамках собственных теорий. Про конечные автоматы они, конечно же, знали, но там были нужны модели совсем другого вида. И модеМногосортных алгебр тогда еще не использовали.
(Reply) (Parent) (Thread)
From:_qwerty
Date:August 16th, 2010 09:27 am (UTC)
(Link)
Они, кстати, не ограничивались конечным множеством помещаемых в стек значений, так что конечный автомат бы им не помог. Если же воспользоваться ограниченностью памяти реализующего стек компьютера, то размер полученного таким образом автомата был бы воистину ужасающ.
(Reply) (Parent) (Thread)
[User Picture]
From:furia_krucha
Date:August 16th, 2010 09:58 am (UTC)
(Link)
Так что они пытались сделать? Описать ADT "конечный стек" в некоем формализме? Построить формальную формальную теорию конечных стеков, адекватную ожидаемой модели?

Про пользу формальных методов говорит отношение плотности дефектов в software и hardware (конференции по формальным методам на 90% состоят из приложений к железу). Если бы аппаратное обеспечение делалось по методам software, инженеров Интела отлавливали бы на перекрёстках и били. :-)
(Reply) (Parent) (Thread)
From:_qwerty
Date:August 16th, 2010 06:46 pm (UTC)
(Link)
Описать конечный стек в двух формализмах.

Так нет - имеется намерение и две его реализации, одна на обычном языке программирования, другая в виде формализма. Формализм лучше в том смысле, что про него можно пытаться что-то доказывать, в т.ч. и автоматически. Но хуже длиной и заковыристостью. Вопросы установления соответствия намерения и обычной реализации формализму и интерпретации формально доказанного в рамках обычной реализации нетривиальны. Формальные методы не бесполезны, но граница их полезной применимости очень близка.
(Reply) (Parent) (Thread)