JUG Ru Group corporate blog
High performance
Programming
Conferences
Distributed systems
Comments 29
+6

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

+2

Имхо, именно поэтому в первом абзаце очень чётко обозначено, что это статья не про то, как писать код — а про то, как понять — в чём проблема, как ты её собираешься решать. Спека, которую ты пишешь — это в первую очередь инструмент для обдумывания проблемы, а не способ написания конечной реализации.

+8

А это — не очевидные вещи?
Создание "спеки" на формализованном языке НИЧЕМ не отличается от "написания конечного кода".
Чтобы рассуждать (правильно рассуждать), нужно хорошо владеть любым формальным языком — будь то язык алгебры или язык программирования.
Иногда полезно иметь "промежуточный" язык и писать на нём рассуждения. А иногда от этого больше вреда, чем пользы.

+6

У вас на работе принята практика написания формальных спецификаций с помощью TLA+ или подобного? Вы знаете хоть кого-нибудь, у кого в российском "кровавом энтерпрайзе" принято?


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

+3

Не пишут. Потому, что это не нужно.
Потому, что часто исходные задачи меняются быстрее, чем решаются.
Потому, что задачи такого уровня.
Тех, кому действительно нужен TLA, не нужно убеждать в том, что он нужен.
Что он из себя представляет?
Ещё один "язык высокого уровня".
Очередной "суржик" для "недоменеджеров", нихрена не смыслящих ни в программировании, ни в предметной сфере, оправдывающий лишнее звено, лишний (в 99% случаев) "слой абстракции", пожирающий ресурсы разработки.
Посудите сами, если задача полность формализована в "спеках", то "кодер"=="ручной компилятор". А если "спеки" "недоформализованы", то это фуфло, а не спеки.
А теперь объясните смысл этой работы.
Как в примерах от автора M и N переименовать в х и у?
Это, блин, что за "программисты", для которых открытие века — необходимость думать и формализовать задачи? И кто они, если им для "подумать" нужен "специальный язык"?

+1

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


то "кодер"=="ручной компилятор".

Очень хороший ручной компилятор. Намного, намного более лучший, чем просто компилятор.


Например, есть какие-то хорошо изученные темы вроде того, как по грамматике языка сгенерировать парсер. Но парсер, написанный человеком вручную почти всегда будет лучше. Не стоит недооценивать человеков :)

+2

Хм…
Мне на почту прилетел несколько иной текст ответа.
Чтобы не было недопонимания, коротко отвечу по нему.
Так вот, я не оспариваю то, что пишет Лэмпорт в отношении "надо думать". А ещё он пишет абсолютно верную вещь, что "думать" можно на любом языке — хоть на китайском. И предлагает ОДНО ИЗ ВОЗМОЖНЫХ решений для "думать".
Я против того, чтобы это решение приподносилось как "золотая пуля" или "мастхэв" на все случаи жизни. Такое "понимание" написанного им — это и есть отрицание главного его посыла "думать надо", и пример абсолютного "клипового мышления".
Если "зомби" заставить "писать спеки", то получится "зомби, пишущий спеки".
Про "задача, возникает при написании спеков" — Вам правильно задали ниже вопрос.
А надо ли писать "спеки на спеки"? Ведь, тогда "постановку задачи" можно ещё дальше отодвинуть.
Или можно "просто думать, прежде, чем кодить"?

+1

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


Дальше возникает вопрос: что такое постановка задачи? Допустим, если к вам приходит заказчик и говорит: вы делали мне электронный магазин еды, я хочу чтобы кнопочка "купить пожрать" теперь вела сразу на покупку, а не на корзину. Это простая, интуитивно понятная задача. Иначе говоря, с постановкой задачи справилась интуиция. (Причем совершенно не факт, что справилась правильно).


А есть какие-то другие задачи, про которые непонятно даже, в чем задача, и есть ли она здесь. А если есть — нет ни одной идеи, как ее можно решить. Может быть окажется, что чтобы только понять проблему нужно полгода времени десяти профессоров. А потом окажется, что спека есть, а решения не существует в принципе, как вам такое.


Второй вопрос, что в общем случае спека описывает не решение, а класс решений. Например, есть спецификация языка и виртуальной машины Java. А реализаций у них написана куча. Без спеки ничего такого бы не было. Причем в спеке есть такие моменты (например, вся фигня про модель памяти, многопоточность, итп), которые до конца понимают три с половиной землекопа в мире.


Мир очень разнообразная штука. Не нужно вам конкретно думать над спекой — ну не думайте, в чем проблема-то, move along citizen

