Учебное пособие по дисциплине Разработка языков программирования высокого уровня

• Название: Учебное пособие по дисциплине Разработка языков программирования высокого уровня
• Дата: 05.03.2023
• Размер: 1.74 Mb.
• Имя файла: Lektsii_YaPVU_Lukinova_2_semestr.docx
• Тип: Учебное пособие; #970477
• страница: 20 из 20

7.4.5. Операторы цикла

Рассмотрим цикл типа пересчета

For x = 1 to 10 do s(x) end.

Здесь счетчик цикла х всегда перечислимого типа, изменяется от хmin до хmax, т.е. число итераций всегда известно и тело такого цикла можно рассматривать как последовательность операторов s(xmin ), …. , s(xmax ), т.е. предусловия и постусловия можно рассматривать как для группы операторов. Тогда правильный вывод можно записать в виде

{(хmin <= x <= xmax) and {P([xmin-1 , …. , x])} s(x) {P([x, …. , xmax])}

{P([xmin-1 … xmax])} for x=xmin to xmax do s(x) end {P([xmin … xmax])}

Далее рассмотрим цикл с условием типа

While B do S end.

Аксиоматическое описание этого цикла

{ P } while B do S end; {Q}.

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

Пусть существует предикат I такой, что { I and B } S { I }. Тогда этот предикат I называется инвариантом цикла.
Итак, инвариант должен удовлетворять следующим условиям:

- из слабейшего предусловия должна следовать истинность инварианта,

- из истинности инварианта должна следовать должна следовать истинность предусловия после завершения цикла,

- во время выполнения цикла результаты вычисления логического условия B и тело цикла не должны влиять на истинность инварианта. Тогда полное аксиоматическое описание цикла можно представить как

1. P => I

2. { I } B { I }

3. { I and B } S { I }

4. ( I and (not B)) => Q

5. завершение цикла.

Таким образом, для доказательства корректности цикла (нахождения слабейшего предусловия) необходимо найти инвариант, обеспечивающий истинность этих условий 1-5. Тогда правило вывода для вычисления предусловия цикла while следующее:

{ I and B } S { I}

{ I } while A do S end , { I and not B }

Пример 7.

Доказать корректность следующего цикла:

While y <> x do y = y + 1 end { y = x }.

Чтобы обнаружить инвариант I, используем постусловие цикла Q для вычисления предусловий нескольких повторений тела, начав с нуля повторений. Здесь тело состоит из оператора присваивания, поэтому используем аксиому присваивания. Введем функцию wp(оператор, постусловие) =предусловие.

0-ое повторение: слабейшее предусловие очевидно

{ y = x }

1-ое повторение:

wp(y = y + 1, {y = x} ) = { y + 1 = x } = { y = x – 1 }

2-ое повторение:

wp(y = y + 1, {y = y – 1} ) = {y + 1 = x – 1 } = { y = x – 2 }

3-е повторение:

wp(y = y + 1, {y = x – 2 } ) = {y + 1 = x – 2 } = { y = x – 3}

Далее, на основании индуктивных соображений, можно записать общее условие

{ y <= x },

которое будем использовать в качестве инварианта I. Кроме того, в качестве предусловия P возьмем P = I.

Докажем, что выбранный инвариант удовлетворяет вышеуказанным 5-ти условиям:

1. 
   Поскольку P = I, то P => I.
   
2. 
   { I } B {I }, т.е. на инвариант не влияет на вычисление условия цикла В. В примере В есть y <> x.. Здесь значения переменных х, у не изменяются, т.е. на инвариант влияния не оказывается.
   
3. 
   { I and B } S { I } , т.е. на инвариант не влияет вычисление тела цикла. В нашем примере имеем { y <= x and y <> x } y = y + 1 { y <= x }. Применим к последнему выражению аксиому присваивания y = y + 1 { y <= x }. Тогда получим условие { y + 1 <= x }, что эквивалентно условию { y < x }. Таким образом 3-е утверждение доказано.
   
4. 
   ( I and (not B)) => Q. В нашем случае имеем
   

{ ( y <= x ) and ( not ( y <> x )) } => { y = x }

{ ( y <= x ) and ( y = x ) } => { y = x }

{ ( y = x ) } => { y = x }

5. 
   Завершение цикла. Рассмотрим, завершается ли цикл в нашем примере
   

{ y <= x } while y <> x do y = y + 1 end { y = x }

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

Итак, наш выбор условия I удовлетворяет 5-ти критериям, следовательно оно может быть инвариантом и предусловием цикла.

Пример 8.

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

While s > 1 do s = s/2 end {s = 1}.

Найдем инвариант для данной конструкции:

0: { s = 1 }

1: wp ( s = s/2, { s = 1 } ) = { s/2 = 1 } = { s = 2 }

2: wp ( s = s/2, { s = 2 } ) = { s/2 = 2 } = { s = 4 }

3: wp ( s = s/2, { s = 4 } ) = { s/2 = 4 } = { s = 8 }

т.е. в качестве инварианта здесь служит { s – положительная степень двойки }.

Однако это условие не является слабейшим предусловием, потому что видно, что в качестве предусловия можно взять { s > 0 }. Это условие значительно шире, чем степень двойки.

Найти инварианты не всегда легко. Для этого следует понять их природу.

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

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

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

Контрольные вопросы:

1. 
   В чем заключается смысл и назначение аксиоматической семантики Хоара?
   
2. 
   Как формулируется основная теорема аксиоматической семантики?
   
3. 
   Какую программу можно считать завершённой?
   
4. 
   Какая программа называется частично корректной?
   
5. 
   Какая программа называется полностью корректной?
   
6. 
   Какие существуют схемы доказательства корректности программ в семантике Хоара?
   
7. 
   В чем заключается аксиома присваивания?
   
8. 
   Сформулировать правила консеквенции, логического следствия, замены.
   
9. 
   Привести примеры доказательства корректности оператора присваивания.