Спецификация программ

Спецификация программ

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

В спецификации может быть указан размер программы.

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

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

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

                     {Q} S {R},

где  Q – предусловие, S –программа, R – постусловие  .

Если выполнение S началось в состоянии, удовлетворяющем Q, то имеется гарантия, что оно завершится в конечное время в состоянии удовлетворяющем R.

Рекомендуемые материалы

Пример спецификаций:

            Записать в z произведение a и b, предполагая, что a и b больше либо равны нулю.

            z:=a*b

{a ³ 0 Ù b ³ 0} S {z = a * b}  

Понять {z=a*b}  можно и  так: программа не должна делать ничего кроме того, что должна делать.

Пример2:  сспецификация на сортировку

Даны n >= 0 и массив  b[0:n-1].

Менять можно только по два элемента.

a). R: ("I: 0£i<n-1: b[i]£b[i+1])

b). {n ³ 0 and b = B} S { "i: 0 £ i < n-1: b[i] £ b[i+1] and b = перем.(B) }

где b является перемещением от B.

Пример3: обмен значениями переменных.

{x = X Ù y = Y} S {x = Y Ù y = X}

Пример4: найти максимальное значение переменных в массиве B, который изменяется от 0 до n-1:

{n>0} S {("i: 0 £ i <n: b[i] £ x) Ù ($ i: : 0 £ i < n: x = b[i])}

Пример5: придать x абсолютное значение x.

{x = X} S {(X £ 0 Ù x = -X ) Ú (X ³ 0 Ù x = X)}

Рекомендуем посмотреть лекцию "II. Чрезвычайные ситуации техногенного характера".

                                или

{(x ³ 0) Ù ( x = X Ú  x = -X)}

Пример6: придать каждому значению массива b[0:n-1] значение суммы элементов этого массива.

{n > 0 Ù b = B} S { "i:0£i<n:b[i] = åj:0£j<n:B[j]}

Пример7: в массиве  a[0:n-1] отсортирован список преподавателей Политеха, в b[0:m-1] отсортирован список, получающих пособие по безработице. Найти первого “жулика”, который преподает и получает пособие.

{n>0 Ù m>0} S {0£p<n Ù 0£q<m Ù a[p]=b[q] Ù (i,j:0£i£p Ù 0£j£q:a[i]=b[j]) = 1}