Формальные спецификации по

Традиционные технические дисциплины, такие, как электротехника или гражданское строительство, обычно легко адаптируют лучшие математические методы. Например, в машиностроении не возникало трудностей с применением методов математического ана­лиза. Однако инженерия программного обеспечения не идет таким путем. Хотя прошло более 25 лет исследований по использованию математических методов в процессе созда­ния ПО, воздействие этих методов все же ограниченно. Так называемые формальные ме­тоды разработки программных систем широко не используются. Многие компании, раз­рабатывающие ПО, не считают экономически выгодным применение этих методов в про­цессе разработки.

Термин "формальные методы" подразумевает ряд операций, в состав которых входят создание формальной спецификации системы, анализ и доказательство спецификации, реализация системы на основе преобразования формальной спецификации в программы (см. главу 3) и верификация программ. Все эти действия зависят от формальной специфи­кации программного обеспечения. Формальная спецификация — это системная специфи­кация, записанная на языке, словарь, синтаксис и семантика которого определены фор­мально. Необходимость формального определения языка предполагает, что этот язык ос­новывается на математических концепциях. Здесь используется область математики, которая называется дискретной математикой и основывается на алгебре, теории мно­жеств и алгебре логики.

Формальные спецификации в процессе разработки по

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

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

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

Рис. 9.1. Разработка спецификации и проектирование

Рис. 9.2. Разработка формальной спецификации

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