Формальные спецификации, доказательство и верификация программ

Разработка спецификации проводится по следующей схеме:

Определение терминов, которыми будет специфицироваться программа.

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

Описание инвариантных свойств программы.

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

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

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

Для демонстрации возможностей VDM языка рассмотрим задачу поиска ("Поиск") в каталоге ( $$catalR$$ ) репозитария компонентов имени компонента $$С$$ и сравнения его с заданным в запросе пользователя. В случае совпадения имен проверяются параметры, и при их совпадении из каталога извлекается код компонента и передается пользователю.

Спецификация переменных программы "Поиск"

$$\begin{array}{rcrl} repoz :: = developеrs : dl \to Init - set \\ catalR: cat \to Init - set \\ role : inst \to facet \\ facet :: = autors: Milk \\ title : N \\ user :: = developer : Itn \\ free : Bool, \end{array}$$

где $$developers$$ - cведения о разработчике компонента $$С$$ ; $$facet$$ - переменная, в которую посылается код компонента, выбранного из каталога $$catalR$$ репозитария $$repoz$$ при совпадении имен в каталоге и запросе; $$role$$ - переменная, в которой хранится текущий элемент из репозитария, найденный по фасете компонента с номером $$N$$ для $$user$$ ; $$autors: Milk$$ - имя разработчика компонента; $$free: Bool$$ - переменная, которая используется для задания признака - компонент не найден или к нему никто не обращался.

Описание инвариантных свойств программы

$$\begin{array}{l} type \;inv - repoz: repoz \to Bool \\ inv - repoz (dev) = \\ let\; mk \; repoz (cd, c, role) = dev\;in \\ (\forall i \in dom \; cd)\\ (\forall i \in cd (i)\\ ((\exists j \in dom \;cd\; \ \;i \in c) \;\\; \exists a \in elems\;role (i)\text{, }autors (a \in dom cd)\\ \\; free = false \Leftrightarrow developer = catalR \;\\; facet (N) = role \dots \end{array}$$

Операторы программы проверяют список имен компонентов в каталоге, который содержит $$N$$ элементов типа $$set$$. Если они совпадают с именем в запросе, результат сохраняется в $$role$$.

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

6.1.2. Спецификация программ средствами RAISE

RAISE-метод и RSL-спецификация (RAISE Specification Language) [6.9, 6.10] были разработаны в 80-х годах как результат предварительного исследования формальных методов и их пополнения новыми возможностями. Метод содержит нотации, техники и инструменты для конструирования программ и доказательстве их правильности. Он имеет программную поддержку в виде набора инструментов и методик, которые постоянно развиваются и используются при доказательстве правильности программ, описанных в RSL и ЯП (С++ и Паскаль). Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации) и конкретные типы данных (модельноориентированные), подтипы, операции для задания последовательных и параллельных программ. Он предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также формальное конструирование программ в других ЯП и доказательство их правильности. Синтаксис этого языка близок к синтаксису языков С++ и Паскаль.

В RSL-языке имеются предопределенные абстрактные типы данных и конструкторы сложных типов данных, такие как произведение ( $$product$$ ), множества ( $$sets$$ ), списки ( $$list$$ ), отображения ( $$map$$ ), записи ( $$record$$ ) и т.п. Далее рассмотрим некоторые конструкторы сложных типов данных.

Произведение типов - это упорядоченная конечная последовательность типов $$Т_{1}, Т_{2}, \dots, Т_{n}$$ произведения ( $$product$$ ) $$Т _{1} \times Т_{2} \times, \dots, \times Т_{n}$$. Представитель типа имеет вид ( $$v_{1}, v_{2} , \dots, v_{n}$$ ), где каждое $$v_{i}$$ -это значение типа $$Т_{i}$$. Компонент произведения можно получить операцией $$get$$ и переслать $$set$$, т.е.

$$\begin{array}{l} get\;component(i, d) = get\;value(i, d), \\ set\;component(d, i, val) = d \Rightarrow \nabla(I \to val). \end{array}$$

Количество компонентов произведения d находится таким образом:

$$size (d) = id \nabla (null (couter inc(counter))).$$

Конструктор произведения $$d_{1}$$ и $$d_{2}$$ строит произведение $$d_{1} \times d_{2}$$ вида:

$$product (d_{1}, d_{2}) = id \nabla (size(d_{1}) \Rightarrow couter\;1) \nabla (null (couter\;2) inc\; couter\; 2))).$$

Для каждого конкретного типа $$product(Т_{1} \times Т_{2} \times, \dots, \times Т_{n})$$ можно построить конструктор значения этого типа из отдельных компонентов произведения таким образом:

$$make\; product (value_{1}, \dots, value_{n}) = (value_{i} \Rightarrow 1) \nabla \dots \nabla (value_{n} \Rightarrow n),$$

где каждое значение $$value_{i}$$ имеет тип $$Т_{i}$$, а результирующее значение - тип произведения $$Т_{1} \times Т_{2} \times, \dots, \times Т_{n}$$

Списки типов - это последовательность значений одного типа $$list\;Т$$, могут быть конечным списком типов $$Т^k$$ и неконечными списком типов $$T^n$$. В качестве структур данных типа списка может быть бинарное дерево, в котором есть голова ( $$head$$ ) и сын ( $$tail$$ ), который следует за ним в списке, и хвост. К операциям списка относится операция $$hd$$ - взятия первого элемента списка, т.е. головы, и операция $$tl$$ - хвоста остальных элементов (аналогично как в VDM).

Функция $$Caddr (I) = L \Rightarrow tail \Rightarrow tail \Rightarrow Head$$ выбирает из списка $$I$$ -элемент. Индекс элемента помогает выбрать нужный элемент списка:

$$Index(I, idx) = L(idx) = \text{ while }(\neg \text{ is }null(idx))\text{ do }((L \Rightarrow tail \Rightarrow L) \nabla dec(idx)) L \Rightarrow Head.$$

