Информатика и выч. техника \ Информатика

Программа как математический объект: Методические указания для самостоятельного изучения темы и выполнения РГР, страница 19

                        P

            C ( X, Y )

   proof  ( доказать)    

последовательность: g; h

 Y = h ° g (X)

f=[g;h] доказать f=h°g

for_do:for I ÎL(1:n) do g                 od

Y = gL(n)° . . . ° gL(1) (X)

f= gL(n)° . . . ° gL(1) (X)

if _ then: if p then g fi

(p(X)®Y = g(X)) L

 (Øp(X) ®Y = X)

iftest true (p®f)=(p®g)

iftest false (Øp®f)=(Øp®I)

if _ then _else: if p then g  else h fi

(p(X)®Y = g(X)) L

 (Øp(X) ®Y = h(X))

iftest true (p®f)=(p®g)

 iftest false (Øp®f)=(Øp®h)

case : case p part(CL1) g . . .

part(CLn) h else t esac

(p(X)ÎCL1 ®Y = g(X)) L

(p(X)ÎCLn ®Y = h(X)) L

(p(X) ÏCL1, ..., CLn ) ®

Y = t(X))

part 1

(pÎCL1 ®f)=(pÎCL1 ®g)

part n

(pÎCLn ®f)=(pÎCLn ®h)

else_case

(p ÏCL1, ..., CLn ) ®f

(pÏCL1, ..., CLn ) ® t

while _do: while p do  g od

(p(X)®Y = f ° g(X)) L (Øp(X) ®Y = X)

while_test true

(p®f) = (p®f°g)

while_test false

(Øp®f)= (Øp®I)

do _until: do  g until p od

(p°g(X) ®Y = g(X))

L(Øp ° g(X) ®Y = f °g(X))

until _test true

(p°g ®f)=( p°g ®g)

until _test false

(Øp°g ®f)=(Ø p°g ®f°g)

 do _while _do: do  g while p do  h od

(p ° g(X)®Y =f ° h ° g(X)) L(Øp ° g(X) ®Y = g(X))

while_test true

(p°g ®f) = (p°g ®f°h° g)

while_test false

(Øp°g ®f) = (Øp°g®g)

Отметим, что теорема правильности констатирует отношения между тремя объектами:  функцией f, программой P и условием C, рассматриваемыми с упорядоченными  парами (X , Y). Для того чтобы представить эти отношения более чётко, сформулируем вопросы правильности в другой форме:

1) полная правильность

                                   (X, Y) Î f « (X, Y) Î[P]

2) достаточная правильность

                                (X, Y) Î f ® (X, Y) Î[P]

4.3.4.  Синтаксис, используемый при доказательстве правильности

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

function

формулировка заданной функции или ссылка на неё

program

формулировка программной части или ссылка на неё

proof

формулировка доказательства или ссылка на неё

result    pass или fail, suff или comp

Формы раздела proofдля каждой элементарной программы приведены в таблице теоремы правильности.

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

4.4.1.  Трассировочные таблицы

Для доказательства того, что последовательная программа G;H правильно выполняет функцию f, необходимо верифицировать следующие отношения:

                                      f = [G, H ] и f Ì [G, H]

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

Фрагмент

        x

        y

1. x:= x + y

x1 = x0 + y0

 y1 = y0

2. y:= x - y

x2 = x1

y2 = x1 - y1

3. x:= x - y

x3= x2 - y2

y3 = y2
Скачать файл