Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Categories:

Вынос из комментов


shmel39
Мне всегда было интересно как верифицировать программы математически. То есть я теоретически представляю как это должно происходить, но мозг отказывается представить верификацию чего-то больше чем на несколько экранов :-( Или все гораздо проще?



akuklev
А я, если честно не помню, где конкретно он вводил основные методы верификации.

Исторически идеи подходов к верификации возникают в 1930ые-40 годы в ряде перекликающихся работ фон Неймана с Уламом и Тьюринга с Чёрчем. Но методологии верификации алгоритмов у них нормальной не было, верификация использовала каждый раз разные подходы.

Чуть позже находится простая и хорошая методология для придания семантики (и вообще верификации) императивных программ: В 1969 году Хоар пишет An axiomatic basis for computer programming, где показывает, как надо описывать императивные инструкции, а именно — динамическим инвариантом.

An axiomatic basis for computer programming:
http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf

Потом они пишут вместе с Дейкстрой книжку Structured Programming, 1972 год. Там вводятся переходы динамических инвариантов для всех структурных элементов современного императивного программирования.

Хоаровский верификатор для подмножества Джавы:
http://isabelle.in.tum.de/Bali/

А потом Дейкстра проясняет десятки тонких вопросов и прорабатывает сотни примеров, либо выводя алгоритмы напрямую из желаемого результата (его основная методология), либо верифицируя уже существующие. В процессе он сильно расширяет возможности Хоаровской логики.
Дейкстра использует Хоаровскую логику для мультитрединговых систем — его язык вообще по определению мультитрединговый, он просто вводит семантику семафоров и других синхронизационных механизмов. В итоге он находит методологию верификации уже не просто алгоритмов, но уже систем.

Все это делается в разных местах. Синопсис в трёх основных книжках
- A Discipline of Programming, 1976.
- Selected Writings on Computing, 1982.
- A Method of Programming, 1988.

Но эволюция метода (и самое ценное) не в книжках, а в его бумажном блоге, который называется EWD. Он опубликован в инете полностью и его можно читать целиком день за днём, и будет страшный кайф. :-)

Надо сказать, это всё касается только императивного программирования. У функциональных языков программирования семантика задаётся, так сказать, автоматически. Дело в том, что Типизированное Тотальное Лямбда-Исчисление само по себе прекрасная семантическая система. В его рамках верификация кода делается так: Ставится утверждение, которое бы хотелось доказать для функции f, и оно доказывается структурной индукцией по лямбда-структуре f снизу до верху. Верификация обычно лёгкая как мёд, только привыкнуть надо.

Есть такой функциональный язык, как Хаскелл, который всем очень хорош, кроме отчасти синтаксиса, документации и подхода к работе с переменными.
(Исторически сложилось так, что mutables в Хаскелле ввели до того, как сообщество пришло к консенсусу, что взаимодействие со внешним миром надо делать чейнингом при помощи монад. Поэтому io в хаскелле кошерное и purely functional, а mutables сделаны отчасти через жопу. Но это нас не волнует, потому что как раз в алгоритмике роли вообще не играет.)
Так вот, Хаскелл использует Типизированое Лямбда-Исчисление. Любая верификация происходит так: вначале превращаем программу из просто лямбды в total лямбду на бумаге (т.е. снабжаем все рекурсивные функции натуральным уменьшающимся аргуметом, чтобы исключить бесконечную рекурсию), затем проводим индукцию по телу. Всё.

Ещё есть так называемое Function-Level programming, экстремально крутой подход, в котором возможные программы формируют модуль над алгеброй. Там верификация работает прикольными алгебраическими методами. Ладно, чего-то я слишком расписался. :-)

* * *

Ах да. Это я всё про верификацию алгоритмики писал. А ведь есть ещё верификация систем. Именно этим я занимался в посте. В общем, фон Нейман когда-то придумал Agent Based Model, из которого потом выросли Process Calculus со своими многочисленными потомками и Multiagent Systems со своими многочисленными графическими и игротеоретическими способами анализа.

Проверка по существу (Validation):
Первая стадия: Рисуем специальные диаграммы, на которых видны возможные collisions. На диаграммах reasoning'а это коллизии правил, на диаграммах доступа — коллизии доступа. Прорабатываем в голове все коллизии. 95% проблем становятся явными на этом уровне.
Эта ручная верификация, она не подлежит автоматизации. Т.е. рисовать диаграммы может сам контупер. Показывать потенциальные коллизии — тоже может. Но анализировать их должен программист. Головой.

Вторая стадия: (Не используется на практике никем вообще, но я надеюсь дожить до светлых времён, когда это изменится) Для всех существенно различных ситуаций пишется по юнит-тесту. То есть, по одному сценарию, который именно эту ситуацию учитывает. Это довольно много — для одного агента, тупо выполняющего ордера, пришедшие от клиентов, это 40-50 юнит-тестов. Однако плюс в том, что это полная, ультимативная, фактическая верификация поведения, лучше которой принципиально ничего нельзя придумать.
Эти сценарии показываются заказчику и если он с каждым из них согласен, то это значит, что система будет работать в точности как он хочет.

Детектировать "существенно разные" ситуации тоже можно автоматизированным способом. Существует дуальность между одной из современных process models и одной из современных agent models. (Грубо говоря, описание поведения агентов полностью описывает процессы между ними/внутри них и наоборот.)
Благодаря этой дуальности можно математически-чисто сформулировать, что такое "существенно разные ситуации" и автоматически находить водораздел между таковыми. Я два года назад писал об этом большую и заумную статью, правда сейчас мне стыдно за тамошний английский и вообще я был молодой и глупый, так что показывать я её не буду. :-)

Техническая проверка (Verification): Выставляем набор утверждений, которые нам бы хотелось доказать.
Делается это поаспектно. Технический аспект включает в себя отсутствие дедлоков и бесконечных рекурсий. Специфичные аспекты для приложений включают в себя специфичные требования. Примеры:
- Для микроядра Fiasco: full preemtibility.
- Для финансового движка: общая сумма денег в системе остаётся постоянной.

Требования формулируются на языке темпоральной логики какой-нибудь или пи-исчисления. Затем каждый их них доказывается структурной индукцией. Задача математика-верификатора — сформулировать требования. Доказательства же должны выполняться автоматизированной доказывающей системой. Theorem prover'ом. Когда прувер не может, он показывает программисту, где корень зла, и программист должен либо осознать дыру в коде, либо объяснить пруверу, почему это нифига не баг, а очень даже фича.
Именно так был верифицирован VFiasco и так сейчас верифицируется Coyotos.

Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

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

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

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

  • 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.
  • 4 comments