Для определения количества элементов в списке выполняется функция:

$$\begin{array}{l} len (L) = (ld\; \nabla\; null (result)) \\ \text{while }(L \Rightarrow)\text{ do }(( L \Rightarrow tail \Rightarrow tail \Rightarrow L)\; \nabla\; inc (result)) \\ result \Rightarrow. \end{array}$$

Элемент списка находится так:

$$\begin{array}{l} elem (L) = (ld\; \nabla \;empty (result)) \\ \text{while }(L \Rightarrow)\text{ do }(( L \Rightarrow tail \Rightarrow L)\; \nabla \\ (result \uparrow ( L \Rightarrow head \Rightarrow) \Rightarrow elem ) \Rightarrow result) \\ result \Rightarrow. \end{array}$$

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

Отображение - это структура ( $$map$$ ), которая ставит в соответствие значениям одного типа значение другого типа. Вместе с тем отображение - это бинарное отношение декартова произведения двух множеств как совокупности двухкомпонентных пар, в которых первый компонент - $$arg$$ содержит элементы аргументов отображения, а второй компонент $$res$$ - соответствующие элементы значений этого отображения.

В языке имеются разные допустимые операции над отображениями: наложение, объединение, композиция, срез и др. Среди этих видов отношений рассмотрим, например, композицию отображений ( $$m_{1}$$, $$m_{2}$$ ):

$$\begin{array}{l} (ld\;\nabla\; (compose (m_{1}, m_{2}) \Rightarrow m))\;apply\;(m, elem) \\ apply\; to\; composition\;(m_{1}, m_{2}, elem) =\\ =(ld\; \nabla\; (image (elem, m1)\Rightarrow s)\;restrict\;(m_{2}, s) \Rightarrow map \\ (ld\; \nabla\; (map\text{ getname }elem \Rightarrow name))\;getvalue\;(name, map). \end{array}$$

При этом используются функции:

$$\begin{array}{l} \text{Apply (}m\text{, elem) = image (elem,}m)\text{ elem }\Rightarrow, \\ \text{Apply (}m\text{, elem) = getvalue (elem,}m)\text{ elem }\Rightarrow. \end{array}$$

Запись - это совокупность именованных полей. Этот тип соответствует типу $$record$$ в языке Паскаль и $$struct$$ в языке С++. В языке RAISE для записи определено два конструктора - $$record$$, $$shurt record$$, описание которых имеет вид

$$\begin{array}{l} type\; record\; id =\\ type\; mk\_id\; (short _record\; id ) ::=\\ destr\_id_{1} : type\_expr_{1} \leftrightarrow recon\_id\\ \;\;\;\;\;\;\dots\\ destr\_id_{n} : type\_expr_{n} \leftrightarrow recon\_id. \end{array}$$

Идентификатор $$mk\_id$$ - это конструктор типа $$record$$, для которого задается деструктор $$destr\_id_{n}$$ как функции получения значения компонентов записи.

Объединение - это конструктор $$union$$ для объединения типов $$type id = id_{1} , id_{2} ,\dots, id_{n}$$, при котором тип $$id$$ получает одно из значений в списке элементов.

Конструктор типа имеет вид

$$\text{type }id = id \text{\_from\_} id_{1}(id \text{\_to\_} id_{1:} id_{1})\;|\;\dots\;| \; id \text{\_from\_} id_{n}(id\text{\_to\_}idn_{:} id_{n}).$$

Операции над самим типом не определены в языке RAISE.

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

6.1.3. Спецификации задач концепторным языком

Для постановки сложных математических задач (суммирование бесконечных рядов, теоретикомножественных операций с бесконечными множествами, гильбертов оператор и др.) и задач искусственного интеллекта (игры, распознавание образов и др.) предложен общематематический процедурный язык, так называемый концепторный язык - КЯ [6.17]. В этом языке процесс описания сложной задачи проводится путем обоснования решения задачи с математической точки зрения, затем формального описания постановок задач и, наконец, делается переход к алгоритмическому описанию.

Средства спецификации сложных задач.Основу КЯ составляет теоретикомножественный язык, который содержит декларативные и императивные средства теории множеств ЦермелоФренкеля. Ядро содержит набор элементов (типы, выражения, операторы) и средства определения новых типов, выражений и операторов.

Декларативные средства КЯ - это типизированный, многосортный логикоматематический язык задания выражений и структуризации множества значений (денотат). Выражения состоят из термов и формул, термы обозначают объекты ПрО, а формулы - утверждения об объектах и отношениях между ними. К конструкторам составных типов и формул относятся функторы, предикаты, конекторы и субнекторы.

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

Императивные средства КЯ - это операторы и процедуры для описания объектов ПрО с помощью концепторов, состоящих из разделов для определения объектов решаемой задачи и действий над ними. Каждый концептор - это именованный набор определений и действий со следующей структурой описания:

концептор К (< список параметров >)
 <список импортных параметров>
 <определение констант, типов, предикатов>
 <описание глобальных переменных>
 <определение процедур> 
 начало К
 <тело концептора> 
 конец К.

Концептор - это декларативное описание объектов и императивное описание операторов вычисления выражений тела. Рассматривается два случая:

декларативный концептор состоит из определений параметров и типов;

императивный концептор - это тело из операторов задач.

Декларативный концептор задает описание объектов и понятий, связанных с математической постановкой задачи, а описание метода ее решения с помощью императивных концепторов. Концепторное описание - это формальная спецификация задачи, которую можно трансформировать до алгоритмического описания и верификации.

Если полученный концептор неэффективен, то для повышения эффективности строится алгоритм, эквивалентный данному концептору. Он строится аппроксимацией концепторного решения путем замены неконструктивных объектов и неэффективных операций конструктивными и более эффективными аналогами.

Формализация КЯ. Общая схема формализации декларативной и императивной частей КЯ расширяется логикоматематическим языком, традиционными структурными операторами (присваивание, последовательность, цикл и т.п.), а также теоретикомодельными (денотационными) и аксиоматическими средствами формализации неконструктивной семантики КЯ.

Денотационный подход состоит в определении семантики языка путем подстановки каждому выражению соответствующего элемента из множества денотатов функции $$\phi$$ интерпретации символов сигнатуры языка. Каждой константе $$c \in C$$, функциональному символу $$f \in F$$ и предикатному символу $$p \in P$$ сопоставляется объект из множества денотат. Этот способ интерпретации семантики выражений и операторов языка аналогичен денотационной семантики ЯП. Главное отличие семантики КЯ от семантики программ - это ее неконструктивность. С каждым КЯ можно связать некоторую дедуктивную теорию, которая отражает свойства концепторов.

Формальная дедуктивная теория строится путем выделения из множества всех формул подмножества аксиом и правил вывода. Для каждой пары $$R_{1}$$, $$R_{2}$$ формул дедуктивной теории и каждого оператора $$І$$ создается операторная формула $$\{R_{1}\}I\{R_{2}\}$$ с утверждением, что если $$R_{1}$$ истинно перед выполнением оператора $$I$$, то завершение оператора $$I$$ обеспечивает истинность $$R_{2}$$, т.е. формула $$R_{1}$$ - предусловие, а $$R_{2}$$ - постусловие оператора $$I$$. С помощью неконструктивных объектов и неразрешимых формул этой теории можно адекватно описывать свойства неэффективных процедур.

Аксиоматическое описание КЯ - это аксиомы и утверждения относительно концепторного описания и проведения дедуктивного доказательства и верификации этого описания.

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

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

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

На втором этапе система $$S$$ детализируется в виде совокупности взаимозависимых подсистем $$S_{1} , \dots, S_{n}$$, каждая из которой описывается алгебраической спецификацией. В результате получается спецификация системы $$S$$ из функций переходов и выходов, для которых необходимо доказывать корректность. Процесс детализации выполняется на уровне элементной базы или элементарных программ и сопровождается доказательством их корректности. В конечном итоге получается система S, эквивалентная исходной спецификации. Примеры доказательства систем приведены в [6.17]. Рассмотрим один из них.

Пусть требуется построить спецификацию натуральных чисел из множества этих чисел с сигнатурой операций $$\sum = (+, \times, \le)$$. При построении используется число $$0$$ и функция следования $$s: N \to N^\prime$$. Спецификация состоит из следующих аксиом:

$$х + 0 = x$$,

$$x + s(y) = s (x + y)$$,

$$x \times 0 = 0$$,

$$x + s(y) = s (x \times y) + x$$,

$$0 \le x$$,

$$x \le y \supset s(x) \le s(y)$$

$$s(x)< s(y) \supset x \le y$$

При этом алгебраические системы становятся многоосновными алгебрами, а аксиомы - спецификациями: тождественными и квазитождественными. Алгебраические спецификации - наиболее используемые, поскольку для них существуют эффективные алгоритмы выполнения, которые преобразуют спецификации в ЯП высокого уровня. Поэтому такие языки называют языками выполняемых логико-алгебраических спецификаций. Их операционная семантика основана на переписывании термов, а создаваемая алгебраическая спецификация получает логическую семантику, используемую при доказательстве теорем.

6.2. Методы доказательства правильности программ

Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и аппарат вывода. Правила доказательства являются громоздкими и поэтому на практике редко используются рядовыми программистами. Однако с теоретической точки зрения они развивают логику применения математического метода индукции при проверке правильности программ. На основе спецификации программ проводится частичное и полное доказательство правильности программ [6.4, 6.5].

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

Для доказательства частичной правильности используется метод индуктивных утверждений, сущность которого состоит в следующем. Пусть утверждение $$А$$ связано с началом программы, $$В$$ - с конечной точкой программы и утверждение $$С$$ отражает некоторые закономерности значений переменных, по крайней мере, в одной из точек каждого замкнутого пути в программе (например, в циклах). Если при выполнении программа попадает в $$i$$ -ю точку и справедливо утверждение $$A_{i}$$, а затем она проходит от точки $$i$$ к точке $$j$$, то будет справедливо утверждение $$A_{j}$$.

Теорема 6.1. Если выполнены все действия метода индуктивных утверждений для программы, то она частично правильна относительно утверждений $$А$$, $$В$$, $$С$$.

Требуется доказать что, если выполнение программы закончится, то утверждение $$В$$ будет справедливым. По индукции, при прохождении точек программы, в которых утверждение $$С$$ будет справедливым, то и $$n$$ -я точка программы будет такой же. Таким образом, если программа прошла $$n$$ -точку и утверждения $$А$$ и $$В$$ справедливы, то тогда, попадая из $$n$$ -ой точки в $$n+1$$ точку, утверждение $$A_{n+1}$$ будет справедливым, что и требовалось доказать.

6.2.1. Характеристика формальных методов доказательства

Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. [6.4, 6.5, 6.18, 6.19].

Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе пересекал хотя бы одну контрольную точку. Для этих точек формулируются утверждения о состоянии и значениях переменных в них (для циклов эти утверждения должны быть истинными при каждом прохождении циклаинварианта).

Каждая точка рассматривается для индуктивного утверждения того, что формула остается истинной при возвращении в эту точку программы и зависит не только от входных и выходных данных, но и от значений промежуточных переменных. На основе индуктивных утверждений и условий на аргументы создаются утверждения с условиями проверки правильности программы в отдельных ее точках. Для каждого пути программы между двумя точками устанавливается проверка на соответствие условий правильности и определяется истинность этих условий при успешном завершении программы на данных, удовлетворяющих входным условиям.

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

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

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

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

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

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

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

Выполняемая программа рассматривается как серия изменений состояний. Самое последнее состояние программы считается выходным состоянием и если оно получено, то программа считается правильной. Данный метод обеспечивает высокое качество исходного кода.

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

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

Процесс формального доказательства правильности программ методом математической индукции зарекомендовал себя как система правил статической проверки правильности программ за столом для обнаружения в них формальных ошибок. С помощью этого метода можно доказать истинность некоторого предположения $$Р(n)$$ в зависимости от параметра $$n$$ для всех $$n \ge n_{0}$$, и тем самым доказать случай $$Р(n_{0})$$. Исходя из истинности $$Р(n)$$ для любого значения $$n$$, доказывается $$Р(n+1)$$, что достаточно для доказательства истинности $$Р(n)$$ для всех $$n \ge n_{0}$$.

Путь доказательства следующий. Пусть даны описание некоторой правильной программы (ее логики) и утверждение $$A$$ относительно этой программы, которая при выполнении достигает некоторой определенной точки. Проходя через эту точку $$n$$ раз, можно получить справедливость утверждения $$А(n)$$, если индуктивно доказать, что:

$$А(1)$$ справедливо при первом проходе через заданную точку,

если $$А(n)$$ справедливо при $$n$$ проходах через заданную точку, то справедливо и $$А(n+1)$$ прохождение через заданную точку $$n+1$$ раз.

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

6.2.2. Доказательство конкретности с помощью утверждений

Рассмотрим формальное доказательство программы, заданной структурной логической схемой и совокупностью утверждений, задаваемых логическими операторами, комбинациями переменных (true/false), операциями (конъюнкция, дизъюнкция и др.) и кванторами всеобщности и существования (табл. 6.1).

Список логических операций

Логические операции
Название	Примеры	Значение
Конъюнкция	$$x \; \ \; y$$	$$x$$ и $$y$$
Дизъюнкция	$$x * y$$	$$x$$ или $$y$$
Отрицание	$$\neg x$$	не $$x$$
Импликация	$$x \to y$$	если $$x$$ то $$y$$
Эквивалентность	$$х = у$$	$$x$$ равнозначно $$y$$
Квантор всеобщности	$$\forall{х}\;Р(х)$$	для всех $$x$$, условие истинно
Квантор существования	$$\exists{х}\;Р(х)$$	существует $$x$$, для которого $$Р(х)$$ истина

Цель алгоритма программы - построение для массива целых чисел $$T$$ длины $$N (array Т[1:N])$$ эквивалентного массива $$Т^\prime$$ той же длины $$N$$, что и массив $$Т$$. Элементы в массиве $$Т^\prime$$ должны располагаться в порядке возрастания их значений. Данный алгоритм реализуется сортировкой элементов исходного массива $$Т$$ по их возрастанию. Доказательство правильности алгоритма сортировки элементов массива $$Т$$ проводится с использованием ряда утверждений относительно элементов этого алгоритма, которые описываются пунктами П1- П6.

Входное условие алгоритма задается в виде начального утверждения:$$А_{beg}: (Т [1:N]\text{ - массив целых}) \;\ \; (Т^\prime[1:N ]\text{ - массив целых })$$

Выходное утверждение $$А_{end}$$ - это конъюнкция таких условий:

$$(Т\text{ - массив целых}) (Т^\prime\text{ - массив целых})$$,

$$(\forall{i}\text{, если }i \le N\text{, то }\exists{j}(T^\prime(i) \le T^\prime(j)))$$,

$$(\forall{i}\text{, если }i \le N\text{, то }(T^\prime(i) \le T^\prime(i+1))$$,

т.е.$$А_{beg} \text{ - это }(Т [1:N]\text{ - массив целых}) \;\ \; (Т^\prime[1:N ]\text{ - массив целых }) \\ \ \; \forall{i}\text{, если }i \le N\text{, то }\exists{j}(T^\prime(i) \le T^\prime(j)),\\ \ \; \forall{i}\text{, если }i \le N\text{, то }(T^\prime(i) \le T^\prime(i+1)).$$

Расположение элементов массива $$T$$ в порядке возрастания их величин в массиве $$T$$ осуществляется алгоритмом пузырьковой сортировки, суть которого заключается в предварительном копировании массив $$T$$ в массив $$Т^\prime$$, а затем проводится сортировка элементов согласно условия их возрастания. Алгоритм сортировки представлен на блоксхеме (рис. 6.2).

Операторы алгоритма размещены в прямоугольниках, условия выбора альтернативных путей - параллелограммами, точки с начальным $$A_{beg}$$ и конечным $$A_{end}$$ условиями и состояниями алгоритма - кружками. В кружках также заданы: начальное состояние - $$0$$, состояние после обмена местами двух соседних элементов в массиве $$Т$$ - одна звездочка, состояние после обмена местами всех пар за один проход всего массива $$Т$$ - две звездочки.

Кроме уже известных переменных $$Т$$, $$Т^\prime$$ и $$N$$, в алгоритме использованы еще две переменные: $$i$$ - целое и $$М$$ - булева переменная, значением которой являются логические константы $$true$$ и $$false$$.

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

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

Так, оператор присваивания означает, что для всех $$i$$ ( $$i \le N i\ge0$$ ) выполняется ( $$T^\prime[i] : = T[i]$$ ). Результат выполнения алгоритма в точке с нулем может быть выражен утверждением

$$(T[1: N]\text{ - массив целых}) \;\\; (T^\prime[1: N]\text{ - массив целых})\\ \\; (\forall{i}\text{, если }i \le N (T[i] = T[i])).$$

Доказательство очевидно, поскольку за семантикой оператора присваивания (поэлементная пересылка чисел из $$Т$$ в $$T^\prime$$ ) сами элементы при этом не изменяются, к тому же в данной точке их порядокв $$Т$$ и $$T^\prime$$ одинаковый. Итак, получили, что выполняется условие б) исходного утверждения.

(рис 6.2) Схема сортировки элементов массива Т

Заметим, что первая строка доказанного утверждения совпадает с условием а) исходного утверждения $$А_{end}$$ и остается справедливой до конца работы алгоритма, поэтому в следующих утверждениях приводиться не будет.

