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

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

Технология стерильного цеха

Основные идеи технологии стерильного цеха (cleanroom process model) были предложены Харланом Миллзом в середине 80-х годов XX века. Технология складывается из следующих частей (рис. 19.9):

• разработка функциональных и пользовательских спецификаций;

• инкрементальное планирование разработки;

• формальная верификация;

• статистическое тестирование.

Процесс проектирования связан с представлением программы как функции в виде так называемых «ящиков»:

• черного ящика с фиксированными аргументами (стимулами) и результатами (ответами);

• ящика с состоянием, в котором выделяется внутреннее состояние;

• прозрачного (белого) ящика, представляющего реализацию в виде совокупности функций при пошаговом уточнении.

Использование ящиков определяют следующие три принципа:

Рис. 19.7. Технология стерильного цеха

• все определенные при проектировании данные скрыты (инкапсулированы) в ящиках;

• все виды работ определены как использующие ящики последовательно или параллельно;

• каждый ящик занимает определенное место в системной иерархии.

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

Прозрачный ящик получаем из ящика с состояниями, определяя процедуру, выполняющую требуемое преобразование. Таким образом, прозрачный ящик — это просто программа, реализующая соответствующий ящик с состоянием.

Однако в данной технологии отсутствует такой вид работ, как отладка. Его заменяет процесс формальной верификации. Для каждой управляющей структуры проверяется соответствующее условие корректности.

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

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