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

Верификация – процесс док-ва того, что в рез-те исполнения прог-ммы

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

решения м.б. вычислены этой программой.

Спецификация – программы S явл. любое множество опред-ий, которое

точно задает содержимое каждого из отнош-ий, встреч-ся в программе,

и, в частности, отношения в G. Это отношение будем называть осн.

специфицир-м отношением и обозначать как R.

Частичная правильность – программа (P,G) частично правильна тогда

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

 1)для все Q, если tQÎR, то tQÎR*;

 2)R явл. подмнож-м интервала G относительно S;

 3)для всех Q, если P=R(tQ),то S=R*(tQ).

Полнота – программа (P,G) явл. полной относит. специфик-ии S тогда и

только тогда, когда всякое специфиц. решение tQ явл. также и вычисл.

решением, т.е. выполняется одно из след-х условий:

1)для всех Q, если tQÎR*, то t tQÎR;

2)интервал G относительно S явл. подмнож. R;

3)для всех tQ, если S=R*(tQ), то P=R*(tQ).

Полная прав. программы – программа (P,G) явл. полностью прав-ой относительно специфик-ии S тогда и только тогда, когда она явл-ся и частично правильной и полной, т.е. выполн-ся одно из след-х условий:

1)для всех Q tQÎR тогда и только тогда, когда tQÎR*;

2)R равно интервалу G относительно S;

3)для всех Q P=R*(tQ) тогда и только тогда, когда S=R*(tQ).

Если S=P, то программа (P,G) частично правильна относит S.

Если множ-во опред-й P полно относит. S, то P явл. G-полным относ S.

Если S=P и множ-во опред-й P явл. полным, то программа (P,G) полностью правильна относительно S.

Разрешимость – программа явл. разрешимой, если с ее помощью выч.

по крайней мере, одно решение.