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

Недавно появилась статья, чем-то напоминающая много кем известную "Они пишут правильную вещь" (оригинал).

Мне кажутся интересными ряд моментов для передачи свойств предметной области. А вместо их выделения проще привести и перевести все целиком. Ниже мой перевод.

---

Как правило, обычный писатель программ-скриптов скорее всего не приводит полный пакет доказательств со всей строгостью формальной верификации. Это хорошо потому, что средний программист также не пишет программы для реактивных самолетов или атомных станций, или для роботов-хирургов. Но кто-то же пишет — и когда ваша жизнь окажется в руках его программы, то хорошо бы иметь высокую вероятность безошибочной её работы. И в тот момент, как вы можете быть уверенным в том, что этот человек, — не бездарность?

А никак. Что ставит другой вопрос: как этот тип программ тестируется?

Это было в небольшом посте блога, написанном Gene Spafford, профессором информатики в Purdue University, написанным на волне ответа на этот конкретный вопрос. Он ссылается на историю об истоках кокпитов, где началась применятся проводная связь — такие самолеты управляются в полете электроникой, внедрение чего случилось непосредственно в конце 1980х. Мы уже привыкли к таким самолетам, но тогда это был большой скачок вперед: прямой контроль был убран и передан в руки программного обеспечения, которое было разработано для телеуправления механическими приводами из кокпита. С того момента компьютер мог разбить самолет.

А фактом являлось то, что людей, которые отвечали за компьтеры, поместили непосредственно в тестируемую среду.

Spafford пишет:

В конце 1980х, где-то когда аэробус A340 был представлен (1991), тем из нас, кто работал над разработкой программного обеспечения, критичного к безопасности, рассказывали историю (возможно апокрифическую). Эта история о том, как программное обеспечение электронной авионики тестировалось на основных коммерческих авиалайнерах. Согласно истории, инженеры аэробуса реализовали и верифицировали согласно последним самым сильным формальным методам, предоставляли результаты проверки моделей и формального доказательства всего кода авионики. В то же время, согласно истории, Боинг выполнял обширное тестирование и рецензию кода, и принуждал всех своих инженеров программного обеспечения участвовать в первых полетах самолетов. Основным результатом истории было то, что для большинства из нас (как казалось) было то, что всем нам было более комфортнее лететь на самолете Боинга (было бы интересно посмотреть осталось ли таким же мнение сообщества программистов).

Таким образом, программисты Боинга имели дополнительную мотивацию потому, что им в будущем приходилось отдать свою жизнь в руки своего же программного обеспечения. Там, на высоте 9 000 метров, нет возможности что-то исправить — оно должно просто работать. И с чем вы будете более комфортно чувствовать: имея чей-то личный подход к верификации программного обеспечения (прим. оценка эксперта, рецензия), или, с другой стороны, имея кучу формальных доказательств и результатов имитационных испытаний?

Я бы предпочел и то и другое, но вопрос как тестируется это все интересен сам по себе. Ветка Stack Exchange 2011-го года предоставляет много интересного внутренней кухни данного процесса и его эволюции. Для начала, подход Боинга выходит из моды и в основном вышел из моды, согласно сообщению гуглера Uri Dekel:

Там серьезный шаг вперед в плане формальной верификации по сравнению со случайным функциональным тестированием. Государственные агенства, такие как НАСА и некоторые военные ведомства, тратят больше и больше денег на развитие этих технологий. Решение задач такого уровня все ещё PITA (pain in the ass — боль в заднице) для среднего программиста, но они намного более эффективны в тестировании систем, критичных по безопасности.

Scott Whitlock, инженер-программист, который поддерживает свою библиотеку для автоматического тестирования FluentDwelling, смотрит глубже, разьясняя проектные требования для безопасных трансляторов, являющихся системами промышленного применения для мониторинга оборудования, который передает сигналы предупреждения и может остановить сложное оборудование в случае необходимости. Они включают в себя, согласно Whitlock'y, "Два резервированных процессора, которые обычно запистываются от независимых источников питания, и выполненных конструкционно по-разному. Код, работающий на каждом процессоре, разработан двумя раными командами программистов, выполнивших свою работу в изолорованных друг от друга условиях. Результат вычислений обеих процессоров должен быть одинаков, иначе срабатывает реле безопасности."

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

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

"Это программное обеспечение никогда не падает" — пишет Charles Fishman. "Оно никогда не требует перезагрузки. Это програмное обеспечение без багов. Оно совершенно настолько, насколько это возможно из всего того, что было создано человеком. Посмотрите на эту статистику: как минимум три версии программы — каждая по 420 000 строк кода, имело только по одной ошибке. Последний 11 версий имели в общей сложности 17 ошибок. Типичные программы на рынке такой сложности будут иметь 5000 ошибок."

Как программисты НАСА все это делают? Ну, в основном им просто приходится. Малейший баг создает риск потери миллиардов доллагоров и жизней людей. И все это под пристальным вниманием публики.

Для кода как такового, идаельность приходит как результат в основном засчет прямой противоположности тому, что обычно ассоциируется под словом "программист". Креативность в команде Шаттла не приветствуется; работа в режиме 9х5; хитрый код и программисты-суперзвезды не приживаются; более половины команды женщины; отладка (debugging) практически отсутствует, так как ошибки являются редчайшим явлением. Программирование стало продуктом не кодеров и инженеров, а Процесса.

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

И далее:

Группа разработки должна предоставить код, который полностью лишен ошибок, настолько идеальным, что тестировщики не должны ничего найти. Группа тестирования должна идти далеко во множестве сценариев полетов и моделирования, и стараются выявить настолько много недостатков, насколько это возможно. Результат — то, что Tom Peterson называет "дружественно-враждебные отношения". "Они соревнутся в том, что найдет ошибки." говорит Keller. "Иногда они дерутся как кошки и собаки. Разработчики хотят поймать все свои ошибки. Верификаторы возмущаются, что это забирает их время, выделенное на проверку программного обеспечения."

Итак, что вы думаете, астронавт будущего? Программист, который летит на орбиту под контролем своего программного обеспечения, или программист из группы НАСА?

Синглтоны языков программирования

Разбираясь с некоторыми вопросами высоконадежных систем, предназначенных для управления критически важных процессов информатизации (safety-critical systems), нашел некоторую особенность и попытался её разгрызть, почему сделано так.

Согласно стандарту ISO 61508 (сейчас он же действующий ГОСТ Р МЭК 61508), крайне не рекомендуется использовать динамическую память и динамические объекты (что для серьезных западных систем означает нельзя). Аналогичные требования есть в JPL Coding Standard (это ответственные системы NASA, например софт для марсоходов и МКС) и в MISRA C/C++(ответственные системы по умолчанию, например химическое производство которое может устроить катастрофу или автомобильный транспорт с тем же потенциалом для последствий).

Однако, если создать свою структуру данных и верифицировать её в рамках проекта (это обычно не означает написать пару сотен строк кода за день-два, а работу нескольких высококлассных специалистов в течение нескольких месяцев (счет для самых простых структур данных начинается с 3-х месяцев), которые проведут её через все этапы разработки с многоверсионными проверками спецификаций, полным черно-белым тестированием, верификацией формальными методами с использованием дедуктивного анализа и модели с задействованием автоматики, экспертная оценка как человеком, так и автоматикой (статическими анализаторами кода в т.ч.), и все это умножить на два из-за проверки независимой группой по всем этапам). Удовольствие дорогое, но возможное. (отдельным путем является использование компилятора, обеспечивающего безопасное поведение в случае отказов; классические и всем известные C/C++ к таковым не относятся; к ним обычно относится верифицированный куцый C/C++).

Авторов всего этого понять можно: динамика поставила на колени далеко не один проект С/C++, а в последние годы много усилий ушло на уменьшение последствий от возможных проблем на данном минном поле.

Прошло какое-то время, прежде чем мною ощутилась разница между описанным первым (глобальной динамикой) и вторым (верифицированными структурами данных): отдельно разрабатываемые структуры данных играют (в том числе) роль специализированных менеджеров памяти, а поставляемые в коробке new/delete и malloc/free — синглтонов языка программирования.

Динамика как синглтон

new/malloc и delete/free работают глобально, в одной большой куче. Доступ к ней есть отовсюду. О том, как лучше работать с этой кучей — изобретается множество инструментов и техник, так как надо контролировать создание (только один раз) и удаление (только один раз и только после создания), обрабатывать ошибки (переполнение памяти), попадать куда надо указателем (неопределенное поведение) и типом (срезка), получать доступ и разделять ответственность. Фактически сама куча является глобальной структурой данных, поддерживаемой на уровне языка.

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

Если мы берем тот же вектор, то он сам является динамической структурой и может что-нибудь сломать из-за недостатка памяти. Однако намного легче построить программу так, что вектор никогда не расширится выше какого-то предела и при этом не будет протекать (а он может). В случае же проблем можно реализовать переход в безопасное состояние, что делает систему более надежной и безопасной.

Синглтоны C++

Прошелся по языку и нашел следующие синглтоны:

• new/delete
• static
• cout/cerr/cin
• Ресурсы (файловые дескрипторы, коннекты, потоки, …).
• Нелокальные макросы.
• Указатели.

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

Свойства

Свойства очень похожи из того, что есть в оригинальном синглтоне. Для всех описанных (кроме макросов, они на этапе сборки):

• необходимо заниматься синхронизацией в многопоточном приложении;
• все сущности видны отовсюду, и любой может сломать сразу все;
• если в проекте/библиотеке сущность уже прибита гвоздями к стенке, то её размножить сложно;
• нужно заботиться о потенциальных побочных эффектах и сводить в stateless после каждого вызова;
• узкое горлышко многопоточной производительности;
• некоторые синглтоны обладают разной степенью глобальности.

Если начинают появляться проблемы с синглтоновостью, то часть из них решается разбиением на модули в виде отдельного процесса, у которого своя куча, свой лог, свои ресурсы. Таким образом мы синглтоны режем на другие синглтоны и частично решаем проблему модульностью. Вторая часть решается переходом на отдельные структуры данных. Т.е. из динамики лучше уйти в свои контейнеры, а если возможно — то в контейнеры проверенных временем библиотек (STL). Третья часть — если есть возможность уйти от динамики, то лучше уйти. Например полиморфить через ссылки, а не указатели.

Т.о., понимание синглтонов позволяет лучше ощутить источник проблем и ведет к светлому будущему (;

О правильном

В начале всяческой философии лежит удивление, ее развитием является исследование, ее концом — незнание.

М. Монтень

Не бывает правильных (тру-шных и т.п.) программ. Бывают программы с определенными свойствами. Мы не проверяем тестами корректность программы, и не доказываем правильность формальными методами — а определяем вполне её конкретные свойства.

Не бывает правильного способа решения проблемы. Бывают способы с определенными последствиями.

Не бывает правильного принципа или метода. Бывают принципы и методы с определенными достоинствами и недостатками, работающие в определенном окружении.

Выражения «программа должна работать без ошибок», «система должна работать как можно быстрее», «не должно произойти ничего страшного, никогда и ни при каких обстоятельствах» — без контекста лишены смысла. В первом случае должен быть конкретный критерий что есть ошибка, во втором случае обозначен конкретный предел скорости, а в третьем — не бывает абсолютно безопасных систем.

Одно дело когда известен контекст и все понимают, чем «правильный» вариант лучше, чем остальные. Другое дело, когда контекст теряется, и народ уже не понимает что стоит за словом «правильный». «Потому что так написано в книге Х», «Потому что так сказал Y», «Мы всегда делали Z, и в дальнейшем будем делать так же», …

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

После того, как схема принята, то изменить её сложно. Классическая цитата Лоренца:

Для существа, лишенного понимания причинных взаимосвязей, должно быть в высшей степени полезно придерживаться той линии поведения, которая уже — единожды или повторно — оказывалась безопасной и ведущей к цели. Если неизвестно, какие именно детали общей последовательности действий существенны для успеха и безопасности, то лучше всего с рабской точностью повторять ее целиком. Принцип «как бы чего не вышло» совершенно ясно выражается в уже упомянутых суевериях: забыв произнести заклинание, люди испытывают страх. (К. Лоренц, Агрессия)

Если существо работает «правильными методами», которые лишены понимания причинно-следственных взаимосвязей, то мы и получаем такую картину, когда делается потому, что так делалось всегда, а шаг в сторону — это страшно. И работает эта штука подсознательно.

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

Понимайте причинно-следственные взаимосвязи.

Гуманитарные и технические науки

В каждой естественной науке заключено столько истины, сколько в ней математики.

(И. Кант)

Всё, что нельзя выразить в цифрах — это не наука, это — мнение.

(Роберт Хайнлайн)

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

Необходимое условие точных наук

Оно же — необходимое условие для технических наук, для математики и для работы технического мышления.

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

Ключевое здесь то, что любая техническая теория работает только тогда, когда имеется набор железобетонных утверждений. То есть, аксиом, которые выполняются всегда. Например, только если свет распространяется по прямой, то только тогда мы получим геометрию Евклида. Только если числа 1,2,3,4,… упорядочены друг за другом — получим арифметику. Аксиомой может быть постулат или закон (непреодолимость скорости света, закон Ома, …), т.е. что-то, обладающее свойством железобетонности.

Если таких аксиом нет, то нет никакой технической науки. Нет ни математики, ни матмоделей, ни формул, ни цифр, … Но, тем не менее, есть науки, которые не содержат в себе аксиом. Например лингвистика (смысл слова в которой у каждого человека может отличаться от другого и меняться с течением времени; все, что касается правил — работает с исключениями, поправками, натяжками и «авторским стилем»). Кроме того, есть науки, в которых часть изучаемой области аксиоматике не поддается. Например в биологии молекула ДНК это не постоянный носитель информации, а такой носитель, который может в любой момент изменится, быть исправленным другим носителем, стать активным устройством и др..

Постоянный процесс формализации в технических науках

Изначально если брать какую либо предметную область, на сейчас покрытую технической наукой, то в ней не было аксиом. Была предметная область, в которой было все непонятно. Звезды непонятно двигались по небу, тела непонятно как взаимодействовали в природе, свет и тепло непонятно как распространялись и пр.. С течением времени начали замечать, что есть что-то, что повторяется. Есть какие-то свойства, которые закономерны. То есть, в непонятной области выполнялась процедура классификации: выбирались некоторые классы явлений, для которых описывались закономерные свойства. Свет распространялся по прямой, тепло передавалось от горячего к холодному, тела чаще падали на землю, нежели оставались в воздухе и т.д..

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

Таким образом, во-первых, в технических науках постоянно идет процесс формализации. Когда непонятное становится более понятным, количество моделей множится, а наши возможности их использовать увеличиваются. Сам период развития предметной области можно разделить на доаксиоматический и аксиоматический. Во-вторых, техническая наука работает только тогда, когда есть аксиомы. Поэтому техническое мышление начинает сильнее работать только по мере появления новых железобетонных знаний о мире. В-третьих, аксиомы могут быть сгруппированы и сформулированы различным образом. То есть, один и тот же процесс закономерностей можно описать различным набором аксиом (например выбрать 4 направления север-юг-запад-восток, или 4 аналогичных СВ-СЗ-ЮЗ-ЮВ).

Отсутствие аксиом

Что же делать, если аксиом нет? Неужели тут наук нет?

Этим делом как раз таки занимаются гуманитарные науки (в данном контексте).

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

Например языки (любые, как средства общения) постоянно эволюционируют. В силу этого меняется написание слов, их значение, их применение и пр.. Введение неких стандартов (правила языка) частично решает проблему. Но так как в язык постоянно вводятся новые понятия, слова нагружаются новыми смыслами, некоторые слова выходят из употребления, то в силу динамичности сами же стандарты языков вынуждены изменятся.

Даже если выбрать какой-то более оптимальный вариант (возможно привлекая некие технические инструменты), то далеко не всякая система поддастся изменению. Например когда-то пытались все привести к десятичной системе (например время), но это сделать не удалось (так и пользуемся 24 часа, 60 минут и секунд). Мер счисления несмотря на СИ до сих пор много в мире. Таким образом, если уже что-то возникло, и люди к этому привыкли, то изменить это очень сложно. Фактически получается, что больше предыдущий опыт управляет нами, нежели мы оптимизируем его, используя стандарты.

Гуманитарные задачи

Гуманитарными задачами являются: быстрое определение закономерностей; классификация неизвестной предметной области; сопровождение созданных больших систем; создание таких методик и систем, которые способны изменятся под новые факты. Здесь нет аксиом. Здесь все в любое время может изменится. Может появится что-то новое, а что-то уйти в небытие. Система обязана быть полной (описать нужно все, если что потребуется; а если не получается, то ввести новое понятие), но не обязана быть непротиворечивой (одна и та же фраза может быть понята по-разному, но если надо, то можно уточнить; в математике не может быть противоречивых утверждений, иначе она перестает работать на них).

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

Инженерная деятельность

Существует мнение, что для инженерной деятельности (и программирования в том числе) важны технические навыки и мышление. Есть другое мнение, которое говорит о том, что гуманитарная подготовка более важна. Как всегда — истина где-то рядом.

Если разработчик чувствует, что если сделать так, то будет плохо — это работа интуиции (гуманитарное мышление). Если делает выводы на основе железобетонных утверждений — то это логика (техническое мышление).

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

Но. Как только мы определяем утвержденные истины (данные там-то не пропадут; питание не пропадет в течение 10 минут после сигнала тревоги; если записано x=1, то после операции x будет равен 1; на диске есть свободное место в несколько килобайт всегда, …), и начинаем делать выводы от них, то мы решаем задачу технически (математически). У нас есть аксиомы, на основании которых можно делать выводы и писать надежные программы. Или создавать на их основе аппаратные или механические комплексы.

Создание языка (в т.ч. для программирования) — также по большей части гуманитарная задача. Нам нужно вводить новые термины, прибивать старые ненужные структуры, поддерживать нововведения, общаться с пользователями и пр..

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

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, итерационная разработка, способность к постоянному допиливанию и т.п..

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

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

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

Ковариантность и контравиантность

Понятия достаточно широкие, и соответственно могут использоваться как в математике, так и в физике, так и в computer science, так и при математическом доказательстве правильности программ (см. вики и wiki).

Обозначение

Если A ковариантен B, то это будем записывать как A cov B.

Если A контравариантен B, то это будем записывать как A contrav B.

Если A инвариантен B, то это будем записывать как A inv B.

Общее определение

A cov B тогда true, когда все что есть в B есть в A. Или более точно: условие A всегда захватывает B.

A contrav B тогда true, когда все что есть в A есть в B. Или более точно: условие B всегда захватывает A.

A inv B тогда true, когда все что есть в А есть в В, а также все что есть в B есть в A; или A cov B и при этом B cov A.

Примеры

Множества

{x,y,z} cov {x, y} = true

{x,y,z} cov {x, y, z} = true

{x,z} cov {x, y} = false

{x} cov {x, y} = false

{x} cov {} = true

{x} cov {x, y} = false

Типы

Пусть имеется иерархия наследования:

Здесь:

{инструмент} cov {отвертка} = true

{инструмент} cov {крестовая отвертка} = true

{инструмент} cov {отвертка; молоток} = true

{отвертка} cov {молоток} = false

{отвертка} cov {инструмент} = false

{отвертка;молоток} cov {инструмент} = false

Условия

{x > 0} cov {x > 1} = true

{x > 0} cov {false} = true

{x > 0} cov {true} = false

{x > 0} cov {x > 0 and y > 0} = true

{x > 0} cov {x > 0 or y > 0} = false

{x > 0 and y > 0} cov {x > 0} = false

{x > 0 and y > 0} cov {x > 1} = false

Применение

LSP

См. LSP

Пусть имеется базовый тип A и его подтип B.

Для них необходимо, чтобы для любой функции

type1
func( type2 value );

выполнялось:

A::type1 cov B::type1

A::type2 contrav B::type2

Т.е. например можно так:

class A {
    float
    func( double x );
};
 
class B: public A {
    double
    func( float x );
};

Но нельзя так:

class A {
    float
    func( double x );
};
 
class B: public A {
    double
    func( float x );
};

Если для функции существует любое предусловие pred и любое постусловие post, то необходимо, чтобы выполнялось 

A::pred contrav B::pred

A::post cov B::post

Например:

1. Имеется предусловие перед созданием объекта A о необходимости открытого файла f. Тогда в предусловии создания объекта B этот файл может быть как открыт, так и нет.
2. Имеется постусловие после выхода из полиморфной функции объекта A - внутренняя функция Release() должна быть вызвана. Соответственно, в этой же функции в объекте B внутренняя функция Release() также должна быть вызвана.

Изменение условий вывода при доказательстве правильности

Если рассматривается программа в виде троек Хоара

{P} C {Q}

то при движении в прямом направлении можно усиливать условия. Т.е. должно выполнятся Q_old cov Q_new.

Соответственно при движении в обратном направлении должно выполняться  P_old contrav P_new.

Например имеем программу и предусловие:

{x > 0}
x = x + 1;

Для неё постусловие есть {x > 1}. Но чтобы сказать, что {x > 0} возможно будет достаточно доказательства что {x > 2}.

И для постусловия:

x = x + 1;
{x > 0}

Здесь предусловием будет {x > -1}. Но данное предусловие можно усилить. Т.е. если мы докажем, что {x > 0}, то это также будет доказывать, что {x > 0} после инкремента.

Рафинирование