+3
Я начинающий любитель, и информации о проектировании программ очень много, с математикой в этом разделе вообще встречаюсь впервые, так что хотелось бы узнать где прочитать что-то фундаментальное. Непонятно с чего начинать — псевдокода или математики или чего-то еще.
+1
Начинающему любителю лучше избегать подобных тем, как черту — ладана. Это не фундаментальное, и никак не поможет вам лучше проектировать.
+6
Не понял как сделать так чтобы коллеги перестали быть зомби, а то запарился за них думать уже.
+4
Вот вот… первые абзацы очень в точку… а после видимо придется им оставаться зомбями
+5
Нужно ли писать спецификации на сложные спецификации?
+1
Для крупных проектов есть вики и jira, для средних достаточно комментариев. Да или нет?
Но, безусловно, польза от продумывания задачи перед решением огромная.
+3
Я внимательно на TLA+ не смотрел и вообще первый раз про него слышу. Но, чем это отличается от обычных юнит-тестов? Тест же тоже по сути является спецификацией тестируемого кода. И с теми же проблемами — не все можно описать. Попробуй вот написать тест, который проверяет освобождение памяти или закрытие ресурса А еще в кровавом энтерпрайзе есть JBehave например, который позволяет описывать бизнес-задачу на формальном языке.
P.S. Насколько я понял, основная мысль статьи — сначала думай, потом пиши код. А чтобы убедиться, что действительно подумал — записывай.
0
TLA+ решает конкретную задачу — написание формальных спецификаций для распределенных систем. Юнит-тесты проверяют корректность отдельных модулей исходного текста программы. Между юнит-тестами и TLA+ нет абсолютно никакой связи, разве только то, что и то и другое повышают качество программной системы.
+1
Если честно пользы увидел мало (ну либо нужно переворить все в голове).
Настоящие ведь проблемы возникают в формальной спецификации сложной предметной области.
+1
А что делать тем, для кого самый удобный язык описания спецификаций — это их язык программирования? Лично я полностью согласен, что прежде чем что-то делать — нужно думать, но мне удобнее всего записывать мысли непосредственно в код. Как и читать. Ну и каждая абстрактная спецификация требует кучи ресурсов на поддержание актуальности, по сути эти затраты ничем не отличаются от непосредственного внесения изменений в код, только добавляют необходимость переключения между форматами изложения…
+1
Наверняка вы сталкивались с тем, что когда вроде осознаешь задачу, пишешь код — а он раз и работает, мозг выдает награду — молодец и вы радостно переключаетесь на следующую/идете пить пиво. Но вот автор предполагает(и лично мой опыт говорит — он прав), что в таком случае вероятность появления багов в таком случае выше, чем если бы вы сначала написали «спецификацию». В общем-то, ИМХО, тоже самое, что и TDD, где слово тест заменяем на «спецификация».
Например, в порыве возникшего в голове алгоритма легко забыть про то же целочисленное переполнение, что может быть фатально, если мы деньги считаем или там мощность рентгена.
P.S. Если olegchir спросит автора, в чем же отличие авторского TLA+ от unit tests и напишет ответ сюда, то мы скажем спасибо.
+1

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


Например, можно было бы посчитать, что действительно, TLA+ — это что-то типа продвинутого фаззера. Но фаззеру для работы нужно запустить программу множество раз, а проверяльщику модели — не нужно запускать ни разу. Он не запускает, а только проверяет. Что позволяет ему проверить бесконечное количетство запусков с бесконечным количеством шагов в каждом из них.


К примеру, в Amazon DynamoDB, TLA+ позволила обнаружить такие баги, которые требовали 35+ шагов для их воспроизведения — для этого пришлось написать спеку примерно на 1000 строк в TLA+.


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


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

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


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

Вот тут можно подробнее почитать про верификацию и спецификации —
www.hillelwayne.com/post/why-dont-people-use-formal-methods
0
Статья «За все хорошее против всего плохого». Ни одного внятного примера спецификаций не приведено.
Здесь ничего не понятно. Я тоже могу сказать: чтобы стать чемпионом, тренируйтесь. Но чемпионом Вы не станете, даже если будете упахиваться на тренировках. Чтобы стать чемпионом, Вас должен тренировать чемпион, а не лузер вроде меня. И мастерство, которое тренер может показать, гораздо важнее физических нагрузок и мотивации в стиле «давай-давай, думай, пиши спецификацию». Мастерства в статье и нет. Статья ни о чем. В раздел «мотивация» ее нужно отправить.
Заминусуют — ну и плевать.
+1
Как мне кажется путь программиста — это путь познания, всегда и везде. Т.е. ты идешь по улице видишь, что на противоположной стороне перекрестка загорелся зеленый для пешеходов, а на твоей стороне нет, либо светофор горел слишком долго, и ты думаешь почему именно так, а не иначе. Нужно быть любознательным, без любознательности можно застрять на одном месте и ты не сможешь себя назвать настоящим программистом.
0
думать надо не перед тем как кодить, а перед тем как начать решать задачу, например это можно на уровне спеки начать делать, когда решаються задачи бизнеса, дальше когда программист будет кодить он уже будет решать задачи программистские и всем будет хорошо.
Но везде где я работал, все пытаются спихнуть задачи бизнеса на программистов тоже, а спека получалась не спекой, а описанием бизнеса, не более.
0
Как все можно превратить в такую тягомотину, предварительно написав «Приятного чтения!»?
Пойду, наверное, убиваться об стенку. Ведь я недопрограммист, судя по заявленному я, получается, один из «нелюбителей тестировать написанное».
Или, все-же, тестировать «написанное» должен автор?
Only those users with full accounts are able to leave comments. , please.