[Перевод] Если вы не пишете программу, не используйте язык программирования11.06.2019 12:47

Лесли Лэмпорт — автор основополагающих работ в распределённых вычислениях, а ещё вы его можете знать по буквам La в слове LaTeX — «Lamport TeX». Это он впервые, ещё в 1979 году, ввёл понятие последовательной согласованности, а его статья «How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs» получила премию Дейкстры (точней, в 2000 году премия называлась по-старому: «PODC Influential Paper Award»). Про него есть статья в Википедии, где можно добыть ещё несколько интересных ссылок. Если вы в восторге от решения задач на happens-before или проблемы византийских генералов (BFT), то должны понимать, что за всем этим стоит Лэмпорт.

Эта хабрастатья — перевод доклада Лесли на Heidelberg Laureate Forum в 2018 году. В докладе пойдёт речь о формальных методах, применяемых в разработке сложных и критичных систем вроде космического зонда Rosetta или движков Amazon Web Services. Просмотр этого доклада является обязательным для посещения сессии вопросов и ответов, которую проведет Лесли на конференции Hydra — эта хабрастатья может сэкономить вам час времени на просмотр видео. На этом вступление закончено, мы передаём слово автору.

Когда-то давно Тони Хоар написал: «В каждой большой программе живет маленькая программа, которая пытается выбраться наружу». Я бы это перефразировал так: «В каждой большой программе живет алгоритм, который пытается выбраться наружу». Не знаю, правда, согласится ли с такой интерпретацией Тони.

Рассмотрим в качестве примера алгоритм Евклида для нахождения наибольшего общего делителя двух положительных целых чисел $(M, N)$ . В этом алгоритме мы присваиваем $x$ значение $M$ , $N$ — значение $y$ , и затем отнимаем наибольшее из этих значений от наименьшего, пока они не оказываются равны. Значение этих $x$ и $y$ и будет наибольшим общим делителем. В чем существенное отличие этого алгоритма и программы, которая его реализует? В такой программе будет много низкоуровневых вещей: у $M$ и $N$ будет определенный тип, BigInteger или что-то в таком роде; нужно будет определить поведение программы в случае, если $M$ и $N$ неположительные; и так далее и тому подобное. Четкой разницы между алгоритмами и программами нет, но на интуитивном уровне мы чувствуем отличие — алгоритмы более абстрактные, более высокоуровневые. И, как я уже сказал, внутри каждой программы живет алгоритм, который пытается выбраться наружу. Обычно это не те алгоритмы, про которые нам рассказывали в курсе алгоритмов. Как правило, это алгоритм, который полезен только для данной конкретной программы. Чаще всего он будет значительно сложнее тех, которые описаны в книгах. Такие алгоритмы зачастую называют спецификациями. И в большинстве случаев выбраться наружу этому алгоритму не удается, потому что программист не подозревает о его существовании. Дело в том, что этот алгоритм нельзя увидеть, если ваше мышление сосредоточено на коде, на типах, исключениях, циклах while и прочем, а не на математических свойствах чисел. Программу, написанную таким образом, сложно отлаживать, поэтому что это значит отлаживать алгоритм на уровне кода. Средства отладки предназначены для того, чтобы находить ошибки в коде, а не в алгоритме. Кроме того, такая программа будет неэффективной, потому что, опять-таки, вы будете оптимизировать алгоритм на уровне кода.

Как и почти в любой другой области науки и техники, решить эти проблемы можно, описав их математически. Для этого существует много способов, мы рассмотрим наиболее полезный из них. Он работает как с последовательными, так и с параллельными (распределенными) алгоритмами. Заключается этот метод в том, чтобы описать выполнение алгоритма как последовательность состояний, а каждое состояние — как присвоение свойств переменным. Например, алгоритм Евклида описывается как последовательность следующих состояний: вначале x присваивается значение M (число 12), а y — значение N (число 18). Затем мы отнимаем меньшее значение от большего ( $x$ от $y$ ), что приводит нас к следующему состоянию, в котором мы отнимаем уже $y$ от $x$ , и на этом выполнение алгоритма останавливается: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6], [x \leftarrow 6, \leftarrow 6]$ .

