2020-04-07
331
Аксиоматическая семантика не даёт непосредственного представления об исполнении программы, но тем не менее связана со смыслом программы, поскольку позволяет отвечать на вопросы о том, что делает программа. Например, для цикла, используемого нами в качестве примера,
while (n > 0)
{
if (n%2)
y = y*x;
x = x*x;
n = n / 2;
}
можно задать следующий вопрос: "Правда ли, что если перед циклом значение x, n и y были равны, соответственно, X, N и 1, и N неотрицательно, то после цикла n будет равно 0, а y = XN?"
Аксиоматическая семантика строится на понятии предусловия и постусловия, а утверждения формулируются в виде троек
{ P } S { Q }
где P - предусловие, S - синтаксическая конструкция, Q - постусловие.
Для доказательства утверждений аксиоматическая семантика задаёт систему аксиом и правил вывода, сводя таким образом задачу к использованию математической логики. Система правил всегда включает в себя правило следствия - замены предусловия более сильным, а постусловия - более слабым:
| P ⇒ P ', Q ' ⇒ Q, { P } S { Q } |
| { P '} S { Q '} |
Продемонстрируем определение аксиоматической семантики на примере нашего простого языка. Будем считать, что смысл выражений в языке очевиден и, более того, мы можем использовать эти выражения при записи утверждений. Каждый оператор присваивания привносит в систему новую аксиому:
|
|
|
{ P [ var → expr ]} (присв получатель: var источник: expr) { P }
где запись P [ var → expr ] означает утверждение P, в котором все вхождения var заменены на expr. Например, пусть P = x>0, тогда для присваивания x=x+1 мы получим
{(x > 0) [x→x+1]} x=x+1 {x>0},
что эквивалентно
{x+1 > 0} x=x+1 {x>0}
и
{x > -1} x=x+1 {x>0}.
Ещё одна аксиома имеется для пустой последовательности операторов
{ P } {} { P },
которая означает, что любое условие сохраняется в результате её выполнения.
В остальных случаях синтаксические конструкции задают не аксиомы, а правила вывода. Для последовательности, состоящей из первого оператора S и остальной части “...”:
| { P } S { R }, { R } {...}{ Q } |
| { P } { S,...}{ Q } |
Для условного оператора:
| { P ˄ E } S 1 { Q }, { P ˄ E } { S 2}{ Q } |
| { P } (if условие: E то: S 1 иначе: S 2) {Q} |
Для цикла:
| { P ˄ E } S { P } |
| { P } (while условие: E тело: S) { P ˄ E } |
Наибольшую сложность вызывает правило для цикла, поскольку в нём, в отличие от остальных случаев, одно и то же условие P появляется как в левой, так и в правой части. По-существу, необходимо отыскать инвариант цикла, то есть такое условие, которое не меняется в результате выполнения тела цикла, если до его выполнения было справедливо также условие цикла. В общем случае это алгоритмически неразрешимая проблема, хотя для конкретного цикла или для определённых классов программ инвариант можно построить.
|
|
|
Для определения инварианта в рассматриваемом примере введём дополнительную переменную k, которая подсчитывает количество итераций цикла: она полагается равной нулю перед циклом и увеличивается на 1 в конце цикла. Тогда в качестве инварианта Inv предложим следующее условие
где a [ b ] означает остаток от деления а на b, а деление подразумевает деление нацело. То, что это действительно так, ещё предстоит доказать.
Для сокращения записи весь цикл обозначим WHILE, его тело - BODY, а условный оператор внутри тела - IF. Мы собираемся доказать, что
Применяя правила следствия и вывода для цикла, достаточно показать, что
1. 
2. 
3. 
Первое утверждение доказывается подстановкой k =0 в Inv, поскольку 2 k =1 и N [2 k ] = 0. Для доказательства второго утверждения достаточно заметить, что из 
следует n =0, и далее
откуда получаем 
.
Осталось доказать третье утверждение, т.е. то, что Inv действительно является инвариантом цикла. Трёхкратное применение правила для последовательности операторов и аксиомы для присвивания сводит его к доказательству утвержения для условного оператора
Оно разбивается на два случая:
и
В любом случае 
и 
. Пусть bi – i -ый разряд в двоичном представлении числа N, т.е. 
. Очевидно, что 
. Тогда
Если n -чётно, т.е. n [2]=0, то
.
Если же n -нечётно, т.е. n [2]=1, то
.
Что и требовалось доказать.
Аксиоматическая семантика может быть использована не только для спецификации результата вычислений программы. В рассмотренном примере несложно показать, что подсчитываемое количество итераций цикла k после его завершения равно 
.
Стиль
Две фразы могут выражать абсолютно один и тот же смысл, но одна воспринимается легко, а смысл другой понять сложно, потому что «так не говорят». Например, можно составить настолько сложное предложение, что к его концу будет уже непонятно, о чём шла речь в начале, хотя с точки зрения грамматики языка оно будет совершенно правильным. Эти проблемы характерны не только для естественных языков, но и для языков программирования.
Набор правил и соглашений о том, как надо оформлять программы, чтобы облегчить простоту их понимания, составляют стиль программирования. Поскольку речь идёт о субъективном восприятии, то «правильный стиль» закрепляется корпоративными стандартами оформления программ. Наличие общего стиля особенно важно, поскольку одну и ту же программу в течении её жизненного цикла может писать и исправлять большое количество людей. Зачастую свод правил может быть достаточно большим. Поскольку большая часть стилистических правил касается либо расположения текста, либо синтаксиса программы, то она может быть эффективно поддержана системой программирования, в частности, рефакторингом. Ниже мы рассмотрим несколько наиболее распространённых требований к стилю.
Лесенка»
Текст должен располагаться так, чтобы выявлять синтаксическую структуру программы. Это достигается за счёт того, что вложенные конструкции располагаются с некоторым (фиксированным) отступом. Рассмотрим, следующий фрагмент программы, в котором убраны все лишние пробелы:
int l1=busy_class(cl,d*lessons_per_day+t1);if(t1==t||l1==-1||lessons[l1]->share[0].teacher!=tch)continue;if(t1<t-1||t1>t+1)++not_sequence;else{++total_class_overload;sum+=
B_CLASS_OVERLOAD; }
Стандартным оправданием для такой записи является то, что "теперь всё перед глазами". Иногда добавляют ещё и заботу об эффективности: мол, в таком виде программа занимает меньше места[10] и транслятору придётся меньше считывать и обрабатывать ненужной информации. Однако, если теперь попытаться выяснить к какому if относится else в предпоследней строке, то придётся потратить несколько секунд, для того, чтобы дать уверенный ответ. И это для программы из четырёх строк! Если же таких строк будет несколько сотен, то задача будет практически неразрешимой без соответствующей поддержки.
|
|
|
Стилистически правильным будет следующее расположение того же самого текста:
int l1 = busy_class(cl, d*lessons_per_day + t1);
if (t1 == t
|| l1 == -1
|| lessons[l1]->share[0].teacher!= tch)
continue;
if (t1 < t-1 || t1 > t+1)
++ not_sequence;
else
{
++ total_class_overload;
sum += B_CLASS_OVERLOAD;
}
Здесь выполнены следующие требования:
· каждый оператор начинается с новой строки;
· каждая открывающая фигурная скобка находится под ключевым словом охватывающего структурного оператора, а закрывающая - строго под открывающей;
· слишком длинные выражения разбиты на несколько строк;
· перед структурными операторами вставляются дополнительные пустые строки.
Напомним, что поскольку речь идёт о стиле, то перечисленные выше требования не носят универсальный характер: правила могут быть немного другими, а набор их шире. В современных системах программирования правильные отступы при наборе текста поддерживаются автоматически, а в некоторых языках, как, например, Occam, "лесенка" является обязательной и вложенность конструкций определяется их расположением.
Имеется, кажется, единственное исключение из этих правил, которое касается вложенных условных операторов, разбирающих несколько возможных альтернатив. Например, для записи
if (x >=1000)
...
else
if (x > 0)
...
else
if (x == 0)
...
else
if (x > -1000)
...
else // x <= -1000
...
используют следующую форму, которая не приводит к "сползанию" всего текста программы вправо:
if (x >=1000)
...
else if (x > 0)
...
else if (x == 0)
...
else if (x > -1000)
...
else // x <= -1000
...
Это настолько частый случай, что в некоторых языках программирования вводят специальное ключевое слово elseif и расширяют синтаксис условного оператора.
