3. Средства описания действий

Средства описания действий - та часть языков программирования, которая непосредственно используется для выражения алгоритмов. Они послужили первоначальным толчком к созданию языков.

На развитие средств описания действий большое влияние оказали языки Фортран, Алгол-60, Паскаль, Ада.

3.1. Определение семантики средств описания действий

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

- проведение декомпозиции общей задачи на точно определенные подзадачи и доказательство того, что если каждая подзадача решена корректно и полученные решения связаны друг с другом определенным образом, то задача будет решена корректно;

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

Чтобы доказать корректность программы, необходимо формально описать семантику операторов языка. Введем ряд понятий, которые потребуются для описания семантики операторов.

Каждая программа имеет статическую и динамическую структуры.

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

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

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

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

Фундаментальное свойство всех описываемых здесь способов композиции заключается в том, что они позволяют объединить в один составной оператор с одним входом и одним выходом один или более операторов также с одним входом и одним выходом и не позволяют строить операторы с несколькими входами или выходами. Именно это свойство дает возможность в достаточно простой форме описывать действия любого оператора или программы. Пусть S - какой-нибудь оператор или программа, Р и Q - предикаты, описывающие состояние вычислений. Тогда семантика S описывается следующим образом:

{P} S {Q}

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

(например, falsе), который будет предусловием S, если Q - постусловие­S. И, наконец, для любых Р и Q всегда найдется программа S (например, while true do; end do;), для которой Р будет предусловием, а Q - постусловием. Задача программиста найти такую программу S, которая завершается и для которой Р является предусловием, а Q - постусловием.

Если S - программа, корректность которой мы хотим установить, то соотношение {P} S {Q} - это то, что мы должны доказать, где Р - условие, которому должны удовлетворять начальные значения переменных, а Q - условие, которому должны удовлетворять конечные значения переменных.

Соотношение {P} S {Q} определяет только частичную корректность S. Программа, в которой гарантируется получение требуемого результата при условии ее завершения,   частично корректна.

Если дополнительно можно показать, что программа завершается при всех исходных данных, удовлетворяющих Р, то программа   полностью корректна. Чтобы доказать завершимость программы, необходим анализ циклов.

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

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

- определение на каждом этапе декомпозиции спецификаций {Pi}­Si­{Qi} для компонент Si, программы;

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

При записи предикатов Р и Q могут быть использованы следующие средства:

1. Имена переменных, арифметические операции, операции сравнения.

2. Математические символы и функции.

3. Логические операции: конъюнкция (and или &), дизъюнкция (оr или v), отрицание (not или ┐), импликация (=>), эквивалентность (=).

4. Кванторы всеобщности ((), существования (() и количества (N).

5. Подстановки.

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

Н1, Н2,......,Hn

───────────────

Н

Если Н1, Н2,......,Hn - истинные утверждения, то Н - также истинное утверждение. Если входных условий нет (т.е. n=О), то правило вывода будем записывать просто в виде

Н

Два простейших правила вывода имеют вид

 

{P} S {Q} , R=>Q P=>R , {R} S {Q}

 ──────────────── и ────────────────

{P} S {Q} {P} S {Q}

 

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

─────────

П р и м е р 3.2. Предположим, что переменные Х, Y, r, q определены на множестве неотрицательных целых чисел. Рассмотрим утверждения

(Х=Y*q+r) & (О<=r<Y) => (Х=Y*(1+q)+(r-Y)),

{X=Y*(1+q)+(r-Y)} r:=r-Y; {Х=Y*(1+q)+r}.

В предусловии Р спецификации (Р) r:=r-Y; {Q} используется старое значение r, а в постусловии Q - новое значение r, которое меньше старого на текущее значение Y. В предположении истинности обеих посылок, получаем, что

{(Х=Y*q+r)&(О<=r<Y)} r:=r-Y; {Х=Y*(1+q)+r}

─────────

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

{Р} S {true} и {false} S {Q}

для любых Р, Q, S. Эти правила называют   правилами тавтологии 0.

Теперь докажем   правила замены 0:

 ш1

Р=>{R} S {Q} {P&R} S {Q}

──────────── и ─────────────

{P&R} S {Q} P=>{R} S {Q}

 ш0

Для доказательства правил достаточно рассмотреть два случая:

Р=true:

(Р =>{R} S {Q}) = ({R} S {Q})=({P & R} S {Q}),

P=false:

(P=>{R} S {Q})=true=({false} S {Q})=({P & R} S {Q})