3.6. ПОДХОДЫ НА ОСНОВЕ ФОРМАЛЬНЫХ ПРЕОБРАЗОВАНИЙ

3.6. ПОДХОДЫ НА ОСНОВЕ ФОРМАЛЬНЫХ ПРЕОБРАЗОВАНИЙ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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