Назовем последовательность состояний поведением, а пару последовательных состояний — шагом. Тогда любой алгоритм можно описать множеством поведений, которые представляют все возможные варианты выполнения алгоритма. Для каждого конкретного M и N есть только один вариант выполнения, поэтому для его описания достаточно множества из одного поведения. У более сложных алгоритмов, в особенности параллельных, множества поведений большие.

Множество поведений описывается, во-первых, начальным предикатом для состояний (предикат — это просто функция с булевым значением); и, во-вторых, предикатом следующего состояния для пар состояний. Некоторое поведение $s_1, s_2, s_3 ...$ входит в множество поведений только если начальный предикат верен для $s_1$ , и предикаты следующего состояния верны для каждого шага $(s_i, s_{i+1})$ . Попробуем описать таким образом алгоритм Евклида. Начальный предикат здесь такой: $(x = M)\land(y = N)$ . А предикат следующего состояния для пар состояний здесь описывается следующей формулой:

$$Next_E:\\ \hspace{0.5cm}\hspace{0.5cm}(\hspace{1.2cm}(x>y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x-y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y)\hspace{0.6cm})\\ \lor\hspace{0.7cm}(\hspace{1.2cm}(y>x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y-x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x)\hspace{0.6cm})$» /> Пожалуйста, не пугайтесь — в ней всего шесть строк, разобраться в них очень просто, если делать это по порядку. В этой формуле переменные без штрихов относятся к первому состоянию, а переменные со штрихами — это те же переменные во втором состоянии. Как видим, первая строка гласит, что в первом случае x больше y в первом состоянии. После логического И утверждается, что значение x во втором состоянии равно значению x в первом состоянии минус значение y в первом состоянии. После еще одного логического И утверждается, что значение y во втором состоянии равно значению y в первом состоянии. Все это значит, что в случае, когда x больше y, программа отнимет y от x, а y оставит неизменным. Последние три строки описывают случай, когда y больше x. Обратите внимание, что эта формула ложна, если x равен y. В этом случае следующего состояния нет, и поведение останавливается. Итак, мы только что описали алгоритм Евклида двумя математическими формулами — и нам не пришлось связываться ни с каким языком программирования. Что может быть прекраснее этих двух формул? Заменить их одной формулой. Поведение <img src=$ является выполнением алгоритма Евклида только в том случае, если:

верно для ,
верно для каждого шага $(s_i, s_{i+1})$ .

Записать это как предикат для поведений (будем называеть его свойством) можно следующим образом. Первое условие можно выразить просто как $Init_E$ . Это значит, что мы интерпретируем предикат состояния как верный для поведения только в том случае, если он верен для первого состояния. Второе условие записывается так: $\square Next_E$ . Квадрат означает соответствие между предикатами пар состояний и предикатами поведений, то есть $Next_E$ верно для каждого шага в поведении. В итоге формула выглядит так: $Init_E\land\square Next_E$ .

Итак, мы записали алгоритм Евклида математически. В сущности, это просто определения, или сокращения для $Init_E$ и $Next_E$ . Полностью эта формула выглядела бы так:

$$(x = M) \land (y = N) \land\square\thinspace\thinspace(\\ \hspace{0.5cm}\hspace{0.5cm}(\hspace{1.2cm}(x>y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x-y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y)\hspace{0.6cm})\\ \lor\hspace{0.7cm}(\hspace{1.2cm}(y>x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y-x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x)\hspace{0.6cm})$» /> Не правда ли, она прекрасна? К сожалению, для науки и техники красота не является определяющим критерием, но она говорит о том, что мы на правильном пути. Свойство, которое мы записали, верно для некоторого поведения только в том случае, если выполняются два условия, которые мы только что описали. При <img src=$ и $N = 18$ они верны для следующего поведения: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6], [x \leftarrow 6, \leftarrow 6]$ . Но эти условия также выполняются для более коротких версий того же поведения: $[x \leftarrow 12, \leftarrow 18], [x \leftarrow 12, \leftarrow 6]$ . А их мы не должны учитывать, поскольку это просто отдельные шаги уже учтенного нами поведения. Есть очевидный способ от них избавиться: просто не учитывать поведения, которые заканчиваются состоянием, для которого возможен хотя бы один следующий шаг. Но это не совсем правильный подход, нам нужно более общее решение. Кроме того, такое условие не всегда работает.

