Методы и средства инженерии программного обеспечения



         

Методы верификации объектно–ориентированных программ


 

Верификация  таких программ имеет свою специфику и ее можно рассматривать исходя из композиционного метода, применяя к ним известные методы доказательства  правильности композиционных программ [14, 16, 17].

Выделим несколько этапов для верификации исходного проектирования объектных моделей и программ:

1. Верификация базовых (простых) объектов сводится к верификации структуры, где атрибуты объектов являются данными структуры, а внутренние операции объекта — функциями над этими данными.

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

– базовые объекты считаются проверенными, если  их операции (функции) приняты за теоремы;

– доказательство  объектов сводится  к этим теоремам;

– доказывается, что все операции, которые применяются над подобъєктами, не выводят их из множества состояний, для которых они верифицированы.

3. Верификация интерфейсов объектов сводится к доказательству:

 – правильности данного интерфейса;

–   достаточности параметров интерфейса.

Метод верификации ООП на основе композиционного подхода можно использовать как “вниз” так и “вверх”. Сначала  доказывается правильность построенной ОМ для некоторой ПрО. Верификация ОМ требует реализации на этапах ЖЦ следующих   вопросы:

– удаление лишних атрибутов объектов и их интерфейсов в ОМ, внесение необходимых изменений и повторное доказательство правильности объекта;

– выбор типа множества для атрибутов объекта и проверка  реализации  операций и множество значений этого типа.

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

                   

       




Содержание  Назад  Вперед