Здравствуйте, TimurSPB, Вы писали:
G>>И у валидного внутреннего состояния всегда есть инварианты. TSP>Только определить эти инварианты не всегда так просто.
В догонку — вот тебе пример реального инварианта на состояние. Те, кто сталкивался с биржевыми приложениями — поймут, что это такое.
int open, high, low, close;
always( low <= open <= high );
always( low <= close <= high );
И подобных инвариантов в реальных программах дофига. Они как слышатся, так и пишутся, нет совершенно никаких проблем их "определять". Это в действительности очень просто.
Все дело в том, что для того, чтобы пользоваться техникой, или хотя-бы понимать, о чем идет разговор — надо ее знать и уметь. И изучать ее по постам РСДН — не лучший способ.
G>int open, high, low, close; G>always( low <= open <= high ); G>always( low <= close <= high );
Для полноты картины приведи доказательство, что этих инвариантов достаточно, что бы утверждать о правильности работы кода.
P.S. а точно "int open ...", может float или double все таки?
Здравствуйте, TimurSPB, Вы писали:
G>>int open, high, low, close; G>>always( low <= open <= high ); G>>always( low <= close <= high );
TSP>Для полноты картины приведи доказательство, что этих инвариантов достаточно, что бы утверждать о правильности работы кода.
А что, я где-то говорил, что их будет достаточно? Или я говорил, что у каждой функции будут свои предусловия и постусловия?
Приведенный инвариант касается только самих данных, и от функций обработки никак не зависит.
TSP>P.S. а точно "int open ...", может float или double все таки?
Может быть и так, и так. По своей природе — котировка это fixed point, а не double. И это удобно для целей сериализации — сетевого слоя и слоя хранения.
А вот когда накладывают индикаторы и считают аналитику — оперируют, естественно, double-ами.
Если бы я использовал double, мне пришлось бы закрыться при сравнении эпсилонами. Ничего по сути это бы не добавило, и для примера — излишне.
TSP>>Для полноты картины приведи доказательство, что этих инвариантов достаточно, что бы утверждать о правильности работы кода. G>А что, я где-то говорил, что их будет достаточно? Или я говорил, что у каждой функции будут свои предусловия и постусловия? G>Приведенный инвариант касается только самих данных, и от функций обработки никак не зависит.
Приведенный инвариант можно легко увидеть на экране при построении графика. И поймать в дебагере его очень легко.
TSP>>P.S. а точно "int open ...", может float или double все таки? G>Может быть и так, и так. По своей природе — котировка это fixed point, а не double. И это удобно для целей сериализации — сетевого слоя и слоя хранения.
Может быть и так и этак. В общем это та самая "понеслась..."
Я вот котировки только в телевизоре видел, но сразу заподозрил неладное. А ведь в финансах это тонкий вопрос. Да и округления там специфичные и очень значимые для дела.
Вообще дискуссии о формальных методах носят весьма холиварный характер. Я за развитие в этом направлении, но без фанатизма.
Здравствуйте, TimurSPB, Вы писали: G>>А что, я где-то говорил, что их будет достаточно? Или я говорил, что у каждой функции будут свои предусловия и постусловия? G>>Приведенный инвариант касается только самих данных, и от функций обработки никак не зависит. TSP>Приведенный инвариант можно легко увидеть на экране при построении графика. И поймать в дебагере его очень легко.
Ты сомневаешься в существовании инвариантов, которые не так легко увидеть на экране, и поймать в дебаггере, или что?
Привести примеры? Вот я беру — и не вывожу на экран эти самые OHLC бары, а использую их, допустим, в оптимизаторе торговых роботов. Где на них считаются сложные сигналы, которые потом черт знает во что превращаются. И что тогда?
Или, например, последний "бар" постоянно обновляется из потока котировок — раз 20 в секунду. Я что, 24 часа в сутки следить должен — не взглючнет-ли? А может быть, я лучше робота посажу за этим следить? И, может быть, это у меня будет не единственный инвариант в системе? И кроме инвариантов, еще, может, таки будут пред-пост-условия на функциях?
Которые, кроме прочего, увеличивают читаемость кода, являясь конструктивными комментариями к нему.
TSP>>>P.S. а точно "int open ...", может float или double все таки? G>>Может быть и так, и так. По своей природе — котировка это fixed point, а не double. И это удобно для целей сериализации — сетевого слоя и слоя хранения. TSP>Может быть и так и этак. В общем это та самая "понеслась..."
Я вот котировки только в телевизоре видел, но сразу заподозрил неладное. А ведь в финансах это тонкий вопрос. Да и округления там специфичные и очень значимые для дела.
И совершенно напрасно заподозрил. Человеку, 6 лет отработавшему в CQG Int., ты можешь доверять. Особенно, если этот человек был тимлидом группы разработки сервера, который эти бары строит. Все под контролем, я не понаслышке знаю, насколько это тонкий вопрос, и тебя не обману.
Чтобы не ошибиться в столь тонком вопросе — там архитектура "слоеная", и в каждом слое применяется свой тип цены. Не нарушая NDA, могу тебе сообщить, что вообще — их три. Raw Price (int), Correct Price (double), и Display Price (сложная штука внутри, снаружи чаще всего видна как обычный int).
А с округлениями там ничего специфического нет — все по граждански.
TSP>Вообще дискуссии о формальных методах носят весьма холиварный характер. Я за развитие в этом направлении, но без фанатизма.
Ну, и я тоже за развитие, и тоже без фанатизма. Выходит, мы на одной стороне?
Еще пример дам. Про пред-пост-условие. Чтоб ничего кроме РСДН не читать, и все понять .
Смори. Определяем функцию, которая добавляет к существующему OHLC бару одну котировку.
OHLC & append_quote( int i_price );
pre: i_price > 0
post: high >= i_price, low <= i_price, close == i_price
Понятно, что она не полна. Она не защищает от того, что ты ВНЕЗАПНО max_int впишешь в high, например.
Но она уже дает некоторое понимание, что функция делает, не так-ли? Напоминая читателю о ряде закономерностей, которые система при исполнении проверит. Что такое формальные спецификации? То, что очевидно, и то, в чем ты думаешь, что ты уверен. Оно так часто на практике не так оказывается.
На практике — надо подходить без фанатизма. И такой подход дохрена багов на практике ловит. Ибо код — тоже по сути своей спецификация, тока — исполняемая.
И тогда — будет щастье. Пардон — заметное сокращение затрат на локализацию багов.
Формальные спецификации можно понимать, как перенос проверок юнит-тестов в сам код. Это хорошее, правильное понимание. Сильно снижающее трудозатраты.
Здравствуйте, Gaperton, Вы писали:
G>OHLC & append_quote( int i_price ); G>pre: i_price > 0 G>post: high >= i_price, low <= i_price, close == i_price
Кстати, у меня эти инварианты однажды сломались, что взорвало нам мозг. Цена оказалась таки отрицательная.
Когда мы спросили у трейдеров, может ли цена быть отрицательная — они сказали — нет. Но она была.
Так мы узнали про так называемые "сплиты". Когда довыпуск акций делается, предыдущие цены корректируются вниз. И — благодаря колебаниям, такое таки возможно, что на гражданском графике котирововок акций, цена уползет в минус.
Это произошло в нашем тесте внезапно, на акциях ZRAN (Zoran Corp., http://www.zoran.com/).
Вот так. Формальный спек — это твое представление о требованиях. Оно может столкнутся с реальностью, и тебе сильно повезет, если ты это представление выразил в терминах формального спека. Съэкономишь массу времени.
Здравствуйте, Gaperton, Вы писали:
G>y = sqrt( x ); G>спецификация: для всех x > 0 и наперед заданного eps > 0, всегда верно | y^2 — x | < eps.
G>Независимо от вида и размера алгоритма вычисления корня — спецификация настолько полна, что враг не пройдет. Никак.
очень характерный момент... Вы уверены в том, что спецификация полная, а между тем, случай x==0 благополучно пропущен
Здравствуйте, vitasR, Вы писали:
R>Здравствуйте, Gaperton, Вы писали:
G>>y = sqrt( x ); G>>спецификация: для всех x > 0 и наперед заданного eps > 0, всегда верно | y^2 — x | < eps.
G>>Независимо от вида и размера алгоритма вычисления корня — спецификация настолько полна, что враг не пройдет. Никак.
R>очень характерный момент... Вы уверены в том, что спецификация полная, а между тем, случай x==0 благополучно пропущен
В каком месте он упущен? Для его решения не будет соблюдаться спецификация?
Здравствуйте, vitasR, Вы писали:
G>>y = sqrt( x ); G>>спецификация: для всех x > 0 и наперед заданного eps > 0, всегда верно | y^2 — x | < eps.
G>>Независимо от вида и размера алгоритма вычисления корня — спецификация настолько полна, что враг не пройдет. Никак.
R>очень характерный момент... Вы уверены в том, что спецификация полная, а между тем, случай x==0 благополучно пропущен
Действительно, очень характерный момент.
Вы действительно так сильно уверены в том, что работая с плавающей запятой, вы можете вот так запросто сравнивать числа на равенство, в том числе с нулем, да?
Здравствуйте, Курилка, Вы писали:
К>В каком месте он упущен? Для его решения не будет соблюдаться спецификация?
Ну, строго говоря, там у меня предусловие x > 0, захватывающее машынный ноль только с одного конца.
Но если совсем правильно вводить ноль (на что я для целей иллюстрации забил) — надо еще отрицательную окрестность ноля в спецификацию ввести. Ибо оный ноль может являться результатом вычислений, и строго говоря быть не равным ноль.
Есть еще один способ писать спецификации, в котором нет предусловий, и полагается полностью расписывать постусловие функции для всего пространства аргументов. При его использовании таких вопросов не возникает, ибо граничные условия всегда гарантированно явно прописаны. То есть, для квадратного корня, это может выгрядеть, например, вот так:
-infinity < x <= -epsilon; y == nan
-epsilon < x <= epsilon; y == 0
epsilon < x < infinity; | y^2 — x | < epsilon
Возможны, собственно, разные варианты требований к точности, машинным нулям, и обработке исключительных ситуаций.
Именно такой способ крайне рекомендуется при составлении спецификаций для существующего кода. Зачастую, без выписывания такой спецификации "отрефакторить" легаси-код невозможно. Обычная проблема фрагментарного рефакторинга сложного легаси-кода — неявно заданное и нецелостное поведение этого кода в граничных ситуациях, и такие же неявные закладки на оное поведение в стопицот местах этого кода. На что быстрый и ловкий новичок налетает, а потом удивляется — что это у него его правильный код нифига не работает.
Здравствуйте, Gaperton, Вы писали:
R>>очень характерный момент... Вы уверены в том, что спецификация полная, а между тем, случай x==0 благополучно пропущен
G>Действительно, очень характерный момент.
G>Вы действительно так сильно уверены в том, что работая с плавающей запятой, вы можете вот так запросто сравнивать числа на равенство, в том числе с нулем, да?
кстати да, уверен. с нулем — уверен. и если человек не по наслышке знает о проблемах сравнения чисел с плавающей точкой, то он должен это прекрасно понимать
это во2ых. а во1ых, где в моем посте предлагается СРАВНИВАТЬ с нулем?
Вы утверждали, дословно, "спецификация настолько полна, что враг не пройдет. Никак."
при этом упустили важный частный случай.
Здравствуйте, Aleх, Вы писали:
A>Итак, на вопрос, что такое баг распространен следующий ответ. Баг — это несоответствие программы спецификации.
Заменяем слово "спецификации" на "ожиданиям пользователя" и получаем правильное и понятное определение.
Ну, и соответственно все твои слова становятся неверными, так как сужают понятие бага.
Простой пример входящий за рамки твоей трактовки бага — пользователь послал документ на печать указав в настройках принтера двустороннюю печать, но документ напечатался только на одной стороне бумаги. Никаких:
— некорректный (несоответствующий архитектуре) машинный код — неизвестная комманда процессора.
— недопустимое значение операндов — обращение по нулевому адресу, деление на ноль.
— нарушение целостности данных — запись данных за пределы выделенной памяти и повреждение кучи, попытка чтения данных за пределом буфера вследствие его неверного размера.
— необрабатываемые исключения
— зацикливание алгоритма
— несоответствие различных частей программ — не соблюдается договоренность (контракт) по области значений передаваемых данных.
в программе не наблюдается. Баг проистекает из-за неверной логики работы программы (например, принудительного задания настроек печати).
То что ты описал — конечно тоже баги, но на них баги не заканчиваются. Так что исходное определение таки верно, а ты сужаешь понятие бага и потому делаешь не верные выводы.
Есть логика намерений и логика обстоятельств, последняя всегда сильнее.
Здравствуйте, vitasR, Вы писали:
G>>Вы действительно так сильно уверены в том, что работая с плавающей запятой, вы можете вот так запросто сравнивать числа на равенство, в том числе с нулем, да?
R>кстати да, уверен. с нулем — уверен. и если человек не по наслышке знает о проблемах сравнения чисел с плавающей точкой, то он должен это прекрасно понимать
И совершенно напрасно вы в этом уверены. Что должен понимать любой студент, который мало-мальски прилежно учился Computer Science.
R>это во2ых. а во1ых, где в моем посте предлагается СРАВНИВАТЬ с нулем?
Как где? Вот здесь: "случай x==0 благополучно пропущен"
"Случая х==0" в спецификациях на функции с плавучкой нет и быть не может. Окрестность задавать надо.
R>Вы утверждали, дословно, "спецификация настолько полна, что враг не пройдет. Никак." R>при этом упустили важный частный случай.
Ну, во-первых, вы очень сильно преувеличиваете его важность, ибо с практической точки зрения это полнейшая ерунда.
А во-вторых, — с кем не бывает, нет-нет да и пропустишь какую-нибудь мелочь.
Впрочем, с кем такого никогда не бывает — известно. Исключительно с теми, кто ничего не делает сами. Вот те никогда не ошибаются. Ибо не в чем.
Здравствуйте, Gaperton, Вы писали:
G>Есть еще один способ писать спецификации, в котором нет предусловий, и полагается полностью расписывать постусловие функции для всего пространства аргументов. При его использовании таких вопросов не возникает, ибо граничные условия всегда гарантированно явно прописаны. То есть, для квадратного корня, это может выгрядеть, например, вот так:
G>-infinity < x <= -epsilon; y == nan G>-epsilon < x <= epsilon; y == 0 G>epsilon < x < infinity; | y^2 — x | < epsilon
Еще к плюсам такого стиля стоит добавить легкость проверки на полноту охвата пространства аргументов. Потому как глядя на такой спек, сразу снимается вопрос — автор забыл про ряд вариантов сочетаний входов, или написал такой спек специально. Данная проверка выполняется на "detailed design review".
Ну и конечно, для разделяемого кода подобные спеки весьма желательно писать, если хочется, чтобы система со временем не превратилась в кусок говна.
Еще — такой код очень легко и приятно накрывать white-box тестами.
Во-первых, всякую ерунду проверять нет никакой надобности — она записана в постусловиях. Можно проверять тонкие вещи, сразу концентрируясь на более сложных сценариях использования кода. И тест сразу станет выглядеть более компактно и осмысленно. Простые вещи сами проверятся — главное воздействие подать.
Во-вторых, глядя на спеку, сразу видны все граничные условия, и сочетания вариантов значений аргументов. Что сильно помогает при написании теста, да и просто при чтении кода.
И в третьих, благодаря тому, что проверки перенесены в код, суперпозиция проверок при вызове из разных мест слоеного кода получается автоматически. То есть, тесты кода более высокого уровня все равно будут проверять код низкого уровня, теми же самыми проверками.
Именно поэтому и не обязательно гнаться за полнотой постусловий и тестового покрытия — гораздо выгоднее сохранять их простыми и очевидными (чтоб помогали читать код), и при этом увеличить покрытие спеками по функциям.
Такой подход позволяет помимо прочего сильно сократить объем и требования к покрытию юнит-тестов. Можно даже вообще забить на юнит-тесты, ограничившись хорошим общестистемным, и не ощутить от этого особых потерь. Данная техника сильно расслабляет, да. Потому, что дофига чего ловит.
Здравствуйте, Gaperton, Вы писали:
G>Здравствуйте, Gaperton, Вы писали:
G>>Есть еще один способ писать спецификации, в котором нет предусловий, и полагается полностью расписывать постусловие функции для всего пространства аргументов. При его использовании таких вопросов не возникает, ибо граничные условия всегда гарантированно явно прописаны. То есть, для квадратного корня, это может выгрядеть, например, вот так:
G>>-infinity < x <= -epsilon; y == nan G>>-epsilon < x <= epsilon; y == 0 G>>epsilon < x < infinity; | y^2 — x | < epsilon
... G>Короче, рекомендую.
Я в принципе за но просто пытаюсь донести мысль что объем этих проверок таки зависит от количества комбинаций функция-состояние. И прекрасные все более надежные методики проектирования и языки программирования все более красивым и надежным образом считают сумму 2х чисел или на крайняк факториал. Тут народ пытался это высказать по простому и их не услышали.
более того мне как автору алгоритма решения задачи внешняя спека описывающая все состояния ну совсем не нужна. По хорошему в вакууме программисты сами пишут спеки описывающие все состояния и обновляют их при каждом чихе, на деле это будет как программами у шаттлов сотни человек пишут программу на 250 тыс строк десятилетиями. Разумеется вопрос в качестве/стоимости тестирования но балансом управляют pointy-haired bosses...
Так что я с интересом читаю про то как гдето хорошо и продолжаю лопатить дальше
ps лично я стараюсь делать/оставлять в коде возможность врубить все параноидальные проверки а-ля цена не меньше нуля, но мне это дорого стоит
но просто пытаюсь донести мысль что объем этих проверок таки зависит от количества комбинаций функция-состояние. И прекрасные все более надежные методики проектирования и языки программирования все более красивым и надежным образом считают сумму 2х чисел или на крайняк факториал. Тут народ пытался это высказать по простому и их не услышали.
