July 4th, 2009

with Cat The Cat

Некоторая мысль.

Я являюсь обладателем и читателем интересной книги под названием Program Construction: Calculating Implementations from Specifications.

В ней сперва рассказывается про булеву логику (и даются интересные задачи про воинов и воров), а затем объясняются тройки Хоара. Там очень интересно, например, как они исправляют деление по модулю в Джаве (все примеры программ там на Джаве).

Если кто не помнит, то тройки Хоара это вот: {P} S {Q}, где {P} - множество предусловий для выполнения действия S, {Q} - множество выполняющихся после S постусловий. Если мы должны выполнить два последовательных действия S1 и S2, то их пред- и постусловия объединятся (для независимых S1 и S2 это будет P1∧P2 и Q1∨Q2, для зависимых действий посложнее, но тоже можно вывести). С их помощью программисты тех времен изобретали весьма тонкие алгоритмы, особенно хорошо это получалось у Дейкстры.

Я вспомнил о ней из-за обсуждения на RSDN. В нём два участника обсуждения практически в голос говорили, что спецификация кода практически всегда окажется больше самого кода. Дескать потому, что на каждую строку кода придётся указывать очень много всего.

Вспомнил я про эту книгу в контексте того обсуждения потому, что я немного потренировался программировать с тройками Хоара. Как и говорилось в книге, оказалось достаточно правильно сформировать пред- и постусловия, и большая часть решений по построению алгоритма выполняется выбором всего из одного варианта. Нам надо что-то сделать с массивом? Цикл. Надо, чтобы в какой-то части решения i всегда было не равно 0 и мы можем вернуть признак ошибки? Проверим на 0 и вернём ошибку. И тп.

Это не механический труд, всё равно. При программировании с использованием троек Хоара всё равно придётся формировать словарь-библиотеку, что снизу, что сверху. То, насколько часто будет встречаться выбор всего из одного варианта и даёт некоторое представление о качестве словаря. Всё равно придётся оценивать последствия решений и прочее такое же. Это не панацея, а просто ещё один способ выполнения работы, очень развивающий.

Здесь что интересно. S1 может нарушить что-то из его предусловий P1, поэтому если S2 требует это что-то, разрушенное S1, надо провести восстановление. Это связано с наличием побочных эффектов. В случае чисто функционального кода тройки превращаются в обычную логику (структурное исчисление секвенций, так сказать), что сильно упрощает работу. Достигли P1 и P2 им полностью покрывается? Беспокоиться не о чем, можно выполнять и S1 и S2. А сами S1 и S2 могут быть записаны так: S1 :: P1 -> Q1, S2 :: P2 -> Q2. Это обычные чистые функции.
with Cat The Cat

Фильм по компьютерной игре.

Их было достаточно: Tomb Raider, DOA, Mortal Combat.

На этот раз всё по другому: компанией Universal приобретены права на игру Астероиды.

(флешовый вариант, чтобы ознакомиться, что к чему. Там можно крутиться и стрелять, а ещё и летать взад-вперёд.)