Интернет магазин китайских планшетных компьютеров

Компьютеры - Формальные методы - Разновидности формальных методов

Можно выделить три уровня применения формальных методов:

Нулевой уровень

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

Первый уровень

Программный код выводится из формальной спецификации автоматически, используются механизмы верификации, доказываются наиболее критичные свойства системы. Этот путь зачастую выбирается для высокоточных систем.

Второй уровень

Автоматические доказатели теорем используются для выведения полностью формализованных доказательств, проверяемых автоматически. Подход требует объёмных вложений и исследований, но оправдывает себя в самых критичных частях сложных систем, где ошибки непозволительны.

Подходы к формальным методам также можно классифицировать аналогично формальной семантике языков программирования:

Денотационная семантика

Значение системы выражается через частично упорядоченные множества, а методы полагаются на хорошо разработанную теорию вокруг них. Ограничение метода — в том, что не каждая система может быть интуитивно или естественно рассмотрена как функция.

Операциональная семантика

Значение системы обозначается последовательностью действий в рамках более простой вычислительной модели. Методы славятся своей простотой, если не акцентировать внимание на том, что они полагаются на семантику «более простой» системы, которую тоже надо через что-то определять.

Аксиоматическая семантика

Смысл системы определяется в терминах предусловий и постусловий, что позволяет связать теорию с классической логикой, но не даёт представления о том, что конкретно происходит внутри системы.

Кроме того, нередко резко положительных результатов можно достичь, пожертвовав глобальной применимостью и сверхформализацией — такие случаи называют «облегчёнными» формальными методами. Их можно разделить на два типа: с усиленной и с ослабленной автоматизацией. Пример усиленной автоматизации — анализатор спецификаций Alloy Analyzer, который для того, чтобы свести задачу поиска модели к решаемой, сужая область поиска. Пример ослабленной — сходимость грамматик, в которой неразрешимость задачи эквивалентности двух формальных языков обходится тем, что преобразования совершает сам человек, а выводы делаются уже по свойствам использованных им операторов.