Исправление SZT, (текущая версия) :
Я немного тыкал в ACLS. Интересная в общем-то штука, можно эти контракты переводить через Why3 в теоремы(код) на Coq и через Coq доказывать потом. Только это очень долго и муторно. Тебе это может быть нужно только если ты пишешь что-то очень серьезное, вроде софта для АЭС, авионики самолетов, прошивок для автомобилей, кардиостимуляторов. For safety- and security-critical software в общем. Но даже в таких областях на это часто забивают болт. А вот например прошивка для марсохода как раз писалась с использованием подобных инструментов
https://dev.by/news/marsokod-ili-kak-sozdavalos-po-dlya-marsohoda-curiosity
Инструмент Spin для проверки моделей специально предназначен для верификации программ, работающих в распределенных системах и имеющих множество потоков выполнения. Его внутренний проверочный алгоритм основан на методе формальной верификации с применением конечных автоматов, сформулированном Варди и Вольпером. Неформально Spin играет роль фонового планировщика процессов и пытается найти такие варианты выполнения кода в системе, которые нарушают требования, заданные пользователем. Простые примеры типов требований, выполнение которых может быть доказано или опровергнуто таким способом — допустимость программных утверждений и отсутствие сценариев, приводящих к возникновению взаимных блокировок. Но возможности программы для проверки моделей этим далеко не ограничиваются. Инструмент может верифицировать осуществимость или неосуществимость значительно более сложных требований, которые могут быть выражены средствами линейной темпоральной логики.
Исходная версия SZT, :
Я немного тыкал в ACLS. Интересная в общем-то штука, можно эти контракты в теоремы переводить через Why3 в теоремы на Coq и через Coq доказывать потом. Только это очень долго и муторно. Тебе это может быть нужно только если ты пишешь что-то очень серьезное, вроде софта для АЭС, авионики самолетов, прошивок для автомобилей, кардиостимуляторов. For safety- and security-critical software в общем. Но даже в таких областях на это часто забивают болт. А вот например прошивка для марсохода как раз писалась с использованием подобных инструментов
https://dev.by/news/marsokod-ili-kak-sozdavalos-po-dlya-marsohoda-curiosity
Инструмент Spin для проверки моделей специально предназначен для верификации программ, работающих в распределенных системах и имеющих множество потоков выполнения. Его внутренний проверочный алгоритм основан на методе формальной верификации с применением конечных автоматов, сформулированном Варди и Вольпером. Неформально Spin играет роль фонового планировщика процессов и пытается найти такие варианты выполнения кода в системе, которые нарушают требования, заданные пользователем. Простые примеры типов требований, выполнение которых может быть доказано или опровергнуто таким способом — допустимость программных утверждений и отсутствие сценариев, приводящих к возникновению взаимных блокировок. Но возможности программы для проверки моделей этим далеко не ограничиваются. Инструмент может верифицировать осуществимость или неосуществимость значительно более сложных требований, которые могут быть выражены средствами линейной темпоральной логики.