Обсуждение этой проблемы приводит нас к понятиям безопасности и активности. Свойство безопасности указывает, какие события допустимы. Например, алгоритму разрешается вернуть правильное значение. Свойство активности указывает, какие события должны рано или поздно произойти. Например, алгоритм рано или поздно должен вернуть некоторое значение. Для алгоритма Евклида свойство безопасности выглядит следующим образом: $Init_E \land \square Next_E$ . К этому необходимо добавить свойство активности, чтобы исключить преждевременные остановки: $Init_E \land \square Next_E \land L$ . В языках программирования в лучшем случае есть некоторое примитивное определение активности. Чаще всего активность даже не упоминается, просто подразумевается, что следующий шаг в программе обязательно должен произойти. И чтобы добавить это свойство, нужен довольно замысловатый код. Математически же активность выразить очень легко (как раз для этого нужен тот квадратик), но, к сожалению, у меня на это нет времени — нам придется ограничить наше обсуждение безопасностью.

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

$s = 17, \sqrt{2}, -2, \pi, 10, 1/2\\ t = 17, \sqrt{2}, -2, e, 10, 1/2$

Расстояние между этими двумя функциями — ¼, поскольку первое различие между ними — на четвертом элементе. Соответственно, чем более продолжителен участок, на котором эти последовательности идентичны, тем ближе они друг к другу. Сама по себе эта функция не так уж и интересна, но она создает очень интересную топологию. В этой топологии свойства безопасности являются замкнутыми множествами, а свойства активности являются плотными множествами. В топологии одна из фундаментальных теорем гласит, что каждое множество является пересечением замкнутого множества и плотного множества. Если вспомнить, что свойства — это множества поведений, то из этой теоремы следует, что каждое свойство является конъюнкцией свойства безопасности и свойства активности. Это вывод, который будет интересен в том числе и программистам.

Частичная корректность означает, что программа может остановиться только в том случае, если выдаст правильный ответ. Частичная корректность алгоритма Евклида гласит, что если он завершил выполнение, то $x = GCD(M, N)$ . А завершает выполнение наш алгоритм в случае, если $x = y$ . Иначе говоря, $(x = y) \Rightarrow (x = GCD(M, N))$ . Частичная правильность этого алгоритма означает, что эта формула верна для всех состояний поведения. Добавим в ее начало символ $\square$ , который означает «для всех шагов». Как видим, в формуле нет переменных со штрихом, так что ее истинность зависит от первого состояния в каждом шаге. А если нечто верно для первого состояния каждого шага, то это утверждение верно для всех состояний. Частичная корректность алгоритма Евклида удовлетворяется любым поведением, допустимым для алгоритма. Как мы видели, поведение допустимо в том случае, если истинна только что приведенная формула. Когда мы говорим, что свойство удовлетворено, это просто значит, что это свойство следует из некоторой формулы. Не правда ли, это прекрасно? Вот она:

$Init_E\land\square Next_E \Rightarrow \square((x = y) \Rightarrow (x = GCD(M, N)))$

Перейдем к инвариантности. Квадрат со скобками после него называется свойство инвариантности:

$Init_E\land\square Next_E \Rightarrow \color{red}{\square((x = y) \Rightarrow (x = GCD(M, N)))}$

Значение, заключенное в скобки после квадрата, называется инвариант:

$Init_E\land\square Next_E \Rightarrow \square(\color{red}{(x = y) \Rightarrow (x = GCD(M, N))})$

Как доказать инвариантность? Чтобы доказать $Init_E\land\square Next_E \Rightarrow \square I_E$ , нужно доказать, что для любого поведения $s_1, s_2, s_3 ...$ следствием $Init_E\land\square Next_E$ является истинность $I_E$ для любого состояния $s_j$ . Мы можем доказать это методом индукции, для этого нам необходимо доказать следующее:

