![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sab123Первая часть: http://sab123.livejournal.com/324552.html
В-общем, прочитал я его книжку более-менее. Долго и упорно читал-старался и ждал, когда наконец-то расскажут про пользу от его моделей и то, как проводится автоматический анализ на его нотации. Дочитал первую часть, так и не рассказали, плюнул, остальное быстро пролистал в поисках.
В-общем, оказалось, что он любит свою нотацию графов состояний как самоцель, и считает, что просто записывание алгоритма в ней способствует глубокому пониманию. Нотация при этом чрезвычайно корявая и непригодная для потребления людьми. Я вижу, почему она может быть подходящей для доказательств и автоматического анализа, но по уму язык описания должен быть более человеческим, и транслироваться в машинопригодную форму автоматически. Ну, и при нормальном программировании обычная программа гораздо более читаема, понятна и пригодна для поиска ошибок человеком. Выигрыш в понимании при записывании в его нотации получается только если изначальная программа написана косоруко, без разделения слоев абстракций, а просто смешав все в кашу (угу, деятели От Науки любят так писать программы). Но всех делов-то - писать не косоруко.
Про автоматический анализ оказалось, что его не совсем нет, но его написал во-первых не сам гуру, во-вторых он убогий: все, что они сподобились сделать - это суметь прогнать модель через некоторое количество всевозможных шагов из изначального состояния и проверить, что условия правильности в них не нарушены. Но прохождение всех возможных путей быстро ведет к комбинаторному взрыву. Надежда тут только на то, что граф состояний небольшой, что позволит многим путям сомкнуться в те же состояния, и таким образом можно будет пообрубать дупликаты и пройти все возможные пути за это небольшое количество шагов. Но на самом деле описание такое, что граф обычно оказывается почти бесконечным. Теоретически может быть возможно свернуть этот граф во что-то более конечное через нахождение эквивалентных состояний, но это нетривиально и они этого не делают.
Это при том, что толковая идея для автоматического анализа у него таки присутствует, прям в первой части. Но почему-то они не почухались ее реализовать. Идея такая: выделить в большой модели разные маленькие аспекты. Описать и промоделировать каждый аспект отдельно, и убедиться, что он правильный. После чего доказать, что полная модель эквивалентна в каждом аспекте маленькой модели этого аспекта, и он не оказался испорченным в процессе объединения. Доказать такую эквивалентность можно даже для бесконечных графов.
В-общем, прочитал я его книжку более-менее. Долго и упорно читал-старался и ждал, когда наконец-то расскажут про пользу от его моделей и то, как проводится автоматический анализ на его нотации. Дочитал первую часть, так и не рассказали, плюнул, остальное быстро пролистал в поисках.
В-общем, оказалось, что он любит свою нотацию графов состояний как самоцель, и считает, что просто записывание алгоритма в ней способствует глубокому пониманию. Нотация при этом чрезвычайно корявая и непригодная для потребления людьми. Я вижу, почему она может быть подходящей для доказательств и автоматического анализа, но по уму язык описания должен быть более человеческим, и транслироваться в машинопригодную форму автоматически. Ну, и при нормальном программировании обычная программа гораздо более читаема, понятна и пригодна для поиска ошибок человеком. Выигрыш в понимании при записывании в его нотации получается только если изначальная программа написана косоруко, без разделения слоев абстракций, а просто смешав все в кашу (угу, деятели От Науки любят так писать программы). Но всех делов-то - писать не косоруко.
Про автоматический анализ оказалось, что его не совсем нет, но его написал во-первых не сам гуру, во-вторых он убогий: все, что они сподобились сделать - это суметь прогнать модель через некоторое количество всевозможных шагов из изначального состояния и проверить, что условия правильности в них не нарушены. Но прохождение всех возможных путей быстро ведет к комбинаторному взрыву. Надежда тут только на то, что граф состояний небольшой, что позволит многим путям сомкнуться в те же состояния, и таким образом можно будет пообрубать дупликаты и пройти все возможные пути за это небольшое количество шагов. Но на самом деле описание такое, что граф обычно оказывается почти бесконечным. Теоретически может быть возможно свернуть этот граф во что-то более конечное через нахождение эквивалентных состояний, но это нетривиально и они этого не делают.
Это при том, что толковая идея для автоматического анализа у него таки присутствует, прям в первой части. Но почему-то они не почухались ее реализовать. Идея такая: выделить в большой модели разные маленькие аспекты. Описать и промоделировать каждый аспект отдельно, и убедиться, что он правильный. После чего доказать, что полная модель эквивалентна в каждом аспекте маленькой модели этого аспекта, и он не оказался испорченным в процессе объединения. Доказать такую эквивалентность можно даже для бесконечных графов.
