суббота, 10 декабря 2011 г.

Разработка с помощью примеров и на основе правил

ML, наслоившись на Лерера, и на опыт разработок различных систем, нарисовало противоречие двух различных подходов в разработке. Это разработка на основе правил (формулировка фиксированных требований) и с помощью примеров (на основе единичных примеров).

Разработка с помощью примеров

Характерна тем, что имеется конечное число требований и формулировок, которые должны быть выполнены. На их основе строится все остальное.

Например.

Пользователь: «Хочу, чтобы я нажал на кнопочку, а письмо ушло по вот этому адресу.» Здесь пользователя не волнует, что будет если письмо будет очень большое. Или если сервер будет не доступен. Ему в формулировке важно, чтобы было создано письмо и оно дошло.

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

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

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

Грамотный программист в отличие от новичка в состоянии подобрать такую функцию, которая не только бы удовлетворяла всем примерам, но и имела бы грамотный запас прочности по расстоянию (не скатывалась в Overfitting и Underfitting). И кроме того, он в состоянии найти эту функцию быстро.

Можно рассмотреть это как пример формального вывода. Если мы имеем функцию возведения в квадрат:

int sqr( int x )
{
    return x*x;
}
То тест будет выглядеть например так:
int
test_sqr( int x  )
{
    const int result = sqr( 1 );
    assert_true(result > 0);
    return result;
}

void
test()
{
    assert_true( test_sqr(1) == 1 );
    assert_true( test_sqr(4) == 16 );
    assert_true( test_sqr(-1) == 1 );
    assert_true( test_sqr(0) == 0 );
}

Фактически, есть ряд примеров, которые хочет пользователь, и на них проверяет программу.

Разработка на основе правил

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

Примеры правил:

  • В системе реакция на события происходит с задержкой не более 100 мс.
  • Отправленное сообщение если не доставлено в течение 1 с, то оно не будет доставлено вообще.
  • Стрелка не должна переводиться в случае, если её секция занята (перевод стрелки под поездом).
  • При входе в функцию аргумент не должен превышать 100.

В проектируемых системах в случае наличия таких правил-аксиом можно проводить проектирование на основе правил вывода и применения методик верификации доказательством правильности. То есть, можно проверять и захватывать не отдельные примеры, а накрывать целые области.

Например если взять нашу функцию sqr, то с применением метода predicate Abstraction и выводом постусловия сверху вниз можно вывести постусловие из предусловия. Например если на входе аргумент находится в диапазоне от 0 до 10, (предусловие {0 < x < 10}), то на выходе аргумент будет находится в диапазоне от 0 до 100 (постусловие {0 < x < 100}).

Другое применение: если мы требуем, чтобы на выходе не было переполнения ({-INT_MAX < x < INT_MAX}), то с помощью правил вывода можно рассчитать предусловие:

{-INT_MAX < x*x < INT_MAX}

{x*x < INT_MAX}

{-sqrt(INT_MAX) < x < sqrt(INT_MAX)}

Таким образом получить предусловие, для которого вычисление x*x не даст переполнения.

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

Так исторически сложилось, что значительную часть времени мне пришлось провести именно в таком контексте работы — длительным изучением и применением доказательства правильности к системам. И это наложило последующий отпечаток.

Разница подходов на характерных примерах

Тренировка на примерах и вывод нужной функции из аксиом

Подход на примерах

  • Формулируется что-то вида «оно-интуитивно-должно-работать».
  • Запускается тестовый пример (на доске, в тетрадке, в голове, …). Смотрится, как оно по идее должно отработать. Интуитивно понимается, что скорее всего вот здесь проблема, а здесь возможно долго кодить, а здесь наверное надо-ещё-подумать.
  • Если обнаружены проблемы на предыдущем шаге, то начинается размышление чего-исправить-чтобы-заработало.
  • Добавляется ещё много-много-примеров. Пока не появится уверенность, что все должно работать.
  • Если ничего не получается, то идет переход к первому шагу с попыткой переписать все с нуля. Или берется таймаут до новых идей.

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

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

Серебряная пуля и результат проекта в таком подходе представляет собой функцию от «кривизны рук программистов» (интуитивного опыта в разработке), знания конкретной предметной области (кол-во шишек, набитых в данной сфере) и отсутствием белых пятен в проекте (все этапы должны быть либо известны, либо протоптаны, либо интуитивно понятны).

Подход на системе правил

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

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

В синтезе с подходом на примерах получается приблизительно следующее:

  • Исследование предметной области (ТЗ, железо, библиотеки, …) и установка правил (трафик не превышает 100 транзакций в секунду; таблица не должна содержать более 1М записей; введение индекса по такому-то полю позволит выполнить select со сложностью log N).
  • Формулировка варианта решения с учетом всех правил. Если правила невыполнимы, то задача в таком ключе не решается и надо их пересмотреть.
  • Формулировка дополнительных правил исходя из варианта решения.
  • Прогон на тестовых примерах (не важно где, в уме или на стенде).

Такой подход позволяет быстрее отбраковывать неэффективные или неверные решения, аналитически находить узкие места, формулировать конкретные требования к модулям ещё до разработки, выдавать рекомендации к построению софта. Такой подход при разработке ПРЦ для ответственных модулей и при верификации действующего софта во многом помогал и оправдывал себя. Даже не имея большого опыта разработки, и наличия мощной системы по последовательному внедрению и сопровождению, удалось создать работающую и безопасную систему. Но вот напротив, за время работы в «Intervale» данный подход имел очень ограниченное и малоэффективное применение.

Особенность железной дороги в том, что разрабатываемый софт нижнего уровня работает на одном и том же железе. С минимумом привлечения сторонних библиотек. При конкретных и не меняющихся требованиях заказчика. Все намного более жестко детерминировано. В банковских системах эти моменты теряют смысл. Требования к проекту могут измениться через неделю после старта разработки при проведенном проектировании. Исследовать свойства предметной области чаще не удается, чем удается. Перед внедрением внезапно заказчику хочется прикрутить какую-нибудь рюшечку. В документации написано, что на запрос должен прийти ответ «Пиво», а на самом деле приходит «Жопа». В договоре темп 100 транзакций в секунду, но почему-то раз в сутки в зависимости от фазы Луны происходит всплеск в 200 шт в секунду. Когда показываешь логи с фактом, то оказывается, что лучше допилить приложение. И т.д. и т.п.. В таких условиях сформулированные когда-то правила летят кувырком. Аксиомы, на которых строилась теорема, перестают быть аксиомами. И лишенное фундамента здание начинает рушиться.

Полюса применения

Известность области

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

Подход на системе правил и доказательство правильности работает с областью, которая строго изучена и детерминирована.

Изменение требований ТЗ

Для постоянно развивающихся приложений, приложений, где ничего не понятно, что будет в результате разработки, приложений, где предполагается постоянное обновление библиотек, приложений, где пользователям постоянно в голову приходят разные идеи, семь пятниц на неделе и пр. — нужно всяческое тестирование, TDD, Unit-testing, итерационная разработка, способность к постоянному допиливанию и т.п..

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

Использование библиотек

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