kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

По поводу верификационных тулов

Надо понимать, что задача "гарантировать абсолютную правильность программы" - это если и возможный, то труднодостижимый максимум. Реально ставится задача "снизить вероятность ошибки" и по возможности вытеснить ошибки в относительно небольшие и явно известные части кода - библиотеки, те же верификаторы.

В случае универсальных библиотек и верификаторов надежность повышается еще и за счет эффекта их массового использования - что опять же - снижает вероятность незамеченной ошибки

Во-вторых - верификатор строго говоря не доказывает правильность программы - он доказывает соответствие кода некоторым формальным утверждениям о его свойствах.

Во-третьих - в остальном есть два опять же варианта:

1) максималистский - прописывается формально вся существенная семантика, и в случае если верификатор не справляется (а это в случае сложных условий довольно обычная ситуация), ему объясняют "что и как" вручную*

2) минималистский - всякие фичи типа приведеных выше используются по принципу "что удалось формализовать и проконтролировать - то и формализуем и контролируем". По мне тут удается формализовать довольно много и я бы очень бы непротив иметь подобную функциональность и в обычных приложениях. В частности потому что она неплохо подстраховывает от привнесения ошибок при модификации кода.

*) По поводу того что "все доказать невозможно - ибо Гедель и Тьюринг" - тут дело такое - автоматически - да - невозможно. Но вот проверить доказательство - не просто возможно - но и очень просто - и эти системы как правило и позволяют если автоматически не удалось доказать - просто выписать ключевые моменты доказательства вручную (что заметно более трудоемко - но и только) - после чего система без особых затруднений проверяет/доказывает его.

А выписать доказательство возможно всегда, когда автор кода действительно понимает почему он должен работать так как он хочет.
Subscribe

  • В казани грят какая-то "трагедия"

    Уже даже не смешно - учителок постреляли - этих и вовсе не жалко - ну школоту тоже прибрали - тоже не жалко

  • "Вам Шура не завидно? Мне завидно"

    Ко Дню Победы, Илон Маск и компания SpaceX осуществили десятый повторный полет первой ступени. Ускоритель Falcon 9 Block 5 под номером B1051 поднялся…

  • "Иликой пабеды прозник"

    Щас subj положено плясать - хотя нынешняя россияния имеет к нему примерно столько же как и украиния. Эту войну выиграли совсем другие страны. И…

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

  • В казани грят какая-то "трагедия"

    Уже даже не смешно - учителок постреляли - этих и вовсе не жалко - ну школоту тоже прибрали - тоже не жалко

  • "Вам Шура не завидно? Мне завидно"

    Ко Дню Победы, Илон Маск и компания SpaceX осуществили десятый повторный полет первой ступени. Ускоритель Falcon 9 Block 5 под номером B1051 поднялся…

  • "Иликой пабеды прозник"

    Щас subj положено плясать - хотя нынешняя россияния имеет к нему примерно столько же как и украиния. Эту войну выиграли совсем другие страны. И…