из $Init_E\land\square Next_E$ следует, что верно для состояния ;
из $Init_E\land\square Next_E$ следует, что если верно для состояния , то оно также
верно для состояния $s_{j+1}$ .

Вначале нужно доказать, что $Init_E$ подразумевает $I_E$ . Поскольку формула утверждает, что верно для первого состояния, это значит, что $I_E$ верно для первого состояния. Далее, при $Next_E$ , верном для любого шага, и $I_E$ , верном для $s_j$ , $I_E$ верно для $s_{j+1}$ , потому что $\square Next_E$ значит, что верно для любой пары состояний. Это записывается так: $Next_E \land I_E \Rightarrow I'_E$ , где $I'_E$ — это $I_E$ для всех переменных со штрихом.

Инвариант, отвечающим двум условиям, которые мы только что доказали, называется индуктивным инвариантом. Частичная корректность не индуктивна. Чтобы доказать ее инвариантность, нужно найти индуктивный инвариант, который ее подразумевает. В нашем случае индуктивный инвариант будет такой: $GCD(x, y) = GCD(M, N)$ .

Каждое следующее действие алгоритма зависит от его текущего состояния, а не от прошлых действий. Алгоритм удовлетворяет свойству безопасности, поскольку в нем сохраняется индуктивный инвариант. Алгоритм Евклида может вычислить наибольший общий знаменатель (т. е. он не останавливается, пока его не достигнет) благодаря тому, что в нем есть инвариант $GCD(x, y) = GCD(M, N)$ . Чтобы понять алгоритм, необходимо знать его индуктивный инвариант. Если вы изучали верификацию программ, то вы знаете, что только что приведенное доказательство инварианта — это ни что иное, как метод доказательства частичной корректности последовательных программ Флойда-Хоара. Возможно, вы также слышали о методе Овики-Грис, который является распространением метода Флойда-Хоара на параллельные программы. В обоих случаях индуктивный инвариант пишется при помощи аннотации программы. И если это делать при помощи математики, а не языка программирования, это делается предельно просто. Именно это лежит в основе метода Овики-Грис. Математика делает сложные явления значительно доступнее для понимания, хотя сами явления, конечно же, от этого не станут проще.

Взглянем подробнее на формулы. Если в математике мы написали формулу с переменными $x$ и $y$ , это не значит, что других переменных не существует. Можно добавить еще одно уравнение, в котором $y$ поставлено в отношение к $z$ , это ничего не поменяет. Просто формула ничего не говорит ни о каких других переменных. Я уже говорил, что состояние — это присвоение значений переменным, сейчас к этому можно добавить: всем возможным переменным, начиная $x$ и $y$ и заканчивая населением Ирана. Должен признаться: когда я сказал, что формула $Init_E\land\square Next_E$ описывает алгоритм Евклида, я соврал. На самом деле она описывает вселенную, в которой значения $x$ и $y$ представляют выполнение алгоритма Евклида. Вторая часть формулы ( $\square Next_E$ ) утверждает, что каждый шаг изменяет $x$ или $y$ . Иначе говоря, она описывает вселенную, в которой население Ирана может измениться только в том случае, если изменилось значение $x$ или $y$ . Из этого следует, что в Иране никто не может родиться после того, как завершено выполнение алгоритма Евклида. Очевидно, это не так. Исправить эту ошибку можно в том случае, если у нас допустимы шаги, для которых $x$ и $y$ остаются неизменными. Поэтому к нашей формуле нужно добавить еще одну часть: $Init_E \land \square (Next_E \lor (x' = x) \land (y' = y))$ . Для краткости запишем это так: $$Init_E \land \square [Next_E]_{<x,y>}$» />. Эта формула описывает вселенную, содержащую алгоритм Евклида. Те же изменения нужно внести в доказательство инварианта: <ul><li>Доказываем: <img src=$

$$\color{red}{\square [Next_E]_{<x,y>}} \land I_E \Rightarrow I'_E$» /></li> </ol></li> </ul> Это изменение отвечает за безопасность алгоритма Евклида, поскольку теперь возможны поведения, в которых значения <img src=$ и $y$

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

