Можно ли принудительно проверить проверки по контракту во время компиляции?

Question

Чтение Учебное пособие по дизайну по контракту Я наткнулся на следующую строку:

Контракты в Eiffel - это не просто желаемое за действительное.Они могут контролироваться во время выполнения под контролем параметров компиляции.

с последующими объяснениями, что они будут генерировать исключения при сбое.Это заставляет меня думать, что все проверки require ensure invariant all могут быть выполнены во время выполнения или отключены.Это правильно?Или они могут быть применены также во время компиляции, используя соответствующие параметры компилятора?

Answer 1

Существует инструмент AutoProof для проверки контрактов во время компиляции.Он выполняет некоторые преобразования, заканчивающиеся экземпляром SMT, который проверяется решателем SMT Z3, который сообщает, выполняются ли все утверждения.Из краткого введения следует, что для его использования требуется немало аннотаций.Тем не менее, этот инструмент использовался для проверки Base2 , набора контейнерных классов, аналогичных стандартным классам библиотеки Base .Контракты основаны на так называемой методике Semantic Collaboration , описанной в соответствующих статьях (см. Publications на странице AutoProof page ).

ТамВ настоящее время ведется научно-исследовательская работа , призванная упростить методы, используемые AutoProof, исправить существующие проблемы, адаптировать ее для использования с void-safe системами и SCOOP (Simple Concurrent Object-Ориентированное программирование).На момент написания статьи технология все еще находится на стадии исследования и не готова к первичному использованию в производственной среде.Основным препятствием является сложность и специальная подготовка, необходимая для использования технологии.Тем не менее, основные идеи довольно общие, что позволяет использовать инструмент в учебном процессе.