Информатика и компьютерные науки (стр. 8 из 14)

Рис. 1. Алгоритм для нахождения q и r-, удовлетворяющих условиям x=q*y+r и 0 <= г < y. Таким образом, на выходе q = х div y и r=х mod y.

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

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

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

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

Рассмотрим рис. 1, который воспроизводит алгоритм для определения х div у и х mod у. Заметим, что состояние вычислений, связанное с точкой входа, определяется значениями входных переменных х и у; но после выполнения первых двух операторов состояние вычислений расширяется, включая значения четырех переменных: х, у, q и г. (Значения х и у могут быть различными

в зависимости от применения алгоритма, но остаются постоянными в течение одного применения). Ясно, что следующая за проверкой r >= у передача управления будет зависеть от текущего состояния вычислений.

Фундаментальное свойство всех видов композиции, которые мы будем рассматривать, заключается в том, что они дают возможность объединить в одну сложную структурную схему с одним входом и одним выходом одну или более схем также с одним входом и одним выходом. Как показано на рис. 1, наша процедура проектирования объединяет с этими точками некоторые соотношения, которые описывают существенные аспекты состояний вычислений в этих точках. Каждая такая структурная схема имеет вид, приведенный на рис. 2А, где S может быть отдельным действием ЭВМ или сложной схемой. Чтобы выразить ее в более краткой форме, используем нотацию:

{Р} S {Q}. (1)

Это - спецификация программы со следующим смыслом: если соотношение Р истинно перед выполнением S, то Q будет истинно после завершения выполнения S. Другими словами, если Р истинно при входе, то Q будет истинно при выходе.

Если S — программа, чью корректность мы хотим установить, то нотация (1) в том смысле, как мы ее определили, — это то, что мы хотим доказать, причем Р — соотношение, которому должны удовлетворять начальные значения переменных, а Q — соотношение, которому должны удовлетворять конечные значения переменных. Например, если S - алгоритм, изображенный на рис. 1, то соотношение, которое мы хотим доказать, таково:

{(х >= 0)^(y > 0)} S {(х = q *у + r)^(0<= r < у)}, (2)

где знак ^ используется в качестве формальной нотации для "и".

Как уже отмечалось, соотношение {Р} S {Q} означает, что если P истинно перед выполнением S, то Q должно быть истинно при завершении S. Это означает, что {Р} S {Q} тождественно истинно, если S не завершается, т. е. если на рис. 2А точка выхода никогда не достигается. Другими словами, (1) определяет только частичную корректность S. Частично корректной является такая программа, в которой гарантируется получение требуемого результата при условии ее завершения. Но завершается ли программа действительно для некоторых исходных значений — это другой вопрос. Если дополнительно можно показать, что программа завершается для всех исходных значений, удовлетворяющих соотношению Р, то говорим, что программа полностью корректна. Чтобы доказать завершение программы, получаемой применением правил композиции, введенных ранее, необходим анализ циклов, т.е. операторов итерации.

Можно подвести итог нашему подходу к проектированию программ.

1. Проектирование должно начинаться со спецификации {Р} S {Q}, которой должна удовлетворять проектируемая нами программа. Мы начинаем, таким образом, .с ясного и недвусмысленного определения того, когда программа должна использоваться (предусловие Р), и результата ее использования при этом (постусловие Q).

2. Процесс проектирования сверху вниз определяет спецификации [Рi} Si {Qi} для компонентов Si, из которых строится программа.

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

2.3. ПРАВИЛА ВЫВОДА ДЛЯ ПРОСТЫХ ОПЕРАТОРОВ

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

Н1,…,Hn (,2.26)

H

Если H1, . . . , Hn, - истинные утверждения, то Н - также истинное утверждение.

Два простейших правила вывода формулируются в (2.27) и (2.30). Первое утверждает, что если выполнение программы S обеспечивает истинность утверждения R, то оно также обеспечивает истинность каждого утверждения, которое следует из R, т. е.

[P}S{R}, R ® Q

{P}S{Q}

Например, из

{(х > 0)^(у > 0)} S{(z+u *у = х *у)^(и = 0)}, (2.28)

(z+u*y=x*y)^(u=0)®(z=x*y) (2.29)

заключаем, используя (2.27), что {(х > 0) ^ (у > Q)} S {z = х * у].

Второе правило утверждает, что если R - известное предусловие программы S, приводящей к результату Q после завершения своего выполнения, то это же относится к любому другому утверждению, из которого следует R:

