Методы верификации объектно–ориентированных программ
Верификация таких программ имеет свою специфику и ее можно рассматривать исходя из композиционного метода, применяя к ним известные методы доказательства правильности композиционных программ [14, 16, 17].
Выделим несколько этапов для верификации исходного проектирования объектных моделей и программ:
1. Верификация базовых (простых) объектов сводится к верификации структуры, где атрибуты объектов являются данными структуры, а внутренние операции объекта — функциями над этими данными.
2. Верификация объектов, построенных с помощью наследования, агрегации или инкапсуляции, осуществляется исходя из следующих предположений:
– базовые объекты считаются проверенными, если их операции (функции) приняты за теоремы;
– доказательство объектов сводится к этим теоремам;
– доказывается, что все операции, которые применяются над подобъєктами, не выводят их из множества состояний, для которых они верифицированы.
3. Верификация интерфейсов объектов сводится к доказательству:
– правильности данного интерфейса;
– достаточности параметров интерфейса.
Метод верификации ООП на основе композиционного подхода можно использовать как “вниз” так и “вверх”. Сначала доказывается правильность построенной ОМ для некоторой ПрО. Верификация ОМ требует реализации на этапах ЖЦ следующих вопросы:
– удаление лишних атрибутов объектов и их интерфейсов в ОМ, внесение необходимых изменений и повторное доказательство правильности объекта;
– выбор типа множества для атрибутов объекта и проверка реализации операций и множество значений этого типа.
Правильность спецификаций любого объекта ПС доказывается независимо от правильности смежных объектов и верификации их интерфейсов. Это является заключительной проверкой ОМ.
