Кодеры за работой. Размышления о ремесле программиста

Пейтон-Джонс: Представьте, что ваша цель - иметь для всего автоматическую проверку правильности. Что это будет означать? Проверка по сравнению с чем? По сравнению с некоей спецификацией. Что за спецификация? Она должна описывать все, что делает программа, иначе проверка невозможна. Итак, должна быть формальная спецификация для каждого действия программы. Как написать такую спецификацию? Допустим, вы пользуетесь функциональным языком. Тогда, может быть, ваша спецификация - это и есть ваша программа?

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

Более продуктивным для практических целей будет описание некоторых свойств, которыми должна обладать программа. К примеру, вы пишете: “Клапан 1 никогда не должен закрываться одновременно с клапаном 2. Это дерево всегда должно быть сбалансировано. Эта функция всегда должна иметь результат больше нуля”. Это небольшие частичные спецификации, не полные. Это просто утверждения, в которых вы хотите быть уверены.

Как их написать? Функциональные языки неплохо приспособлены для этого. Именно это и происходит, если писать спецификацию в Quick-Check - свойства получаются функциями языка Haskell. Допустим, мы хотим проверить, что функция reverse является своей противоположностью, тогда мы напишем check reverse с типом список из А -> булевское значение. Итак, checkreverse от xs будет: reverse от reverse xs равно xs. Это функция, которая всегда оказывается верной. Функция-свойство. Но она написана на том же самом языке, и это здорово.

Теперь можно думать о статических проверках этого. Это может быть трудно, а может и легко. Но все равно, если свойство записано по всем правилам, это большое облегчение. Можно проверить его путем генерирования тестовых данных - именно это делает QuickCheck.

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

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

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

Мне кажется очень важным уйти от этого глобального подхода, “все или ничего”, в сторону очень полезного статического и динамического тестирования частичных спецификаций. Это повысит вашу уверенность в правильности программы, а на большее рассчитывать нельзя. Даже так называемые полные спецификации не учитывают вещи вроде того, что программа должна работать за 0,1 с или занимать не более 10 Кбайт памяти. Часто в них ничего не говорится о ресурсах, о времени. Даже если программа формально отвечает спецификации, из-за этих мелочей она может работать не так, как нужно. Думаю, мы обманываем себя, когда говорим, что проверили программу и все в порядке. Лучше честно сказать, что мы повышаем свою уверенность в ней. Тут все может начинаться скромно - вы повышаете уверенность на 75%, прикладывая всего 5% от общего количества усилий. Это хороший показатель.

Сейбел: Поговорим о параллелизме. Гай Стил поручил мне задать вам вопрос о транзакционной памяти - спасет она мир или все же нет?

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

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

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