я заметил, что существует некоторое недопонимание того, что такое баги, почему их стоит рассматривать так или иначе, и что дает верификация программ. Хотя, казалось бы, всё элементарно.
Итак, на вопрос, что такое баг распространен следующий ответ. Баг — это несоответствие программы спецификации. Существуют ли в реальном мире такие спецификации, которые формально описывают то, что делает программа? Очевидно, если же представить себе такую спецификацию, то она будет сопоставима по объему содержащей в себе информации с объемом самой программы. Между ними будет лишь то отличие, что программа будет содержать в себе некоторые детали реализации, относящиеся к взаимодействию программы с платформой, на которой она будет выполняться.
Спецификации такого размера никто, разумеется, писать никогда не будет. К тому же в самой спецификации могут содержаться ошибки.
Поэтому, я считаю данное определение слова баг полностью бесполезным. То есть "программа содержит баг" объективно не значит ничего.
Если посмотреть на большинство программ, содежащих баги (хотя это в некоторой степени зависит от предметной области), проблемы возникают не с тем, что программы выдают неправильный результат (работают не по спецификации), а в том, что они просто его не выдают. Вылетают с ошибкой Acsess Violation или, если язык поддерживает исключения, Unhandled Exception.
Поэтому стоит рассматривать баги, связанные с банальной корректностью программ с точки зрения вычислителя (ЭВМ) и среды (Операционной системы). Количество правил, которым должна удовлетворять программа в большинстве случаев фиксированно и известно.
В качестве примеров можно привести следующие Баги:
— некорректный (несоответствующий архитектуре) машинный код — неизвестная комманда процессора.
— недопустимое значение операндов — обращение по нулевому адресу, деление на ноль.
— нарушение целостности данных — запись данных за пределы выделенной памяти и повреждение кучи, попытка чтения данных за пределом буфера вследствие его неверного размера.
— необрабатываемые исключения
— зацикливание алгоритма
— несоответствие различных частей программ — не соблюдается договоренность (контракт) по области значений передаваемых данных.
На пути развития языков программирования с некоторыми багами научились бороться.
Изобретение языка ассемблера позволило писать код содрежащий только поддерживаемые процессором комманды. В общем случае это именно так, несмотря на то что всё равно существует способ подсунуть процессору черти что.
Изобретение Языка более высокого уровня (Си) позволило сокртаить количество багов, связанных с некорректными условными и безусловными переходами.
Языки с автоматическим управлением памяти и отсутствием указателей с арифметикой позволии избавиться от ошибок обращения по недопутимому адресу и порчи памяти.
На данный момент существуют такие инструменты для программирования, которые позволяют значительно сократить количество багов. От всех багов избавиться вряд ли получитсья.
Верификация программ направлена на значительное сокращение багов, путем проверки отсутствия определенных их классов без выполнения программы.
В современном понимании, я думаю, под ней в основном стоит понимать проверку на выполнение договоренностей (контрактов) по области значения данных.
Как раз для этого и было предложено использовать зависимые типы, поскольку описывая тип, можно наложить ограничения на значения данных (тип зависит от значения <=> установленно взаимооднозначное соответствие между типами и областями значений), которые будут иметь этот тип и тем самым перелодижить проблему соответствий областей значения данных на систему типов.
Интересно, почему в таком случае зависимые типы не пришли в мейнстрим (или пока не пришли), как это произошло, например, с автоматическим управлением памяти и сборкой мусора?
ИМХО существуют некоторые проблемы с реализацией языков программирования, поддерживающих зависимые типы, которые бы позволяли компилировать эффективный код. Например, возникает следующая проблема (я не знаю, решаема она или нет. Если да, то как?). Использование при программировании встроенных типов данных, хорошо поддерживаемых платформой (int, double, массивы). Насколько мы все знаем, в языках не поддреживающих массивы, имеются большие проблемы с производительностью (пример: хеш-таблица на хаскелле).
Как в том случае, если типы встроены в язык и их определение неизвестно, конструктивно описывать и доказывать их свойства?
я заметил, что существует некоторое недопонимание того, что такое баги, почему их стоит рассматривать так или иначе, и что дает верификация программ. Хотя, казалось бы, всё элементарно.
Что-то мне Ваша элементарность не нравится.
A>Итак, на вопрос, что такое баг распространен следующий ответ. Баг — это несоответствие программы спецификации. Существуют ли в реальном мире такие спецификации, которые формально описывают то, что делает программа? Очевидно, если же представить себе такую спецификацию, то она будет сопоставима по объему содержащей в себе информации с объемом самой программы.
Грубо неверно. Потому что смешиваются совершенно разные вещи — _что_ делает программа и _как_ она это делает. Описание, что делает, может быть кратким, но реализация — очень сложной. Видимо, Вы мало сталкивались со сложными алгоритмами. Простейшая постановка задачи (например, решить систему линейных уравнений, или раскрасить карту) может давать очень сложную реализацию (для СЛАУ — поиск варианта решения без промежуточных вырождающихся детерминантов, для раскраски в 4 краски — перебор с возвратами и отбор типичных ситуаций). Сортировка (спецификация которой очень проста) даёт спектр реализаций от десяти строк до тысяч строк (внешняя со сложными схемами слияния). И так далее.
Разумеется, если Вы работаете в области, например, пользовательского интерфейса для делового кода (склад, продажа) — там спецификация будет в разы толще итогового кода, потому что на длинное описание требований к элементу интерфейса в результате будет его название и несколько чисел (грубо говоря).
A>Спецификации такого размера никто, разумеется, писать никогда не будет. К тому же в самой спецификации могут содержаться ошибки.
Может. Спецификации тоже проверяются.
A>Поэтому, я считаю данное определение слова баг полностью бесполезным. То есть "программа содержит баг" объективно не значит ничего.
Нет, оно может содержать — и очень часто содержит — совершенно объективные утверждения.
Если при 0,1,2 на входе на выходе должно быть 2,1,0, а программа даёт 2,0,1 — это баг.
A>Если посмотреть на большинство программ, содежащих баги (хотя это в некоторой степени зависит от предметной области), проблемы возникают не с тем, что программы выдают неправильный результат (работают не по спецификации), а в том, что они просто его не выдают. Вылетают с ошибкой Acsess Violation или, если язык поддерживает исключения, Unhandled Exception.
Да, отказ от ответа — тоже баг.
A>В качестве примеров можно привести следующие Баги: A>- некорректный (несоответствующий архитектуре) машинный код — неизвестная комманда процессора.
Страшная редкость в наше время.
[skip]
A>Верификация программ направлена на значительное сокращение багов, путем проверки отсутствия определенных их классов без выполнения программы. A>В современном понимании, я думаю, под ней в основном стоит понимать проверку на выполнение договоренностей (контрактов) по области значения данных.
A>Как раз для этого и было предложено использовать зависимые типы, поскольку описывая тип, можно наложить ограничения на значения данных (тип зависит от значения <=> установленно взаимооднозначное соответствие между типами и областями значений), которые будут иметь этот тип и тем самым перелодижить проблему соответствий областей значения данных на систему типов.
A>Интересно, почему в таком случае зависимые типы не пришли в мейнстрим (или пока не пришли), как это произошло, например, с автоматическим управлением памяти и сборкой мусора?
Частично пришли. Но они помогают решить далеко не все проблемы. В численных расчётах они вообще ничем не помогут, только помешают. В интерфейсах — очень помогут.
Вообще непонятно, зачем вы связали вместе несколько совершенно разных проблем.
Здравствуйте, netch80, Вы писали:
N>Здравствуйте, Aleх, Вы писали:
N>Грубо неверно. Потому что смешиваются совершенно разные вещи — _что_ делает программа и _как_ она это делает. Описание, что делает, может быть кратким, но реализация — очень сложной. Видимо, Вы мало сталкивались со сложными алгоритмами. Простейшая постановка задачи (например, решить систему линейных уравнений, или раскрасить карту) может давать очень сложную реализацию (для СЛАУ — поиск варианта решения без промежуточных вырождающихся детерминантов, для раскраски в 4 краски — перебор с возвратами и отбор типичных ситуаций). Сортировка (спецификация которой очень проста) даёт спектр реализаций от десяти строк до тысяч строк (внешняя со сложными схемами слияния). И так далее.
Описание может быть кратким, если оно не формальное и не описывает некоторые внешние особенности алгоритма, которые могут быть существенными (например такие, как верхняя оценка сложности, средняя, её дисперсия, использование памяти). Если же в сецификации задана только зависимость результата от входных данных, то алгоритм вообще говоря может быть любой — хоть переборный.
Да, действительно, я подразумеваю под спецификацией не только то, что делает программа, но так оно и есть, если посмотреть определение этого слова. Это просто набор требований, которым должна удовлетворять некоторая сущность (в данном случае программа).
Учитывая то что я имел ввиду формальные спецификации (то есть написанные на таком языке, который не дает возможность трактовать написанное по разному), они в самом деле не будут получаться краткими.
В примере с сортировками, если же просто указать то, что набор данных, получающихся в результате должен быть упорядочен, то сортировка пузырьком тоже будет удовлетворять требованиям спецификации + алгоритм будет коротким. Но скорее всего она не будет удовлетворять своей производительностью. Дополнив спецификацию путем ограничения алгоритмической сложности, получим ещё меньшее множетосво алгоритмов, удовлетворяющий ей. Одним из алгоритмов может быть быстрая сортировка. Но опять же размер алгоритма не сильно увеличился. Тысячи строк могут взяться тогда, когда в спецификации мы ещё сильнее ограничим сложность алгоритма + опишем области значений наиболее часто обрабатываемых данных (чтобы алгоритм в этих случаях возможно работал быстрее). Тогда алгоритм удовлетворяющий этим требованиям соединит в себе несколько различных методов сортировки. Но так же и размер спецификации значительно увеличится. Попробуйте описать все эти ограничения формально
N>Разумеется, если Вы работаете в области, например, пользовательского интерфейса для делового кода (склад, продажа) — там спецификация будет в разы толще итогового кода, потому что на длинное описание требований к элементу интерфейса в результате будет его название и несколько чисел (грубо говоря).
Это да.
N>Может. Спецификации тоже проверяются.
На непротиворечивость или как?
N>Нет, оно может содержать — и очень часто содержит — совершенно объективные утверждения. N>Если при 0,1,2 на входе на выходе должно быть 2,1,0, а программа даёт 2,0,1 — это баг.
Ну да, в данном случае, можно это легко описать. Но бывает описание оплучается сопоставимо по сложности с самим алгоритмом. Хотя, конечно от предметной области многое зависит.
N>Да, отказ от ответа — тоже баг.
На мой взгляд такие баги встречаются чаще всего и определяющим образом влияют на надежность программ.
Здравствуйте, Aleх, Вы писали:
A>ИМХО существуют некоторые проблемы с реализацией языков программирования, поддерживающих зависимые типы, которые бы позволяли компилировать эффективный код. Например, возникает следующая проблема (я не знаю, решаема она или нет. Если да, то как?). Использование при программировании встроенных типов данных, хорошо поддерживаемых платформой (int, double, массивы). Насколько мы все знаем, в языках не поддреживающих массивы, имеются большие проблемы с производительностью (пример: хеш-таблица на хаскелле).
Здравствуйте, Aleх, Вы писали:
A>Поэтому стоит рассматривать баги, связанные с банальной корректностью программ с точки зрения вычислителя (ЭВМ) и среды (Операционной системы). Количество правил, которым должна удовлетворять программа в большинстве случаев фиксированно и известно. A>В качестве примеров можно привести следующие Баги: A>- некорректный (несоответствующий архитектуре) машинный код — неизвестная комманда процессора.
Давай я немного усложню твою картину
Это не баг. Встречая такую ситуацию процессор понимает, что ничего не понимает, и спрашивает мнения вышестоящих по званию. Конкретно x86 вызывает шестое прерывание, обрабатываемое операционной системой. Что делает обрабочик прерывания? Это вопрос. Дефолтный ничего особо разумного, безидейно кинет исключение, а вот если у нас установлен специальный драйвер, то всё становится интереснее. Таким несложным образом может быть огранизован канал взаимодействия с драйвером, несколько в обход стандартных вызовов. Кажется, что-то такое было сделано в HASP -- была такая железка от компании Аладдин для лицензирования софта, цеплялась на LPT-порт.
Но и вообще, это открытый (хотя и кривоватый, и с плохими гарантиями совместимости) путь для расширения системы команд процессора, для эмуляции их операционной системой.
Баг -- не неизвестная процессору команда, баг -- использование неизвестной процессору команды не там, где надо
Здравствуйте, Aleх, Вы писали:
A>Итак, на вопрос, что такое баг распространен следующий ответ. Баг — это несоответствие программы спецификации. Существуют ли в реальном мире такие спецификации, которые формально описывают то, что делает программа? Очевидно, если же представить себе такую спецификацию, то она будет сопоставима по объему содержащей в себе информации с объемом самой программы. Между ними будет лишь то отличие, что программа будет содержать в себе некоторые детали реализации, относящиеся к взаимодействию программы с платформой, на которой она будет выполняться. A>Спецификации такого размера никто, разумеется, писать никогда не будет. К тому же в самой спецификации могут содержаться ошибки.
y = sqrt( x );
спецификация: для всех x > 0 и наперед заданного eps > 0, всегда верно | y^2 — x | < eps.
Независимо от вида и размера алгоритма вычисления корня — спецификация настолько полна, что враг не пройдет. Никак.
y = sort( x );
спецификация: для всех х таких, что len( х ) < 2 результат равен х; для других —
Для каждого i от 0 до ( len( x ) — 1 ) верно y[ i ] <= y[ i + 1 ]
То же самое. И тоже — абсолютно независимо от алгоритма сортировки.
И в обоих случаях размер спецификации никак не зависит от размера программы.
Что там у нас понятно насчет размера спецификации?
Здравствуйте, Gaperton, Вы писали:
G>y = sqrt( x ); G>спецификация: для всех x > 0 и наперед заданного eps > 0, всегда верно | y^2 — x | < eps.
G>Независимо от вида и размера алгоритма вычисления корня — спецификация настолько полна, что враг не пройдет. Никак.
Ну смотря что хотелось. Если ты хотел квадратный корень посчитать, то херовая спецификация, если честно
Я бы попросил
— y > 0 (а то их два)
— относительную погрешность, а не абсолютную (иначе корни из величины порядка eps будет не взять, а если взять слишком маленький eps, он окажется за границами точности double для корней из больших чисел).
— ограничение на время (а то он будет случайно перебирать, ждать замаешься)
Но вот этого, кажется, хватит.
G>y = sort( x ); G>спецификация: для всех х таких, что len( х ) < 2 результат равен х; для других — G>Для каждого i от 0 до ( len( x ) — 1 ) верно y[ i ] <= y[ i + 1 ]
G>То же самое. И тоже — абсолютно независимо от алгоритма сортировки.
не, не, под эту спецификацию подходит следующее:
if len( х ) < 2:
return x
else:
return range(0, len(x))
G>И в обоих случаях размер спецификации никак не зависит от размера программы.
G>Что там у нас понятно насчет размера спецификации?
SH>Я бы попросил SH>- y > 0 (а то их два) SH>- относительную погрешность, а не абсолютную (иначе корни из величины порядка eps будет не взять, а если взять слишком маленький eps, он окажется за границами точности double для корней из больших чисел). SH>- ограничение на время (а то он будет случайно перебирать, ждать замаешься)
SH>Но вот этого, кажется, хватит.
Ух ты, какие мы щепитильные .
Но в целом все, конечно, правильно.
G>>y = sort( x ); G>>спецификация: для всех х таких, что len( х ) < 2 результат равен х; для других — G>>Для каждого i от 0 до ( len( x ) — 1 ) верно y[ i ] <= y[ i + 1 ]
G>>То же самое. И тоже — абсолютно независимо от алгоритма сортировки.
SH>не, не, под эту спецификацию подходит следующее:
Че такой длинный контрпример, печатать не лень?
Тут всего-то добавить надо к спеку:
Для любого x <- X count( x, X ) == count( x, Y ), где
count( x, X ) = count({ i | x == X[i], i <- 0..(len(X)-1) })
И для особо щепетильных:
count( X ) = количество элементов во множестве, len(X) — длина последовательности, и в определении count использована нотация "типо Цермело". А "<-" означает "принадлежит множеству".
G>>Что там у нас понятно насчет размера спецификации?
SH>Что всё немного сложнее.
Да как-то не заметил. Да, распухло на целых две строки каждая. Но че-то не смотря на загадочное "немного сложнее", от размера алгоритма оно зависеть не начало.
Здравствуйте, Gaperton, Вы писали:
SH>>Что всё немного сложнее. G>Да как-то не заметил. Да, распухло на целых две строки каждая. Но че-то не смотря на загадочное "немного сложнее", от размера алгоритма оно зависеть не начало.
Да я не о том. А о том, что пропустить что-то важное легко. Мы вот вроде написали более-менее правильные версии для довольно простых случаев, но вполне вероятно, что сейчас придёт ещё один коллега, ткнёт пальцем, и мы оба поймём, как облажались.
Спецификации полезны и прекрасны, но их полноту обосновать невозможно. Только в духе "пять умных мужиков думали-думали, вот такое придумали, пять лет прошло, никто пока не опроверг". А обосновать невозможно, потому что спецификация должна полно выражать неформальное желание "чтобы всё было хорошо" Даже то, чего я не знал или забыл.
Ну, не знал, что мне понадобятся числа больше 2^32, или знал, но не знал, что это важно. И вот всё плохо -- иногда, внезапно, с непонятными результатами. Ну понятно, остаются только младшие разряды, фактически мусор, и дальше он невозбранно идёт в работу и где-то в недрах всё валится. Опа-на, оказывается, надо учитывать такие детали реализации машинной арифметики.
Или, прекрасный алгоритм, вовсю бегающий по массиву в случайном порядке, оказывается не масштабируемым, т.к. когда массив не влезает в память, случайный порядок обращения вызывает такой свопинг, что кони дохнут. Потому что забыли, забыли сказать, что данных то у нас будет 16 Гб, а оперативной памяти поменьше. Говорили, что "много". Ну, разное бывает много. Ну, можно купить машинку побольше, хотя это недёшево. Но в общем и машинки имеют свой предел.
И это только техника. А сколько юз-кейсов можно забыть! Типа подразумевалось, но не сказалось, или потом в работе обнаружилось, или вдруг внезапно отрубили свет и выяснилось, что надо было хранить критичные данные как-то так, чтоб не портились. Или нагрянули с обыском, и снова выяснилось, что критические данные надо было хранить как-то ещё иначе. Хотя такое обычно не забывают.
Чёт я увлёкся. Короче, без спецификации как-то никуда, на размахивании руками ничего не сделаешь. Но надеяться, что ты сделал полную спецификацию -- враг не подберётся -- можно, но только если это что-то очень простое. Желательно с конечным количеством состояний, которые можно нарисовать на бумажке.
Да, а от размера алгоритма начнёт зависеть, когда тебе зачем-то придётся перейти от декларативной форме к описанию алгоритма решения в каком-то виде. Если не понадобится, то и не начнёт, пожалуй.
Здравствуйте, SergH, Вы писали:
SH>Да я не о том. А о том, что пропустить что-то важное легко. Мы вот вроде написали более-менее правильные версии для довольно простых случаев, но вполне вероятно, что сейчас придёт ещё один коллега, ткнёт пальцем, и мы оба поймём, как облажались.
Да, это вполне вероятно.
И тем не менее, приведенных мной простейших спецификаций на практике достаточно, чтобы отловить большую часть багов.
Штука в том, что действительно полные предусловия-постусловия кроме прочего программу нехило затормаживают при проверке, и потому неправктичны. Ну, если их не выводом проверять, статически, а по простому — при выполнении.
SH>Спецификации полезны и прекрасны, но их полноту обосновать невозможно.
Теоретически это вполне возможно. И практически — для приведенных примеров — уж точно.
На практике — это обычно не нужно. Требования очень редко известны с такой степенью достоверности и детальности.
SH>Ну, не знал, что мне понадобятся числа больше 2^32, или знал, но не знал, что это важно. И вот всё плохо -- иногда, внезапно, с непонятными результатами. Ну понятно, остаются только младшие разряды, фактически мусор, и дальше он невозбранно идёт в работу и где-то в недрах всё валится. Опа-на, оказывается, надо учитывать такие детали реализации машинной арифметики.
Даже простейшие спецификации помогают почти моментально локализовать проблему при ее возникновении. Включая вышеописанные.
SH>Или, прекрасный алгоритм, вовсю бегающий по массиву в случайном порядке, оказывается не масштабируемым, т.к. когда массив не влезает в память, случайный порядок обращения вызывает такой свопинг, что кони дохнут. Потому что забыли, забыли сказать, что данных то у нас будет 16 Гб, а оперативной памяти поменьше. Говорили, что "много". Ну, разное бывает много. Ну, можно купить машинку побольше, хотя это недёшево. Но в общем и машинки имеют свой предел.
Формальные спецификации обычно определяют функциональную корректность, а не быстродействие.
SH>И это только техника. А сколько юз-кейсов можно забыть!
Никто не говорит, что полные спецификации появляются волшебным образом. Их составление работа, в которой также можно ошибиться, и с этим никто не спорит.
И что с того-то, собственно?
SH>Чёт я увлёкся. Короче, без спецификации как-то никуда, на размахивании руками ничего не сделаешь. Но надеяться, что ты сделал полную спецификацию -- враг не подберётся -- можно, но только если это что-то очень простое. Желательно с конечным количеством состояний, которые можно нарисовать на бумажке.
Для простых вещей, лежащих "внизу" сложной системы, и "разделяемого кода", спецификации вообще the must.
SH>Да, а от размера алгоритма начнёт зависеть, когда тебе зачем-то придётся перейти от декларативной форме к описанию алгоритма решения в каком-то виде. Если не понадобится, то и не начнёт, пожалуй.
Не начнет спецификация зависеть от объема решения. Это очевидно, ибо спецификация определяет свойства входов и выходов, и ей по барабану, какой алгоритм. Пока не приведешь контрпример — не поверю.
Ага а потом:
— $%&^@ вашу %^& туда! Вы че не знали что ли что x — комплексное число??? а y — пара решений
— Так а в спеке же ниче не написанно! Такчто не %:?* мозги!!!
— %?:0! вы же инженеры! нельзя тупо читать спецификацию! Кому нафиг нужен простой квадратный корень???
....
И понеслась....
Здравствуйте, TimurSPB, Вы писали:
G>>y = sqrt( x );
TSP>Ага а потом: TSP>- $%&^@ вашу %^& туда! Вы че не знали что ли что x — комплексное число??? а y — пара решений TSP>- Так а в спеке же ниче не написанно! Такчто не %:?* мозги!!! TSP>- %?:0! вы же инженеры! нельзя тупо читать спецификацию! Кому нафиг нужен простой квадратный корень??? TSP>.... TSP>И понеслась....
Как будь-то ровно то же самое не произойдет и без формальной спецификации. Смешные вы, парни.
Здравствуйте, Gaperton, Вы писали:
G>Как будь-то ровно то же самое не произойдет и без формальной спецификации. Смешные вы, парни.
Суровых сибирских мужиков с японской пилой напоминаете. В первую голову ищете, что-бы туда такого положить, чтобы она "хр-р" сказала, и можно было с чистым сердцем пойти рубить лес топорами.
G>Как будь-то ровно то же самое не произойдет и без формальной спецификации. Смешные вы, парни.
Произойдет. Только на это будет потрачено больше ресурсов. На сегодня, формальные спецификации на практике мало применимы.
G>Не начнет спецификация зависеть от объема решения.
А что в данном контексте означает "решение"? G> Это очевидно, ибо спецификация определяет свойства входов и выходов, и ей по барабану, какой алгоритм. Пока не приведешь контрпример — не поверю.
Если мы говорим о классических примерах из книг то все верно. Типа простой детерминированный алгоритм, прекрасно описываемый в терминах вход-выход.
Но реальные программы это больше чем вход — выход. И с ростом объема кода растет пространство состояний системы. Кроме того выполнение программы далеко не всегда при одинаковых входных данных даст одинаковые выходные. Поэтому с ростом объема решения спецификация будет вырастать. Если выполнение программы не детерминировано, то надо будет как минимум в спецификации заводить критерии эквивалентности выходных значений.
Здравствуйте, TimurSPB, Вы писали:
G>>Как будь-то ровно то же самое не произойдет и без формальной спецификации. Смешные вы, парни. TSP>Произойдет. Только на это будет потрачено больше ресурсов. На сегодня, формальные спецификации на практике мало применимы.
На сегодня, для применения формальных спецификаций на практике достаточно наличия элементарных возможностей, вроде выписывания ассертов. В которые кладутся предусловие и постусловие. И это не единственный способ.
Так что отлично они применимы. Те, кто применял — знает.
Здравствуйте, TimurSPB, Вы писали:
G>>Не начнет спецификация зависеть от объема решения. TSP>А что в данном контексте означает "решение"?
Код реализации.
G>> Это очевидно, ибо спецификация определяет свойства входов и выходов, и ей по барабану, какой алгоритм. Пока не приведешь контрпример — не поверю.
TSP>Если мы говорим о классических примерах из книг то все верно. Типа простой детерминированный алгоритм, прекрасно описываемый в терминах вход-выход. TSP>Но реальные программы это больше чем вход — выход. И с ростом объема кода растет пространство состояний системы. Кроме того выполнение программы далеко не всегда при одинаковых входных данных даст одинаковые выходные. Поэтому с ростом объема решения спецификация будет вырастать.
Я применял это в реальных программах. Они не больше, чем входа, выход, и состояние. Которое также делается предметом спецификаций. А уж какая будет комбинаторная сложность по состояниям — от проектировщика зависит. Не готовь "спагетти" на "бойлерплейтах", и он будет вполне приемлема.
TSP>Если выполнение программы не детерминировано, то надо будет как минимум в спецификации заводить критерии эквивалентности выходных значений.
Выполнение программы _всегда_ детерминировано. И у валидного внутреннего состояния всегда есть инварианты.
TSP>>А что в данном контексте означает "решение"? G>Код реализации.
TSP>>Если мы говорим о классических примерах из книг то все верно. Типа простой детерминированный алгоритм, прекрасно описываемый в терминах вход-выход. TSP>>Но реальные программы это больше чем вход — выход. И с ростом объема кода растет пространство состояний системы. Кроме того выполнение программы далеко не всегда при одинаковых входных данных даст одинаковые выходные. Поэтому с ростом объема решения спецификация будет вырастать. G>Я применял это в реальных программах. Они не больше, чем входа, выход, и состояние. Которое также делается предметом спецификаций. А уж какая будет комбинаторная сложность по состояниям — от проектировщика зависит. Не готовь "спагетти" на "бойлерплейтах", и он будет вполне приемлема.
Две переменных int32 — и вот тебе 2^64 возможных состояния. Понятно что это пространство должно быть минимально возможным. Но в реальности то это зависит от программиста больше чем от проектировщика.
TSP>>Если выполнение программы не детерминировано, то надо будет как минимум в спецификации заводить критерии эквивалентности выходных значений. G>Выполнение программы _всегда_ детерминировано.
И да же многопоточных?
G>И у валидного внутреннего состояния всегда есть инварианты.
Только определить эти инварианты не всегда так просто.
G>>Не начнет спецификация зависеть от объема решения.
Сам же пишешь: "Они не больше, чем входа, выход, и состояние. Которое также делается предметом спецификаций."
Если растет "решение", то скорее всего растет каждый из трех пунктов, а как следствие и спецификация.
Здравствуйте, TimurSPB, Вы писали: TSP>>>Но реальные программы это больше чем вход — выход. И с ростом объема кода растет пространство состояний системы. Кроме того выполнение программы далеко не всегда при одинаковых входных данных даст одинаковые выходные. Поэтому с ростом объема решения спецификация будет вырастать. G>>Я применял это в реальных программах. Они не больше, чем входа, выход, и состояние. Которое также делается предметом спецификаций. А уж какая будет комбинаторная сложность по состояниям — от проектировщика зависит. Не готовь "спагетти" на "бойлерплейтах", и он будет вполне приемлема. TSP>Две переменных int32 — и вот тебе 2^64 возможных состояния. Понятно что это пространство должно быть минимально возможным.
Это ерунда.
int32 m_a, m_b;
always( m_a > m_b );
Вот тебе вполне рабочий инвариант на состояние. И разрядность здесь абсолютно по барабану — комбинаторная сложность определяется цикломатикой, т.е. количеством возможных вариантов проходов по коду функции. Будет ошибка, связанная с разрядностью — сломаются самые обычные инварианты.
> Но в реальности то это зависит от программиста больше чем от проектировщика.
В реальности проектировщик — это обязательно программист, а программист — чаще всего проектировщик.
TSP>>>Если выполнение программы не детерминировано, то надо будет как минимум в спецификации заводить критерии эквивалентности выходных значений. G>>Выполнение программы _всегда_ детерминировано. TSP>И да же многопоточных?
Когда ты про "критерии эквивалентности выходных значений", ты, конечно, многопоточность имел в виду, да?
Выполнение каждого отдельного потока детерминоровано. И с точки зрения выполнения предусловий, постусловий, и инвариантов состояния — совокупность этих потоков также детерминирована. То, что вычисления могут в разном порядке происходить, этому никак не мешает.
Параллельную программу вообще без спецификаций отлаживать — стреляться можно.
G>>И у валидного внутреннего состояния всегда есть инварианты. TSP>Только определить эти инварианты не всегда так просто.
Ну, это уж кому как.
G>>>Не начнет спецификация зависеть от объема решения. TSP>Сам же пишешь: "Они не больше, чем входа, выход, и состояние. Которое также делается предметом спецификаций."
Спецификация функции состоит из предусловия и постусловия, и от длины реализации функции не зависит.
TSP>Если растет "решение", то скорее всего растет каждый из трех пунктов, а как следствие и спецификация.
Мне надоело из пустого в порожнее переливать. Пока.
TSP>>Если растет "решение", то скорее всего растет каждый из трех пунктов, а как следствие и спецификация. G>Мне надоело из пустого в порожнее переливать. Пока.
Да че тут переливать? Растет решение — растет спецификация. Удачи
Да, распухло на целых две строки каждая. Но че-то не смотря на загадочное "немного сложнее", от размера алгоритма оно зависеть не начало.
