Применение инвариантов в математике и программировании. Использование инварианта цикла в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом. Проблема автоматического поиска инварианта цикла.
Инвариант цикла - в программировании - логическое выражение истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. Причем если в инвариант входят переменные, определенные только внутри цикла (например, счетчик цикла for в Паскале или Аде), то для входа в цикл они учитываются с теми значениями, которые получат в момент инициализации. Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении всего цикла инвариант будет выполняться. Например, чтобы убедиться, что оптимизированный цикл остался корректным, достаточно доказать, что инвариант цикла не нарушен и условие завершения цикла достижимо. инвариант верификация алгоритм цикл Инвариантом в программировании называется логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.Для успешного решения различных задач по математике и программированию необходимо уметь пользоваться инвариантами при решении задач.
Введение
«…Учитель: Проведем эксперимент. Видите, ребята, на доске написано 11 чисел - 6 нулей и 5 единиц. Теперь 10 раз подряд выполните такую операцию: зачеркните любые два числа и, если они были одинаковы, допишите к оставшимся числам один ноль, а если разные - единицу. Сделайте это у себя в тетрадях. Итак, все? А теперь я скажу вам, какое число у вас получилось. У всех вас должна была получиться единица!»
Эта сцена вызывает единственный вопрос: откуда же учитель заранее знал, какое число получится у ребят? Ведь операции можно выполнять самыми разными способами. Но все дело в том, что после каждой операции сумма всех чисел на доске обязательно остается нечетной, какой она и была в начале. Проверить это совсем не трудно - сумма каждый раз меняется на 0 или 2. Значит, и после 10 операций оставшееся число должно быть нечетным, т.е. равным 1. Объяснив это детям, учитель, наверно, не удержится и упомянет волшебное слово «инвариант».
Что же такое инвариант? Говоря по-русски, инвариант - это то, что не изменяется, как в нашем примере не менялась четность суммы цифр.
Теоретическая часть. Инвариант и его применение
Инвариант преобразования - это величина, не изменяющаяся при преобразовании. Примером инварианта может служить площадь фигуры, которая составляется из нескольких частей или окружность, переходящая сама в себя при повороте плоскости вокруг ее центра.
Для чего же нужен инвариант? Пусть дана задача: у нас есть операция и два положения: начальное и конечное. Требуется узнать, можно ли от начального положения перейти к конечному применением этой операции.
Рассмотрим эту ситуацию на примере: на доске в строчку выписаны 15 чисел - 8 нулей и 7 единиц. Разрешается стереть любые два числа и, если они были одинаковы, написать ноль, а если разные - единицу. Требуется узнать, можно ли в конце получить ноль?
Итак, мы имеем: операцию, которая берет два числа и выдает третье, начальное положение - 15 чисел и конечное - единственный нолик. Посмотрим, что же не изменялось при этой операции, что же было инвариантно? После каждой операции сумма всех чисел, написанных на доске, либо не изменилась, либо уменьшилась на 2. Потому что 1 и 0 переходит в 1, остальные числа не изменились. Значит, сумма осталась та же. Аналогично 0 и 1 переходят в 1, 0 и 0 переходят в 0 - тут сумма не изменилась, а 1 и 1 переходят в 0 - сумма уменьшилась на 2. Значит, инвариантом служит четность суммы - только что мы доказали, что она не изменяется. Теперь смотрим на положения: вначале сумма была нечетна, а в конце - четна, то есть при операции, сохраняющей четность, осуществить переход невозможно. В конце могла быть только единица.
В этом и есть основное применение инварианта - доказать, что нельзя перейти от одного положения к другому с помощью данной операции. Для этого нужно выделить величину, не изменяющуюся при преобразовании, но различную для начального и конечного положений. Также идея инварианта нужна также для того, чтобы узнать, что может получиться из данных начальных условий ( например, в данной задаче из начальной позиции могла получиться только единица). Следует также понимать, что инвариант нельзя применять для доказательства возможности перехода от одного положения к другому, т.к. из совпадения инвариантов положений не следует, что можно осуществить переход.
Инвариант часто используется при решении нестандартных (в т.ч. олимпиадных) задач. Сама же идея инварианта широко применяется в высшей математике: в аналитической и дифференциальной геометрии, топологии, алгебре, программировании и т.д.
Инварианты в программировании
Значение членов или объектов, доступных с помощью членов класса, называется состоянием объекта (или просто значением объекта). Главное при построении класса - это: привести объект в полностью определенное состояние (инициализация), сохранять полностью определенное состояние объекта в процессе выполнения над ним различных операций, и в конце работы уничтожить объект без всяких последствий. Свойство, которое делает состояние объекта полностью определенным, называется инвариантом.
Поэтому назначение инициализации - задать конкретные значения, при которых выполняется инвариант объекта. Для каждой операции класса предполагается, что инвариант должен иметь место перед выполнением операции и должен сохраниться после операции. В конце работы деструктор нарушает инвариант, уничтожая объект. Например, конструктор String::String(const char*) гарантирует, что p указывает на массив из, по крайней мере, sz элементов, причем sz имеет осмысленное значение и v[sz-1]==0. Любая строковая операция не должна нарушать это утверждение.
При проектировании класса требуется большое искусство, чтобы сделать реализацию класса достаточно простой и допускающей наличие полезных инвариантов, которые несложно задать. Легко требовать, чтобы класс имел инвариант, труднее предложить полезный инвариант, который понятен и не накладывает жестких ограничений на действия разработчика класса или на эффективность реализации. Здесь «инвариант» понимается как программный фрагмент, выполнив который, можно проверить состояние объекта. Вполне возможно дать более строгое и даже математическое определение инварианта, и в некоторых ситуациях оно может оказаться более подходящим. Здесь же под инвариантом понимается практическая, а значит, обычно экономная, но неполная проверка состояния объекта.
Понятие инварианта появилось в работах Флойда, Наура и Хора, посвященных пред- и постусловиям, оно встречается во всех важных статьях по абстрактным типам данных и верификации программ за последние 20 лет. Оно же является основным предметом отладки в C .
Обычно, в течение работы функции-члена инвариант не сохраняется. Поэтому функции, которые могут вызываться в те моменты, когда инвариант не действует, не должны входить в общий интерфейс класса. Такие функции должны быть частными или защищенными.
Как можно выразить инвариант в программе на С ? Простое решение - определить функцию, проверяющую инвариант, и вставить вызовы этой функции в общие операции. Например: class String { int sz;
{ check(); // проверка на входе if (i<0 || i<sz) throw Range; // действует check(); // проверка на выходе return v[i];
}
Этот вариант прекрасно работает и не осложняет жизнь программиста. Но для такого простого класса как String проверка инварианта будет занимать большую часть времени счета. Поэтому программисты обычно выполняют проверку инварианта только при отладке: inline void String::check()
{ if (!NDEBUG) if (p==0 || sz<0 || TOO_LARGE<=sz || p[sz]) throw Invariant;
}
Мы выбрали имя NDEBUG, поскольку это макроопределение, которое используется для аналогичных целей в стандартном макроопределении С assert(). Традиционно NDEBUG устанавливается с целью указать, что отладки нет. Указав, что check() является подстановкой, мы гарантировали, что никакая программа не будет создана, пока константа
NDEBUG не будет установлена в значение, обозначающее отладку. С помощью шаблона типа Assert() можно задать менее регулярные утверждения, например: template inline void Assert(T expr,X x)
{ if (!NDEBUG) if (!expr) throw x;
} вызовет особую ситуацию x, если expr ложно, и мы не отключили проверку с помощью NDEBUG. Использовать Assert() можно так: class Bad_f_arg { };
void f(String& s, int i)
{
Assert(0<=i && i<s.size(),Bad_f_arg());
//...
}
Шаблон типа Assert() подражает макрокоманде assert() языка С. Если i не находится в требуемом диапазоне, возникает особая ситуация Bad_f_arg.
С помощью отдельной константы или константы из класса проверить подобные утверждения или инварианты - пустяковое дело. Если же необходимо проверить инварианты с помощью объекта, можно определить производный класс, в котором проверяются операциями из класса, где нет проверки.
Для классов с более сложными операциями расходы на проверки могут быть значительны, поэтому проверки можно оставить только для «поимки» трудно обнаруживаемых ошибок. Обычно полезно оставлять, по крайней мере, несколько проверок даже в очень хорошо отлаженной программе. При всех условиях сам факт определения инвариантов и использования их при отладке дает неоценимую помощь для получения правильной программы и, что более важно, делает понятия, представленные классами, более регулярными и строго определенными. Дело в том, что когда вы создаете инварианты, то рассматриваете класс с другой точки зрения и вносите определенную избыточность в программу. То и другое увеличивает вероятность обнаружения ошибок, противоречий и недосмотров. Две самые общие формы преобразования иерархии классов состоят в разбиении класса на два и в выделении общей части двух классов в базовый класс. В обоих случаях хорошо продуманный инвариант может подсказать возможность такого преобразования. Если, сравнивая инвариант с программами операций, можно обнаружить, что большинство проверок инварианта излишни, то значит класс созрел для разбиения. В этом случае подмножество операций имеет доступ только к подмножеству состояний объекта. Обратно, классы созрели для слияния, если у них сходные инварианты, даже при некотором различии в их реализации.
Инвариант цикла
Инвариант цикла - в программировании - логическое выражение истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла. Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом.
Определение: Инвариант цикла представляет собой математическое выражение (обычно - равенство), в которое неустранимым образом входят по крайней мере некоторые переменные, значения которых изменяются от одного прохода цикла до другого. Инвариант строится таким образом, чтобы быть истинным непосредственно перед началом выполнения цикла (перед входом в первую итерацию) и после каждой его итерации. Причем если в инвариант входят переменные, определенные только внутри цикла (например, счетчик цикла for в Паскале или Аде), то для входа в цикл они учитываются с теми значениями, которые получат в момент инициализации.
Доказательство работоспособности цикла с помощью инварианта
Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему: Доказывается, что выражение инварианта истинно перед началом цикла.
Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении всего цикла инвариант будет выполняться.
Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).
Доказывается (возможно - без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.
Истинность утверждений, доказанных на предыдущих этапах, однозначно свидетельствует о том, что цикл выполнится за конечное время и даст желаемый результат.
Также инварианты используют при проектировании и оптимизации циклических алгоритмов. Например, чтобы убедиться, что оптимизированный цикл остался корректным, достаточно доказать, что инвариант цикла не нарушен и условие завершения цикла достижимо. инвариант верификация алгоритм цикл
Проблема автоматического поиска инварианта цикла
В современном мире почти каждый программный продукт содержит в себе хотя бы одну ошибку. И с этой проблемой хорошо знаком любой программист, хотя бы раз разрабатывавший достаточно сложную программу. Избежать ошибок во время разработки и кодирования практически невозможно. А если еще принять во внимание то, что с каждым годом программные продукты становятся все более сложными и масштабными, то становится, очевидно, что верификация программ является одной из самых сложных и серьезных проблем в данной области.
Для того чтобы не допустить сбоев и ошибок в программном обеспечении существуют методы верификации программного обеспечения, которые позволяют доказать правильность работы программы.
В теории верификации программного обеспечения есть необходимость решения трех следующих задач: 1. Доказательство частичной корректности выполнения программ.
2. Доказательство завершимости программ.
3. Доказательство незавершимости программ.
Разработанный Хоаром аксиоматический подход для задания формальной семантики программ, является одним из наиболее широко используемых методов решения указанных проблем.
Однако ни одна из этих трех задач не может быть в полной мере решена без использования инвариантов цикла.
Инвариантом в программировании называется логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.
Однако, поскольку в общем виде инвариант цикла не является очевидным для конкретного цикла, то задача о поиске инварианта является более чем актуальной в теории верификации программного обеспечения. Если будет возможным найти инвариант для любого заданного цикла, то это позволит в большинстве случаев автоматизировать процесс верификации программного кода. А это является просто чрезвычайно важным обстоятельством, учитывая сложность и размеры большинства современных программ.
Одной из серьезных проблем в теории верификации программного обеспечения является проблема завершимости самой программы. Из всех существующих программных конструкций только циклические конструкции могут привести к незавершимости программ. В предложены условия завершимости циклов: Р&B>(Е>O) (1)
{0<E=E0}S{0?E<E0} (2)
Пусть E - некоторое целочисленное выражение. Предположим, что справедливо условие 1 и для любого выражения Е0, принимающего целочисленные значения, справедливо условие 2. Это означает, что утверждение Е ? 0 также, как и Р является инвариантом цикла, т.е. выражение E остается неотрицательным в течение итерационного процесса. Кроме того, условие (2) означает, что каждое выполнение программы C уменьшает значение выражения E. Таким образом, из справедливости (1) и (2), а также {Р & В} C {P} непосредственно следует вывод о конечности итерационного процесса, так как целочисленное выражение Е не может уменьшаться бесконечное число раз и оставаться положительным, как требует условие (1).
«Eo$m({0<E=Eo}Sm{0?Е<Ео}), (2*)
Таким образом, можно сделать вывод, что для того чтобы доказать завершимость программы необходимо найти утверждение E и проверить его на выполнение условий 1 и 2*.
В данной работе делается попытка найти для конкретно заданного цикла инвариант, который позволял бы доказать его частичную корректность.
Пусть требуется найти инвариант цикла P, который позволял бы доказать частичную корректность выполнения некоторого цикла. Для поиска инварианта P мы определим некоторое множество операций O с типичными элементами o, с индексами или без и множество всех переменных V также с типичными элементами x, y, z,…, с индексами или без, входящих в структуру инварианта, а именно те и только те переменные, что изменяются внутри цикла. Дополнительно требуется определить множество T с типичными элементами t, с индексами или без, которые будут обозначать некоторые выражения. Множество T будет строиться пошагово, на первом шаге все элементы множества Т полностью совпадают со всеми элементами множества V, на последующих шагах новые элементы множества определяются по правилу tn = (ti ok tj), где i < n, j < n и i ? j.
Рисунок 1. Блок-схема программы для поиска инвариантов циклов
Рассмотрим все сказанное выше на конкретном примере, где все переменные являются целочисленными. x := x0; z := 1; n := n0;
while n > 0 do if odd(n) z := z * x; fi n := n / 2; x := x * x; od {z = x0n0}
Найдем инвариант данного цикла. Вначале определим множество всех операций
O = { , -, *, /, ^},
состоящее из операций сложения, вычитания, умножения, деления и возведения в степень
Далее определим множество
V = {x, z, n}, включающее лишь те переменные, которые изменяются в теле цикла.
Далее определим элементы множества T на первом шаге. Поскольку все элементы T на этом шаге полностью совпадают со всеми элементами множества V, то множество
T = {x, z, n}.
Поскольку программа работает с конкретным циклом и с конкретными значениями переменных, то для того, чтобы можно было проверить, является ли конкретный элемент множества T искомым инвариантом P нашего цикла, необходимо задать любые значения начальных переменных x0, n0, и z0 и выполнить этот цикл. По условию примера z0 = 1, а значит остается задать только значения переменных x0 и n0. Пусть в нашем конкретном случае x0 = 2 и n0 = 5. Если окажется, что несколько элементов множества T подходят в качестве инварианта P, то можно будет задать новые значения переменным x0 и n0 и повторить поиск инварианта P. Когда мы найдем утверждение, которое возможно является искомым инвариантом, нужно попытаться доказать с его помощью частичную корректность данного цикла. Если это удастся сделать, то данное выражение есть инвариант цикла.
Проверим каждый элемент множества T на необходимое условие, которым является следующее утверждение: Если известно некоторое утверждение X, заданное в виде некоторого равенства или же неравенства, которое устанавливается после выполнения цикла, то его можно представить в виде
X ? Xv (*) Xu. где Xv - выражение, состоящее из переменных изменяющихся в теле цикла, а, Xu - числовое значение, определяемое начальными переменными, * - логическое отношение (равенство или неравенство). Тогда, искомый инвариант P также может быть представлен в виде отношения P ? Pv (*) Pu, где Pv - некоторое выражение, Pu - значение выражения, * - логическое отношение (равенство или неравенство). В этом случае можно утверждать, что Pu = Xu, поскольку и инвариант P и утверждение X установятся после выполнения цикла, также, по этому, имеет место вхождение переменных выражения Xv в выражение Pv.
В нашем примере утверждение X задано в виде равенства и имеет вид z = x0n0.
Это равенство устанавливается по завершению цикла и в данном случае
Xv = z, а Xu = x0n0.
Для того, чтобы конкретный элемент множества T, в данном примере, удовлетворил заданному условию, его значение должно быть равно x0n0. Кроме того, каждый элемент множества T, претендующий на звание инварианта, обязательно должен содержать в себе переменную входящую в выражение Xv, а именно переменную z.
Перейдем к следующему шагу и дополним множество T, которое теперь примет вид: T={x, z, n, x z, x n,…, z - n, n - x,…,x / z, x / n,…, n ^ x, n ^ z}.
Посмотрим результат выполнения программы на шаге 2: Stage 2 invariants: No invariants Next stage? (Y/N): Нетрудно заметить, что ни один элемент множества T на втором шаге не удовлетворяет нашему условию.
Далее перейдем к выполнению шага 3. Множество T теперь примет вид: T= {x, z, n, x z, x n,…, z - n, n - x,…,x / z, x / n,…, n ^ x, n ^ z, …, (n x) - (n * z), …, (n ^ x) ^ (n ^ z)}.
Проанализируем результат выполнения программы на шаге 3: Stage 3 invariants: [[1], "*", [[0], "**", [2]]] = const
[[[0], "**", [2]], "*", [1]] = const Next stage? (Y/N): Соответственно, результатом работы программы являются коммутативные выражения
Ti ? z * xn и Tj ? xn * z множества T, которые и являются искомым инвариантом
P ? z * xn = x0n0 для конкретного цикла.
Для доказательства завершимости программ можно использовать разработанный Хоаром аксиоматический подход для задания формальной семантики программ, в котором операторы языка программирования ассоциируются с отношениями между утверждениями.
Выражение E является утверждением, для которого в общем случае не существует алгоритма поиска. Чтобы найти выражение E и попытаться решить данную проблему мы используем программу, которая будет генерировать множество различных выражений, начиная от самых простых и до самых сложных. Будем рассчитывать на то, что среди них окажется хотя бы одно, подходящее в качестве искомого выражения E.
Для поиска Е мы определим некоторое множество операций
O = { , -, *, /, ^}, состоящее из операций сложения, вычитания, умножения, деления и возведения в степень и определим множество всех переменных V также с типичными элементами, входящих в структуру инварианта, а именно те и только те переменные, что изменяются внутри цикла. Дополнительно требуется определить множество T, состоящее из типичных элементов, которыми будут являться некоторые выражения.
Множество T будет строиться пошагово, на первом шаге все элементы множества Т полностью совпадают со всеми элементами множества V, на последующих шагах новые элементы множества определяются по правилу tn = (ti ok tj), где i < n, j < n и i ? j.
Рисунок 2. Блок-схема программы для поиска выражения E
Рассмотрим конкретный пример. x := 100; s := -1; n = 0;
while x > 0 do x := x s * n; n := n 20; s := -s; od
Результатом работы программы: Stage 1 result: [0]
В программе переменные для данного примера заданы в виде массива m = [x, s, n], поэтому утверждением E в данном примере является переменная x. Поведение переменной x приведено на рисунке 3.
Рисунок 3.
Очевидно, что в данном примере значение переменной х уменьшается за прохождение не каждого тела цикла, однако все же оно уменьшается за каждые 2 прохода тела цикла, что в принципе является показателем того, что оно не может уменьшаться бесконечным и оставаться при этом положительным.
Предложенный способ поиска инварианта цикла позволяет во многих случаях найти утверждения, которые могут рассматриваться как инварианты циклов для использования их в процессе доказательства частичной корректности программ. А предложенный выше способ поиска выражения E не является универсальным и, далеко не во всех случаях позволяет получить необходимый результат, однако он существенно расширяет число программ, для которых становится возможным доказать завершимость. Это позволяет в части случаев автоматизировать сам процесс поиска выражения E, процесс доказательства завершимости программ и процесс доказательства частичной корректности программ. Заметим, что поиск инвариантов сложных циклов, например вложенных, является предметом дальнейших исследований авторов.
Повторяющиеся операции
Рассмотрим простейший пример - вывод массива на экран (примеры в этой статье приводятся на языке программирования С , однако они настолько просты, что не требуют практически никаких знаний этого языка). for(i = 0; i < N; i ) cout << X[i] << " ";
Данный фрагмент кода выводит на экран элементы массива X с нулевого по (N-1)-й, разделяя их пробелами. Сформулируем таким образом: после выполнения цикла элементы массива с нулевого по N-1 оказываются выведенными на экран через пробел. Такая формулировка точнее с той точки зрения, что она явно подчеркивает повторяемую операцию, в то время как фраза «вывести массив на экран» это только подразумевает.
Итак, элементы массива должны быть выведены на экран, и для этого необходимо использовать цикл. Каким же будет инвариант этого цикла? Очень простым - после выполнения i-й итерации цикла (итерации нумеруются по переменной цикла, то есть, начиная с нулевой) элементы массива с нулевого по i-й включительно будут выведены на экран. Данный пример слишком прост для того, чтобы продемонстрировать полезность инвариантов. Перейдем к следующему по сложности примеру.
Задача: найти максимальное число среди элементов [0 .. N-1] массива X, записать его в переменную M.
M = X[0];
for(i = 1; i < N; i ) if(X[i] > M)
M = X[i];
В данном случае цикл уже содержит условный оператор. Инвариант формулируется следующим образом: после выполнения итерации цикла со значением переменной цикла i=I, M равно максимальному элементу из первых I элементов массива.
Наиболее частой ошибкой при написании циклов являются ошибки в граничных условиях. Автор рекомендует читателям всегда перед тем, как писать нетривиальный цикл, четко уяснить для себя, что именно происходит на очередной его итерации и как именно выглядит инвариант в виде точной формулы, а не на уровне «интуитивного понимания».
Инварианты и оптимальные решения
Виртуозное владение инвариантами особенно полезно при решении задач по информатике, основанных на методе динамического программирования. Метод динамического программирования заключается в сведении задачи к аналогичным, но более простым. При этом алгоритм заключается в хранении «архива» решений простых задач и последовательном расширении этого архива, пока в него не попадет нужная нам задача. Алгоритмы, основанные на динамическом программировании, активно используют память. (см. практическая часть, задача 1.)
Инварианты и регулярные выражения
Эта задача уже может быть отнесена к категории сложных, придумать способ ее решения гораздо труднее, чем в предыдущих задачах. (см. практическая часть, задача 2.)
Для понимания следующей задачи необходимо ввести специальный термин. Регулярным выражением называется строка-шаблон, составленная по определенным правилам. Любую другую строку можно проверить на соответствие данному регулярному выражению. Основные правила построения шаблонов и проверки соответствия таковы: Если в шаблоне встречается символ, он же должен встретиться в рассматриваемой строке.
Если в шаблоне встречается запись вида A | B, то в строке должно встретиться A или B. A и B не обязаны быть буквами алфавита, они, в свою очередь также могут быть регулярными выражениями.
В шаблоне разрешается использовать круглые скобки, например, A | (AB).
Если в шаблоне встречается [A], то в рассматриваемой строке A может как встретиться, так и нет. Как и в предыдущем правиле, A может быть другим шаблоном.
Если в шаблоне встречается A , значит, терм A может встретиться в строке любое число раз подряд, либо вообще не встретиться.
Принято, что если в регулярное выражение необходимо вставить специальный символ, то перед ним ставится обратный слеш \
Например, шаблонами являются AB, A[B], A(B) . Строка AB подходит под все три шаблона, A - под второй и третий, ABB - только под третий. Под шаблон A[B[C]D] подходят строки A, ABD, ABCD, и не подходят никакие другие.
Практическая часть: Инварианты и оптимальные решения
Задача 1. («Покупка билетов»).
За билетами на премьеру нового мюзикла выстроилась очередь из N человек, каждый из которых хочет купить 1 билет. На всю очередь работала только одна касса, поэтому продажа билетов шла очень медленно, приводя «постояльцев» очереди в отчаяние. Самые сообразительные быстро заметили, что, как правило, несколько билетов в одни руки кассир продает быстрее, чем когда эти же билеты продаются по одному. Поэтому они предложили нескольким подряд стоящим людям отдавать деньги первому из них, чтобы он купил билеты на всех.
Однако для борьбы со спекулянтами кассир продавала не более 3-х билетов в одни руки, поэтому договориться таким образом между собой могли лишь 2 или 3 подряд стоящих человека.
Известно, что на продажу i-му человеку из очереди одного билета кассир тратит Ai секунд, на продажу двух билетов - Bi секунд, трех билетов - Ci секунд. Напишите программу, которая подсчитает минимальное время, за которое могли быть обслужены все покупатели.
Обратите внимание, что билеты на группу объединившихся людей всегда покупает первый из них. Также никто в целях ускорения не покупает лишних билетов, то есть билетов, которые никому не нужны.
Решение: Идея решения - объединить некоторых ожидающих в группы по два или три человека. Вопрос - как это сделать максимально эффективно, желательно, один раз прочитав входные данные и не перебирая варианты. На помощь приходят инварианты.
Пусть Z[i] - минимальная стоимость покупки билетов для первых i человек в очереди (в порядке «от кассы»). Понятно, что Z[0] = 0, Z[N] - ответ. Давайте научимся эффективно строить массив Z по мере просмотра людей в очереди.
Человек может купить билет только себе, себе и следующему человеку, либо себе и двум следующим. Таким образом, Z[i] зависит только от Z[i-1], Z[i-2], Z[i-3]. Несложно видеть, что Z[i] = min(Z[i-1] A[i-1], Z[i-2] B[i-2], Z[i-3] C[i-3]).
В переводе на русский язык, приведенная формула выглядит так: «Для того, чтобы оптимально купить билеты первым i людям в очереди, билет i-му человеку либо покупает он сам (при этом предыдущие (i-1) человек уже купили билеты оптимальным способом), либо билет ему берет (i-1)-й человек (и люди с 1-го по (i-2)-го ушли с билетами довольными), либо (i-3)-й человек берет сразу три билета».
В нашем случае, мы разделили большую задачу «найти оптимальный способ купить билеты на N человек (Z[N])» на подзадачи «построить Z[i] на основе предыдущих значений Z». Утверждение Z[0] = 0 является тривиальным решением. А написанная формула представляет собой формулу динамического программирования. Фактически она представляет собой инвариант оптимального решения задачи. Придумать эту формулу - значит, решить задачу. А для того, чтобы написать решение в виде программы, необходимо всего лишь реализовать ее в виде программы, чаще всего, в виде одного или нескольких вложенных циклов. Решение сложной задачи выглядит поразительно просто: #include using namespace std;
int N;
int X[5001][4], Z[5001];
int main() { int i, j;
cin >> N;
// X[i][1] == A[i]
// X[i][2] == B[i]
// X[i][3] == C[i] for(i = 0; i < N; i ) cin >> X[i][1] >> X[i][2] >> X[i][3];
// Идем ``по очереди"", отдалясь от кассы.
// Инвариант: после итерации цикла i=I, // часть массива Z от нуля до I заполнена
Дано регулярное выражение - слово из латинских букв, в котором используются квадратные скобочки. То, что заключено в квадратные скобочки, может присутствовать в слове или нет. Таким образом, регулярное выражение задает множество слов, которые можно из него получить, различными способами раскрывая присутствующие в нем квадратные скобочки. Про такие слова говорят, что они удовлетворяют регулярному выражению. Например, регулярному выражению a[b[c]d]e удовлетворяют следующие слова: ae, abde, abcde и не удовлетворяют слова abcd, abe, acde
Регулярное выражение имеет следующий рекуррентно-определенный синтаксис: regexp ::= ( lexem | "[" regexp "]" )
Это определение регулярного выражения (regexp) записанное в формате EBNF. Вертикальная палочка в этой записи означает союз "или". А комбинация ( X ) означает несколько (больше нуля) объектов X идущих друг за другом. Поэтому наше определение расшифровывается так: регулярное выражение - это либо лексема (lexem), либо какое-то другое регулярное выражение, заключенное в квадратные скобки. Пример регулярного выражения: abc[de[f]g][h]i[j].
Дать ответ, удовлетворяет ли данная строка S данному регулярному выражению R. Максимальная длина строки и регулярного выражения - 1000 символов. Регулярное выражение всегда задано корректно.
Например, под шаблон, приведенный в условии задачи, подходят строки «abcdefgi» и «achij», и не подходит строка «abcdefg».
Воспользуемся инвариантами и динамическим программированием для решения этой задачи. Чтобы перейти к инвариантам, надо научиться разбивать задачу на подзадачи так, чтобы из решения простых подзадач вытекало решение общей задачи.
Пусть, к примеру, первая половина строки подходит под первую половину шаблона, а вторая половина строки - под вторую половину шаблона. Тогда вся строка целиком подходит под шаблон. Идея решения заключается в том, чтобы понимать, какая часть строки подходит под какую часть шаблона.
Пойдем по шаблону слева направо, и, рассматривая начало шаблона R[0..i], будем помнить, для каких значений j часть строки S[0..j] подходит под это начало[4]. Покажем, что возможно оуществить переход от части шаблона R[0..i] к R[0..(i 1)]. Для этого введем следующие правила: • Если на месте i в шаблоне стоит символ (не квадратная скобка), то часть строки, которая раньше подходила под часть шаблона, будет подходить под него дальше тогда и только тогда, когда в строке следующим идет тот же самый символ. Пример: под шаблон «ab[c[d]]m» подходила строка «abcm», для того, чтобы строка подошла под продолжение шаблона «ab[c[d]]mn» необходимо, чтобы ее следующим символом был символ «n».
• Если в шаблоне встретилась открывающая квадратная скобка, то возможных вариантов два. Либо можно полностью пропустить часть шаблона в квадратных скобках, либо попытаться подставить некоторую часть строки, либо всю строку под часть шаблона, заключенную в квадратных скобках.
• Если же в шаблоне встретилась закрывающая квадратная скобка, то ее можно смело пропускать, потому что раз уж мы добрались до нее, значит, часть шаблона, которая заключалась между этой закрывающей и соответствующей открывающей скобками успешно пройдена.
После формулирования этих условий можно определить метод вычисления таблицы D. Элемент D[i][j] будет равен истине тогда и только тогда, когда начало строки S[0..j] подходит под начало шаблона R[0..i]. Начальные условия: в левом верхнем углу таблицы стоит «истина» (D[0][0] = true), переходы осуществяются по сформулированным выше правилам, а ответ будет содержаться в правом нижнем углу таблицы - в ячейке таблицы D[LENGTHR][LENGTHS].
Далее приведена одна из возможных реализаций описанного алгоритма на языке С .
#include
#include using namespace std;
string R, S;
int LENGTHR, LENGTHS;
bool D[1001][1001];
// Если D[i][j] == true, то первые i символов
// шаблона R могут соответствать первым
// j символам строки S. int main() { int i, j, OPENBRACE[1001], Match[1001];
cin >> R « S; LENGTHR = R.length();
LENGTHS = S.length();
for(i = 0, j = 0; i < LENGTHR; i ) { if(R[i] == "[")
OPENBRACE[j ] = i;
else if(R[i] == "]")
Match[OPENBRACE[-j]] = i;
}
// Теперь если R[i] == "[", то R[Match[i]] == "]"
// - соответствующая закрывающая скобка.
D[0][0] = true;
for(i = 0; i < LENGTHR; i ) for(j = 0; j <= LENGTHS; j ) if(D[i][j]) {
} else { // просто буква if(R[i] == S[j]) // только если совпадает
D[i 1][j 1] = true;
}
}
// ответ находится в D[LENGTHR][LENGTHS] if(D[LENGTHR][LENGTHS]) cout << «YES» << endl;
else cout << «NO» << endl;
return 0;
}
Вывод
Для успешного решения различных задач по математике и программированию необходимо уметь пользоваться инвариантами при решении задач. Найти инвариант в сложной задаче непросто, однако это очень мощный, а часто и наиболее быстрый способ получить решение. В программировании владение инвариантами открывает дорогу в мир динамического программирования, одного из наиболее интересных и эффективных методов решения задач.
Список литературы
1. Б. Страуструп. Язык программирования C (третье издание). - Пер. с англ. - СПБ., М.: «Невский диалект». Издательство «Бином», 1999.
2. Д. Кнут. Искусство программирования для ЭВМ. Т. 1-3. - Пер. с англ. - М.: Мир, 1976-1978.
3. В.В. Борисенко. Основы программирования. - М., Интернет-университет информационных технологий-ИНТУИТ.ру, 2005.
