Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Прочитал я тут восхитительное творение МакБрайда про «Сражающие стрелки злого рока», это про то как на языке стрелок (если у нас есть зависимая теория типов) выражается логика Хоара. То есть то, как в идеале достигается максима «если в программе есть баги, она не компилируется». Всего лишь Хаскелл с зависимой системой типов и всё.


When two trains approach each other at a crossing, both shall come to a full stop and neither shall start up again until the other has gone.
— из законодательства штата Канзас.

Замкнутая система взаимодействующих экторов тоже может быть представлена в виде стрелки. По идее, её единственность её аппликабельности к потоку входящих событий, помеченyых «кому», должна означать отсутствие race conditions. Если система не имеет состояние «работа окончена», то отсутствие у неё (или её подсистем, определяемых через бинарную декомпозицию) терминальных состояний означают отсутствие «зависаний». Если таки состояние «система окончила работы», надо требовать, чтобы не было более одного терминального состояния, и чтобы приход к состоянию окончания работы мог случаться только в заранее определённых случаях (т.е. чтобы система не могла «вылетать» в результате странного стечения обстоятельств).

Единственное, что формализовать нельзя — это чтобы в результате стечения обстоятельств система не начала работать неправильно. Против этого нет приёма, кроме как смотреть глазами код. Ну и покрывать юнит-тестами, которые в свою очередь смотреть глазами и головой. А вот приёмы, как проверить степень покрытия юнит-тестами и найти пробелы, есть.

* * *

Напомню, что самая простая экторная модель такова: существует множество внутренних состояний. множество сообщений, которые эктор умеет обрабатывать, и множество сообщений, которые он умеет отсылать, плюс переходное отображение t: для каждой пары (состояние, последовательность исходящих сообщений) задаётся пара (новое состояние, последовательность исходящих сообщений). С эктором естественным образом ассоциирована категория, где объекты — состояния, а переходы — переходы, оснащённые последовательностью генерируемых при переходе исходящих сообщений. При композиции переходов, последовательности исходящих сообщений конкатенируются. Переходы считаются равными, если совпадают исходный и конечный пункт и последовательность исходящих сообщений (эффективное равенство). Можно ввести понятие внешне-неразличимых состояний, а также внешне-неразличимых состояний и внешне-неразличимых переходов при выбранном огрублении исходящих сообщений. Соответственно можно ввести понятие достижимых (в них есть переходы) и терминальных (из них нет выхода) состояний. Для полной проверки данного эктора с точностью до заданного огрубления, следует сделать по одному юниттесту на каждый класс эквивалентности use cases, где эквивалентными считаются use cases, которым соответствуют неразличимые по модулю заданного огрубления переходы. Количество таковых для сложных экторов или систем таковых может быть огромно, но к счастью, их число экспоненциально падает, если систему разбить на подсистемы, а в когерентности их взаимодействия убедиться, просмотрев все возможные диаграммы попарного диалога экторов, которые могут быть сгенерированны автоматически.
Subscribe

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 1 comment