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, итерационная разработка, способность к постоянному допиливанию и т.п..
Если же свойства конкретно определены и не меняются, и при этом разработка идет на библиотеках/компиляторах/…, которые не изменятся, запуск планируется на одном или очень похожем железе с ОС такого же свойства, то возможно строгое задание правил и использование всех преимуществ доказательства правильности.
Использование библиотек
В описании библиотек, интерфейсов и прочих велосипедов есть как строгое задание свойств, так и обучение на примерах. Последователи последнего подхода очень любят хорошие примеры, по которым сразу интуитивно понятно, как это работает. При этом особо не замечая строгие свойства, если они заданы. В результате подход на примерах дает быструю разработку чего-то работающего. Что потом, если нужно, можно допилить. Главное хорошо покрыть тестами.