В точке с одной звездочкой выполнен оператор $$(i < N )\; (T^\prime(i)) > T^\prime(i+1) \to (T^\prime(i)\text{ и }T^\prime(i+1) ,$$ который меняет местами элементы.

В результате работы оператора будет справедливым такое утверждение:

$$\exists{i}\text{, если }i<N\text{, то }(T^\prime(i) < T^\prime(i + 1),$$

которое является частью условия в) утверждения $$А_{end}$$ (для одной конкретной пары смежных элементов массива $$T^\prime$$ ). Очевидно также, что семантика оператора обмена местами не нарушает условие б) выходного утверждения $$А_{end}$$.

В точке с двумя звездочками выполнены все возможные обмены местами пар смежных элементов массива $$T^\prime$$ за один проход через $$T^\prime$$, т.е. оператор обмена работал один или больше раз. Однако пузырьковая сортировка не дает гарантии, что достигнуто упорядочение за один проход по массиву $$T^\prime$$, поскольку после очередного обмена индекс $$i$$ увеличивается на единицу независимо от того, как соотносится новый элемент $$T^\prime(i)$$ с элементом $$T^\prime(i-1)$$.

В этой точке также справедливо утверждение

$$\exists{i}\text{, если }i < N\text{, то }T^\prime(i) < T^\prime(i+1).$$