Поговорим о реализации. Предположим, у нас есть некоторая машина, которая реализует алгоритм Евклида подобно компьютеру. Она представляет числа как массивы 32-битных слов. Для простых операций сложения и вычитания ей нужно множество шагов, как компьютеру. Если пока не трогать активность, то такую машину мы также можем представить формулой $$Init_{ME} \land \square [Next_{ME}]_{<...>}$» />. Что мы подразумеваем, когда говорим, что машина Евклида реализует алгоритм Евклида? Это значит, что следующая формула верна: <img src=$ ). Этим свойством является формула Евклида $$(Init_E \land \square [Next_E]_{<х,у>}$» />, многоточия — это выражения, которые содержат переменные машины Евклида, а <img src=$ — это подстановка. Иначе говоря, вторая строка — это формула Евклида, в которой $x$ и $y$ заменены на выражения в многоточиях. В математике нет общепринятого обозначения подстановки, поэтому мне пришлось придумать его самому. По сути, формула Евклида ( $$Init_E \land \square [Next_E]_{<х,у>}$» />) — это сокращение для формулы: <img src=$ и $y$ в $$(Init_E \land \square [Next_E]_{\color{red}{<х,у>}}$» /> оставаться неизменными. Описанное выражение утверждает не только, что машина реализует алгоритм Евклида, но и что она делает это с учетом указанных подстановок. Если просто взять пару программ и сказать, что переменные этих программ связаны с <img src=$ и $y$ — бессмысленно говорить, что всё это «реализует алгоритм Евклида». Обязательно указать, как именно алгоритм будет реализован, почему после всех подстановок формула станет истинной. Сейчас у меня нет времени, чтобы показать, что описанное выше определение является правильным, вам придется поверить мне на слово. Но вы, я думаю, уже оценили, насколько оно простое и элегантное. Математика действительно прекрасна — при помощи нее мы смогли определить, что значит, что один алгоритм реализует другой.

Чтобы доказать это, необходимо найти подходящий инвариант $I_{ME}$ машины Евклида. Для этого необходимо выполнить следующие условия:

$Init_{ME} \Rightarrow (Init_E, WITH\thinspace x\leftarrow ..., y \leftarrow ...)$
$$I_{ME} \land [Next_{ME}]_{<...>} \Rightarrow ([Next_E]_{<х,у>}, WITH\thinspace x\leftarrow …, y \leftarrow …)$» /></li> </ol> Не будем сейчас в них вникать, просто обратите внимание на то, что это обычные математические формулы, хоть и не самые простые. Инвариант <img src=$ объясняет, почему машина Евклида реализует алгоритм Евклида. Реализация означает подстановку выражений на место переменных. Это вполне обычная математическая операция. Но в программе такую подстановку выполнить невозможно. Нельзя подставить a + b на место x в выражении присвоения x = …, такая запись не будет иметь смысла. Тогда как определить, что одна программа реализует другую? Если вы думаете только в рамках программирования — это невозможно. В лучшем случае вы сможете найти какое-нибудь мудреное определение, но гораздо более хороший способ — перевести программы в математические формулы и использовать определение, которое я привел выше. Перевести программу в математическую формулу значит дать программе семантику. Если машина Евклида является программой, а $$Init_{ME} \land \square [Next_{ME}]_{<...>}$» /> — ее математическая запись, то <img src=$ :

$$Next_E:\\ \hspace{0.5cm}\hspace{0.5cm}(\color{red}{\hspace{1.2cm}(x>y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x-y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y)}\hspace{0.6cm})\\ \lor\hspace{0.7cm}(\hspace{1.2cm}(y>x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y-x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x)\hspace{0.6cm})$» /> а вот эту часть — <img src=$ :

$$Next_E:\\ \hspace{0.5cm}\hspace{0.5cm}(\hspace{1.2cm}(x>y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x-y)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y)\hspace{0.6cm})\\ \lor\hspace{0.7cm}(\hspace{1.2cm}\color{red}{(y>x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(y' = y-x)\\ \hspace{0.5cm}\hspace{0.5cm}\hspace{0.5cm}\land\hspace{0.5cm}(x' = x)}\hspace{0.6cm})$» /> Поэтому можно сказать, что: <img src=$ © Habrahabr.ru