P®R, [R}S{Q}

{P}S{Q}

Правила (2.27) и (2.30) называются правилами консеквенции.

Теперь обратимся к специфическому виду, который принимает {Р} S {Q}, если что-то известно о S. Будем изучать действие структурных операторов в последующих разделах. Здесь рассмотрим случай, когда S - простой оператор. Простейшей формой простого оператора является пустой оператор — тот, который не оказывает никакого воздействия на значения программных переменных. Для любого Р имеем правило вывода

{Р}{Р}. (2.32)

Из простых операзйэров, оказывающих влияние на значения программных переменных и, следовательно, на Булевы значения утверждений Р и Q в [Р) S {Q}, ранее введено только присваивание. Итак, пусть х:=е есть оператор присваивания, который устанавливает х равным значению выражения е. Тогда можем сделать вывод, что для любого Р

{PXe}x:=e{P}. (2.33)

Здесь утверждается, что если Р истинно для подстановки е вместо х перед выполнением присваивания, то Р должно быть истинным, когда переменной х присвоили ее новое значение. Это правило лучше пояснить примерами, данными на рис. 2Б.

2.4. СОСТАВНЫЕ И УСЛОВНЫЕ ОПЕРАТОРЫ

Предположим, мы хотим доказать, что имеет место {Р} S {Q}, когда S является структурным оператором. Нам необходимо правило для каждого типа композиции операторов, которое позволит вывести свойства сложного (структурного) оператора на основе установленных свойств его компонент. В этом разделе обсуждаются такие правила для составных и условных операторов.

Составные операторы.

Простейшей формой структурирования является создание так называемых составных операторов путем последовательной композиции, состо-

ящей из действия S1, за которым следует действие S2. Можно обобщить это определение последовательной композиции на случай произвольного конечного числа действий S1, S2, . . . Sn. В языке Паскаль последовательно соединенные операторы обычно заключают в скобки begin и end, которые указывают, что полученный таким образом оператор является единым, хотя и структурным. Такой оператор имеет вид begin S1;S2,.. . Sn end (2.34)

и называется составным оператором. Он может быть представлен структурной схемой (рис. 2В).

Правило вывода для последовательной композиции гласит, что если S есть begin S1; S2 end и если имеют место {Р} S1 {R} и {R}S2{Q}, то истинно и {Р} begin S1 ;S2 end {Q}. Формально это правило может быть выражено следующим образом:

{Р} S, [R], {R} S, {Q}

{Р}begin Si;S, end {Q} (2-36)

Правило вывода (2.36) обобщается следующим очевидным образом:

{Рi-1}S1{Pi} дпя i=1,....n

{P0} begin S1;. ..Sn. end {Pn}

Условные операторы.

Если S1 и S2 - операторы, а В — Булево выражение (т.е. выражение, имеющее значение Булевого типа), то

if В then S1 else S2 (2.38)

есть оператор, обозначающий следующее действие: вычисляется В; если его значение есть истина, то должно быть выполнено действие, описываемое S1, в противном случае — действие, описываемое S2 Выражение (2.38) может быть графически представлено структурной схемой (рис. 2Г).

Выработаем правило вывода для условного оператора (2.38). Если требуется установить истинность [Р] if В then S1 else S2 {Q},то необходимо доказать два утверждения.

1. Если В истинно, то выполняется S1. Так как Р справедливо перед выполнением (2.38), то делаем вывод, что в этом случае "Р^В также справедливо перед выполнением S1. Если Q справедливо после выполнения (2.38), то должно быть справедливо и [Р ^ В} S1 {Q}. Итак, мы должны доказать {Р^В} S1 {Q}.

2. Если В ложно, то будет выполняться S2. Так как Р было истинно перед выполнением (2.38), делаем вывод, что Р ^ ~В справедливо перед выполнением S2. С этим утверждением в качестве предусловия S2 требуется доказать, что после выполнения S2 будет справедливо Q, т.е. доказать [p^~b}s2{q].

Если мы доказали как [Р^В] S1 {Q}, так и{Р^ ~В} S2 {Q}, то можно утверждать, что если Р справедливо перед выполнением (2.38), то Q будет справедливо по окончании его выполнения независимо от того, какой оператор (S1 или S2) был выбран для выполнения. Итак, можно сформулировать следующее правило вывода: