Skip to content

code

Правильность программы

«Тестирование программ может служить для доказательства наличия ошибок, но никогда не докажет их отсутствия!»

— Edsger W. Dijkstra

Введение

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

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

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

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

В этой статье изучим классические работы Edsger W. Dijkstra, Niklaus Wirth и Harlan D. Mills, заложившие математические основы верификации программ. Эти принципы остаются актуальными и сегодня — они лежат в основе Domain-Driven Design, Type-Driven Development и контрактного программирования.

Модульность программы

«Всё не так легко, как кажется...»

— Закон Мерфи

Введение

Здоровый интерес к структурному программированию может быть как проявлением постепенного осознания правоты Мерфи, так и наступлением определенной зрелости в вычислительном деле. Структурное программирование возникло именно из-за того, что «все сложно, тянется дольше и стоит дороже, чем ожидалось». Нисходящая разработка призвана уменьшить сложность программы и дать возможность закончить ее вовремя. Если «что-то портится», то предлагаются средства, которые помогают обнаружить такие места как можно раньше и оставить достаточно времени на их устранение.

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

Структурирование программ

Программы не люди, а ошибки не микробы программа не может нахвататься ошибок, общаясь с другими дефектными программами. Ошибки всегда допускают программисты.

— Харлан Милла (Harlan Mills)

Введение

По-моему, программирование с изначальными тестами — одна из самых эффективных методик разработки ПО, возникших в 90-х. Но это не панацея, потому что такой подход тоже страдает от общих ограничений тестирования (описаны ниже), выполняемого разработчиками. Что мы сделаем — рассмотрим доказательства правильности программ от отцов-основателей из IBM и других авторов, которые описывали структурное программирование в (70,80)-х годах. Увидим, что надежное ПО — это хорошо спроектированное ПО.

Хорошо спроектированное ПО — это правильно структурированное ПО.

Правильно структурированное ПО — ПО, модули (классы) которого отвечают требованиям (описаны в Характеристики Модулей).

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

Эксперимент с ИИ-ассистентом: бег от Pact в сторону валидации AsyncAPI 3.0 спецификаций

ai-contract-tests-experiment.png

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

1973 Никлаус Вирт. Systematic Programming. An introduction.

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

Я с большим энтузиазмом смотрю на прогресс ИИ-ассистентов, провожу эксперименты с передовыми их проявлениями(по крайней мере известными и доступными мне), такими как Claude терминал, Cursor.

Один из наиболее влиятельных сторонников структурного программирования профессор Э. В. Дейкстра написал

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

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

В данной работе я кратко опишу процесс по созданию утилиты на Golang с ИИ-агентом в клод-терминале для валидации контрактов сервисов в ландшафте информационных систем, где у каждого сервиса есть спецификация Async API 3.0.

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

Со-творчество с машиной

img

Дорогая, работа с AI-агентом превратила меня в супермена. Или супер-мема — сейчас это почти одно и то же.

Я учусь и создаю автоматизацию в разы быстрее. Это новый темп, новый стиль работы.

Помнишь «Джонни-мнемоника»? Как главный герой перевозил информацию в чипе, встроенном в череп? История материализовалась. До нас доходят фрагменты через текстовые каналы.

Где-то китайские специалисты везут 50 ТБ обученных моделей в самолёте из стран с более свободным интернетом. В неоновых лучах Токио якудза с лазерной нитью крадёт первоклассный датасет сверхновой нейросети и перепродаёт через даркнет военным подрядчикам. Проклятая Арасака.

А я тут со своим Go и unit-тестами — как уличный самурай с клавиатурой вместо катаны.

В отражениях небоскрёбов мегаполиса стильные корпораты в дизайнерских костюмах везут обученные модели в гоночных суперкарах. Машина улучшает машину. Recursive enhancement. БУМ.

Я словно с вшитым нейроимплантом: расширенная память, ускоренное написание кода на максималках, прямая связь с матрицей целей. Мои синапсы работают в режиме overdrive.

Быстрее тестирую гипотезы, исследую новые направления. Это прорыв. Digital awakening.

Я не могу объяснить всё — слишком много переварить. Я на эмоциях.

Даже читаю больше и быстрее.

О важности коммуникации в IT: встреча со студентами Бауманки

img

Пообщался в Бауманке со студентами и рассказал им о сложностях коммуникации на работе. В конце было много интересных вопросов.

Казалось бы, у программистов работа про код: взял задачу — сиди, кайфуй, программируй. Но нет. Код - это только часть работы.

Код - побочный эффект коммуникации.

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

Мне нравится думать об этом через фразу:

Make me fucking care

Профессионал отличается от любителя тем, что умеет уточнять ожидания заказчика(руководителя) и понимает важность этого шага.
Не я как руководитель должен бегать за тобой, а ты должен быть заинтересован в результате и точности своей траектории. Это бизнес. И если ты лажаешь, то в следующий раз к тебе не придут за заказом.

Симбиоз с машиной при разработке. Компонентные тесты

Киберпространство в срезе кодописи изменяется стремительно.

Голюцинация: 

#gardener@core: закрываю глаза, обдумываю API компонента, проговариваю контекст, открываю глаза и вижу в git async api 3.0 спецификацию.
Я подключился к паре ИИ-имплантов в виде Claude и Cursor. VS Code в сочетании с cursor меня очень порадовал на практике. Возврат в IntelliJ IDEA теперь ощущается как деградация. Горячие клавиши, молниеносные переходы между кодом и терминалом, древо проекта слева — интерфейс стал продолжением нервной системы.

С машиной я взялся за старый учебный сервис.

Задача: вшить компонентные тесты в проект.

Loading CodeBook

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

Книга Кода — это кодекс для создания надежного киберпространства приложения кирпичик за кирпичиком.

Лови первый дроп - Оглавление.

Оглавление - моя карта, которая затянет тебя в киберпространство, где бизнес-процессы превращаются в понятные нарративы, а сложность растворяется в простоте решений. Это послание...

Погружение в киберпространство малыми итерациями начинается.

Dev2Dev https://codemonsters.team/codebook/

Пиши свои мысли в комментах.