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

Сейбел:Как именно вы это делаете?

Пейтон-Джонс:В GHC есть флажки, которые позволяют выводить что-либо на печать.

Сейбел:Встроенные операторы печати для отладки?

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

Есть разные отладчики для Haskell. Один из них, и просто отличный, написал в этом году студент летней школы, Пепе Иборра: это интерактивный отладчик, который теперь поставляется вместе с GHC. Я, правда, его мало использовал - он появился недавно, и, кроме того, не очень понятно, как пошагово проходить функциональную программу.

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

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

Сейбел:Это как всегда. Зачем создавать новые отладчики, если люди довольствуются операторами печати?

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

Возможно, вы разговаривали в основном с людьми академического склада и с теми, кто в силу возраста не привык к сложным отладчикам. Я бы не стал делать никаких общих выводов. И, конечно, не хочу принизить значение качественных отладчиков — особенно для сложных систем с множеством программных слоев. GHC очень прост сравнительно со средой .NET, где есть слои DOM и UML, и не знаю, что еще. Теперь вокруг столько примочек, что программная поддержка становится действительно важной.

Сейбел:Еще один способ создавать правильные программы - формальные доказательства. Что вы думаете об их полезности?

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

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

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

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

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