Часть алгоритма, обозначенная точкой с двумя звездочками, выполняется до тех пор, пока не будет упорядочен весь массив, т.е. не будет выполняться условие в) утверждения $$А_{еnd}$$ для всех элементов массива $$T^\prime: \foralli, если i < N, то T^\prime(i) < T^\prime(i+1)$$.

Итак, выполнение исходных условий обеспечено порядком и соответствующей cемантикой операторов преобразования массива.

Доказано, что выполнение алгоритма программы завершено успешно, что означает ее правильность.

Этот алгоритм можно представить в виде серии теорем, которые доказываются. Начиная с первого утверждения и переходя от одного преобразования к другому, определяется индуктивный путь вывода. Если одно утверждение - истинно, то истинно и другое. Иными словами, если дано первое утверждение $$А_{1}$$ и первая точка преобразования $$А_{2}$$, то первая теорема - $$А_{1} \to А_{2}.$$

Если $$А_{3}$$ - следующая точка преобразования, то второй теоремой будет $$А_{2} \to А_{3}$$.

Таким образом, формулируется общая теорема $$А_{i} \to А_{j}$$, где $$А_{i}$$ и $$А_{j}$$ - смежные точки преобразования. Эта теорема формулируетсятак, что если условие "истинное" в последней точке, то истинно и выходное утверждение $$А_{k} \to А_{end}$$.

Следовательно, можно возвратиться к точке преобразования $$А_{end}$$ и к предшествующей точке преобразования. Доказав, что $$А_{k} \to А_{end}$$ верно, значит, верно и $$А_{j} \to А_{j+1}$$ и так далее, пока не получим, что $$А_{1} \to А_{0}$$.

Далее специфицируются утверждения типа $$if$$ - $$then$$.

Чтобы доказать, что программа корректная, необходимо последовательно расположить все утверждения, начиная с $$А_{1}$$ и заканчивая $$А_{end}$$, этим подтверждает истинность входного и выходного условий.

Доказательство алгоритма программы завершено.

6.2.3. Валидация сценариев требований

Рассматривается подход к проверке требований, которые заданы в модели требований, построенной с использованием сценариев и акторов, как внешней сущности по отношению к разрабатываемой системе [6.21].

Сценарий после трансформации - это последовательность взаимодействий между одним или несколькими акторами и системой, в которой актор выполняет цели сценария при взаимодействии с ней. В модели требований сценарий задает несколько альтернативных событий, заданных на языке диаграмм UML. Они разделяются на функциональные (системные) и внутренние, определяющие поведение системы. На основе описания сценарных требования проводится их валидация.

Валидация требований - это процесс выявления ошибок в представлении сценарных требований, он итерационный и состоит из следующих шагов:

Формализованное описание требований в виде сценариев;

Создание исполняемой модели требований;

Создание специальных сценариев для валидации требований;

Применение валидационных сценариев к модели требований;

Оценивание результатов поведения модели требований;

Проверка условий завершения процесса валидации и при обнаружении каких-либо неточностей проводится повторение шагов, начиная с п. 2.

При выполнении сценариев возникают ошибочные ситуации, при которых поведение системы становится недетерминированным.В этих целях проводится контроль покрытия сценариев в модели требований валидационными сценариями в целях обнаружения рисков или ошибок. Создается модель ошибок, покрывающая модель требований системы и включающая типичные ошибки, используемые при выводе сценариев. Составная часть валидации требований в сценариях - определение классов эквивалентности входных и выходных данных, используемых и для синтеза сценариев.

Входная информация для синтеза сценариев - сценарная модель задается на языке взаимодействия и приведена на рис. 6.3.

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

Модель проверяется неполноту исходных требований или противоречия в требованиях с помощью тестов и модели ошибок.

(рис 6.3) Валидация сценариев требований к системе

Автоматический синтез основан на следующих процедурах:

валидация требований путем исполнения валидационных сценариев;

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

поиск ошибок в сценариях и проверка разных композиций сценариев.Синтез спецификаций сценариев, заданных диаграммами взаимодействия, может проводиться в среде системы Rational Rose.

6.2.4. Методы анализа структур программ

Методы анализа структуры программ относятся к доказательству правильности программ [6.20] и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, целостность, однозначность и непротиворечивость определений в программе. Сущность инспекции заключается в том, что эксперты пытаются взглянуть на программу "со стороны", подвергнуть ее всестороннему критическому анализу, рассмотреть словесные объяснения разработчиков о способах ее разработки. Цель инспекции - обнаружение ошибок в логике и в исходной программе в статике.

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

Метод простого структурного анализа ориентирован на анализ графовой структуры программы, в которой каждая вершина - оператор, а дуга - передача управления между операторами. На основе графа определяется достижимость вершин программы и существование выходов всех потоков управления для ее завершения.

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

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

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

Метод задается следующими шагами:

построение тестового набора данных для заданного пути в виде последовательности операторов символьного выполнения. В случае невозможности построения такого набора делается заключение о нереализуемости (противоречивости) данного пути;

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

Приведем шаги символьной проверки.

Шаг 1. Пусть $$Р(Х, Y)$$ - программа, выполняемая символически на наборах данных $$D = (d_{1}, d_{2}, \dots, d_{n})$$, где $$D \cup Х$$ и $$Х$$ - множество входных данных.

Пронумеруем операторы программы $$Р = \{P_{1}, P_{2}, \dots,P _{n}\}$$ и обозначим состояние выполнения программы в виде тройки

$$< N, pc, Z >,$$

где $$N$$ - номер текущего оператора программы $$P$$, $$pc$$ ( $$part condition$$ ) - условие выбора пути в программе (вначале $$true$$ ) в виде логического выражения над данными $$D$$ ; $$Z$$ - множество пар $$\{< z_{i} , e_{i} >| z_{i} \in X \cap Y$$, в которых $$z_{i}$$ - переменная программы, а $$e_{i} $$ - ее значение; $$Y$$ - множество промежуточных и выходных данных.

Семантика символьного выполнения задается базовыми конструкциями ЯП и правилами оперирования символьными значениями, как алгебраическими вычислениями. К базовым конструкциям относятся операторы присваивания, перехода и условные операторы.

В операторе присваивания $$Z = e(x,y)$$, $$x \in X$$, $$y \in Y$$ в выражение $$e(x,y)$$ подставляются символьные значения переменных $$x$$ и $$y$$, в результате чего получается выражение $$e(D)$$, которое становится значением переменной $$z (z \in Х \cup Y)$$. Вхождение в полученное выражение $$e(D)$$ переменных из $$Y$$ означает, что их значения, а также значение $$z$$ не определены.

Оператор перехода - это ссылка к помеченной меткой оператора программы.

Согласно условного оператора "если $$\alpha(x,y)$$ то $$В1$$ иначе $$В2$$ " вычисляется выражение $$\alpha(x,y)$$. Если оно определено и равно $$\alpha^\prime(D)$$, то формируются логические формулы:

$$рс \to \alpha^\prime(D),$$ $$рс \to \neg \alpha^\prime(D).$$

Если $$рс - false$$, то только одна из этих формул может быть выполнимой, а именно если

формула (6.1) выполнима, то управление передается на оператор $$В1$$ ;

формула (6.2) выполнима, то управление передается на оператор $$В2$$ ;

(6.1), (6.2) не выполнимы (т.е. из $$рс$$ не следует ни $$\alpha^\prime(D)$$, ни $$\neg \alpha^\prime(D)$$ ), тогда один набор данных, который удовлетворяет $$рс$$ и соответствует части "то" условного оператора и имеется набор данных, соответствующий оператору после "иначе" этого условного оператора.

Таким образом, создаются два пути символьного выполнения в соответствии с формулами: $$рс_1 = рс \cap \alpha^\prime(D)$$ и $$рс_2 = рс \cap; \alpha^\prime(D)$$. Получаем, что $$рс = true$$, тогда когда

для заданного пути формируется $$рс$$ исходя из семантики условного оператора, преобразующего $$рс$$ к виду (6.1) или (6.2);

решаются системы уравнений (6.1) и (6.2) и если решения нет, то это означает невыполнимость пути.

Шаг 2. Определение пути при заданных ограничениях на входные данные проводится так:

полагаем $$рс = \beta(D)$$, где $$\beta(D)$$ - входная спецификация, когда ее нет, то $$рс = true$$ ;

производим символьное выполнение операторов, если встречается ветвление, то запоминается состояние в данной точке или выбирается одна из ветвей; выполняется условный оператор, при котором формируется состояние программы с условием $$рс$$ ;

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

для промежуточных $$\delta(х, у)$$ выходной спецификации $$\gamma (х, у)$$ проводится доказательство выполнимости логических формул $$рс \Rightarrow \delta(х, у)$$ и $$рс \Rightarrow \gamma (х ,у)$$, где $$рс$$ - значение текущего условия в данной точке программы.

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

При проведении статического анализа программы используются различные инструменты, позволяющие определить ошибки в программе (например, неинициализированные или не использованные переменные). Кроме того, имеются способы автоматизации символьного выполнения программ и контроля в среде языковоориентированной разработки [6.23].

6.3. Верификация и валидация программ

Верификация и валидация - это методы анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы [6.19, 6.20].

Верификация помогает сделать заключение о корректности созданной программной системы после завершения ее разработки. Валидация позволяет установить выполнимость заданных требований путем их просмотра, инспекции и оценки результатов проектирования на этапах ЖЦ для подтверждения того, что проводится корректная реализация требований, соблюдение заданных условий и ограничений к системе. Верификация и валидация обеспечивают проверку полноты, непротиворечивости и однозначности спецификации и правильности выполнения функций системы в соответствии с требованиями.

Верификации и валидации подвергаются:

тесты, тестовые процедуры и входные наборы данных.

компоненты системы и их интерфейсы (программные, технические и информационные) и взаимодействия объектов (протоколы, сообщения) в распределенных средах;

описание доступа к БД, средства защиты от несанкционированного доступа к данным разных пользователей;

документация на систему.

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

6.3.1. Подходы к верификации моделей

Объектная модель и модель распределенного приложения отражают специфику предметной области и принципы взаимодействияобъектов со средой функционирования. Их верификации посвящен ряд работ, в том числе [6.22]. Эта область верификации требует дальнейшего развития и в рамках международного проекта на ближайшие десятилетия будет одним из главных ее направлений.

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

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

Проверенных объектов с помощью операций (функции), используемых в качестве теорем, а все операции, которые применяются над их подобъектами, не выводят их из множества состояний объектов.

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

Для доказательства правильности спецификации сообщения создается набор утверждений, доказывающий, что для любой пары элементов сообщения, например, $$А$$ и $$В$$, переход от $$А$$ к $$В$$ проходит за один шаг. Действие, выполняемое в промежутке между $$А$$ и $$В$$, приводит к $$В$$. При этом часть утвердждений проверяет входной параметр и его поступление на вход другого объекта в целях подтверждения его на выходе. Если доказано, что объект, инициированный сообщением, формирует правильный выходной результат - выходной параметр, то сообщение считается правильным.

Доказательство правильности построения ОМ для некоторой ПрО состоит в следующем:

вводятся дополнительные и/или удаляются лишние атрибуты объекта и его интерфейсов в ОМ, доказывается правильность объекта ОМ после изменений спецификации интерфейсов и взаимодействий с другими объектами;

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

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

Верификация модели распределенного приложения - это спецификация процессов SDL (Spesification Description Language), задание модели проверки (model-checking) и индуктивных утверждений. Метод предложен новосибирской школой программирования в [6.12, 6.13]. В нем проверки состоит в редукции системы с бесконечным числом состояний к системе с конечным числом состояний, а также в доказательстве распределенных приложений с помощью индуктивных рассуждений и системы переходов конечного автомата.

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

Основные типы данных спецификации в SDL - предопределенные и конструируемые типы данных (массив, последовательность и т.д.). Формулы описываются с помощью предикатов, булевых операций, кванторов, переменных и модальностей. Семантика их определения зависит от последовательных действий (поведений), спецификацией процесса и от момента времени их выполнения.

В предикатах используются локаторы управляющих состояний процессов, контроллеры заполнения каналов (пусто/заполнен канал), а также отношения между переменными и параметрами сигналов. Спецификация процесса состоит из заголовка, контекста, схемы и подспецификации. В заголовке указывается имя и вид процесса, формулы или предикаты.

Контекст - это описание типов, переменных и каналов. Переменная принадлежит процессу, если в ее описании указано место и имя процесса (через точку), которому эта переменная принадлежит. При ее использовании указывается имя переменной с расширением. Если указывается параметр, то в расширенное имя входит имя канала, сигнал и имена параметров, разделенных точками.

В логических условиях используются кванторы всеобщности и существования.

Схема спецификации процесса - это описание условий выполнения и диаграмм процессов. Она инициируется посылкой сообщения во входной канал, который передает сообщение внешней среде для выполнения.

Диаграмма процесса состоит из описаний переходов, состояний, набора операций процесса и перехода на следующее состояние. Набор операций - это действия типа: чтение сообщения из входного канала, запись его в выходной канал, очистка входного и выходного каналов, изменение значений переменных программы Рпроцесса.

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

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

отправка сообщения в канал;

получение сообщения из канала;

чистка входных и выходных каналов;

выполнение программ;

анализ непредвиденного события (взлом канала и др.).

Семантика выполнения процесса определяется в терминах событий и правил с помощью следующего типа утверждения:

любой процесс $$Рi \in P$$ вызывает событие при чтении или записи сообщения из/в канал, а также при выполнении процесса в узле распределенной системы.

6.3.2. Метод верификации композиции правильных компонентов

Метод верификации композиции компонентов базируется на спецификации функций и временных (temporal) свойствах готовых проверенных компонентов (типа reuse) [6.23]. Свойства составного компонента из компонентов повторного использования - reuse проверяются с помощью абстракции и общей компонентной модели (ОКМ). Эта модель состоит из совокупности проверенных компонентов, спецификаций их временных свойств и условий функционирования, которые проверяются с помощью аппарата асинхроннойпередачи сообщений (АПС). Его основу составляет модель проверки (Model Сhecking) [6.16, 6.23] временных свойств и обнаружения ошибок взаимодействия, возникающих при композиции компонентов.

Модель проверки включает в себя идентификацию правильных компонентов; композицию повторных компонентов по их спецификациям; формирование общей спецификации компонентной системы, составленной из правильных компонентов и др. При этом выполняются следующие условия:

спецификация компонентов задается в языке диалекта UML [6.23] и содержит описание временных свойств;

reuse-компоненты задают функции, спецификации интерфейса и временные свойства;

композиционный аппарат проверяет свойства составных компонентов.

Модель ОКМ - это совокупность специфицированных компонентов и их временных свойств для обеспечения верификации. Свойство компонента определяется исходя из условий среды. Когда компонент многократно используется в составе составного компонента эти свойства должны учитывать возможности среды и связей с другими компонентами композиции. ОКМ проверяется на модели вычислений АПС.

Представители ОКМ-модели могут быть примитивными и составными. Описание свойств примитивных элементов модели проверяется непосредственно с помощью модели проверки, а свойство составного компонента - на абстракции компонента, составленной из примитива и проверенных свойств в интегрированной среде.

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

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

Формально каждый компонент $$С$$ в ОКМ-модели задается в виде $$C = (E, I, V, P)$$, где $$E$$ - исходный код компонента; $$I$$ - интерфейс этого компонента с другими компонентами через передачу сообщений или вызовов процедур; $$V$$ - множество переменных, определенных в $$E$$ и связанных со свойствами множества временных свойств $$P$$, отражающими особенности среды компонента.

Каждое свойство - это пара $$(p, А(p))$$, проверяемая на множестве $$E$$, где $$p$$ - свойство компонента $$С$$ в $$Е$$, $$А(p)$$ - множество временных формул из свойств, определенных на множествах $$I$$ и $$V$$. Свойства компонента $$С$$ включается в абстракцию $$P$$ только тогда, когда оно проверено в среде этого компонента.

Композиция компонентов - это совокупность более простых компонентов: $$(E_{0}, I_{0}, V_{0}, P_{0}), \dots, (E_{n - i} , I_{n - i} , V_{n - i}, P_{n - i})$$, определенных на модели компонента $$С$$ следующим образом. $$E$$ создается из множества представлений $$E_{0}, E _{1}, \dots, E_{n - 1}$$, связанных между собой интерфейсами из набора интерфейсов $$I = \{I_{0}, \dots, I_{n - 1}\}$$, операций связи $$Ih (0 < h < n)$$ для взаимодействия с другими компонентами;

$$P$$ - множество временных свойств, определенных на $$I$$ и $$V$$, и проверенных на компонентах $$E$$ с использованием отдельных свойств $$Р_{0} , \dots, P_{n - 1}$$ ;

$$V$$ - подмножество $$\bigcup_{i=0}^{n-1}{V_i},$$ где $$V_{i}$$ - ссылка на свойство $$i$$ -компонента из $$С$$, заданное в $$Р$$.

Модель вычислений АПС - это вычислительная модель системы, заданная на конечном множестве взаимодействующих процессов представленных кортежами:

$$Р = (Х, \sum, Q, \nabla),$$

где $$X$$ - множество переменных с типом; $$\sum$$ - расширенная модель состояния; $$Q$$ - очередь сообщений в порядке их поступления; $$\nabla$$ - множество начальных значений для каждой переменной из $$X$$, $$E$$ и пустое для $$Q$$.

При выполнении в вычислительной среде создается модель состояния в виде кортежа $$(Ф, М, T)$$, где $$Ф$$ - множество состояний, каждое из которых связано с ассоциативным действием; $$М$$ - множество типов сообщений; $$T$$ - набор переходов, определенных на множествах $$Ф$$ и $$М$$

Каждое из состояний переходов - кортеж $$(r, t, m)$$, где $$r$$ и $$t$$ - состояния в $$Ф$$ и $$m$$ - тип сообщения во множестве сообщений $$М$$.

Семантически каждое действие определяется сегментом программы, составленным из операторов: пустой оператор, присваивания, передачи сообщений, условный и составной операторы и др.

Асинхронная передача сообщений АПС вызывает чередование переходов состояний и действий процессов. Для двух процессов $$Р_{1}$$ и $$Р_{2}$$ передача сообщения от $$Р_{1}$$ к $$Р_{2}$$ включает в себя: тип сообщения $$m$$ из множества $$М$$ для $$Р_{2}$$ и соответствующие параметры. Когда оператор действия выполняется, сообщение $$m$$ с параметрами ставится вочередь к процессу $$Р_{2}$$. Более подробные сведения о верификации компонентов приведены в [6.23].

6.3.3. Перспективные направления верификации программ

По данным, опубликованным в [6.15], ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным методам и спецификациям программ приняли решение поставить теоретические достижения в этой области на производственную основу [6.16]. Этому решению предшествовали результаты исследований по формальной верификации моделей ПрО и обращений к функциям на языке API проекта SDV фирмы Microsoft, а также проверка безопасности и целостности БД и др. Кроме того, начали активно применяться формальные языки спецификации (RAISE, Z, VDM и др.) для разработки приложений. В 2005 г. был сформулирован международный проект по формальной верификации ПО.

Идея создания этого проекта принадлежит Т.Хоару, она обсуждалась на симпозиуме по верифицированному ПО в феврале 2005 г. в Калифорнии. Затем в октябре того же года на конференции IFIP в Цюрихе был принят международный проект сроком на 15 лет по разработке "целостного автоматизированного набора инструментов для проверки корректности ПС".

В нем сформулированы следующие основные задачи:

разработка единой теории построения и анализа программ;

построение всеобъемлющего интегрированного набора инструментов верификации для всех производственных этапов, включая разработку спецификаций и их проверку, генерацию тестовых примеров, уточнение, анализ и верификацию программ;

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

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

В связи с тем, что комитет ISO/IEC в рамках стандарта ISO/IEC 12207:2002 провел стандартизацию процессов верификации и валидации ПО и, учитывая цель проекта, проблема создания автоматизированного набора инструментов и репозитария для проверки корректности разных объектов программирования является перспективной.

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

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

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

разработка стандартных форм для задания и обмена формальными спецификациями разных объектов, инструментов и готовых систем;

разработка механизмов интероперабельности и взаимодействия для переноса готовых верифицированных продуктов из репозитария в новые распределенные и сетевые среды для использования в новых ПС.

Данный проект предполагается развивать в течение 50 лет. Известно, что более ранние проекты ставили подобные цели: улучшение качества ПО, формализация моделей сервисных услуг, снижение сложности за счет использования ПИК, создание отладочного инструментария для визуальной диагностики ошибок и их устранения и др. Однако эти направления еще не получили должной реализации и предполагаемого коренного изменения в программировании пока не произошло.

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

Контрольные вопросы и задания

Дайте определение формальной спецификации.

Назовите категории классификации спецификаций.

Определите основные понятия формальной спецификации VDM.

Определите основные базовые элементы спецификации RAISE.

Сравните математические понятия методов VDM и RAISE.

Определите цель и структуру концепторного языка.

Назовите формальные методы доказательства и приведите. их короткую аннотацию.

Определите понятия пред- и постусловий, аксиом и утверждений.

Опишите, как проходит процесс доказательства программы, заданной спецификацией.

В чем проблемы проведения доказательства программ с по мощью формальных методов?

Приведите отличие техники формального доказательства от символьного выполнения программ?

Дайте определение верификации и валидации.

В чем суть композиции верифицированных программ?

Расскажите о международном проекте по верификации.