Программные продукты и системы

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

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

В рамках проекта ИРБИС (Интегрированная распределенная банковская информационная система), разрабатываемого фирмой ИБИС (г. Одесса, Украина), реализована проверка реестров на полноту и непересекаемость на уровне логических условий. Отметим, что подраздел «Реєстри документів» проекта ИРБИС предусматривает также и многие другие операции с реестрами, как то:

-    выбор документов по условию с отображением в диалоговом окне или в текстовом файле;

-    выбор и сортировка атрибутов докумен- та (структур реестра), отображаемых при его выборе;

-    сортировка и группировка документов по заданной совокупности признаков в случае отчета в файл;

-    шаблоны выходных форм и др.

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

Математический алгоритм

Опишем математическую формализацию задачи проверки корректности совокупности условий, задающих реестры.

Напомним, что логические формулы состоят из букв, соединенных знаками конъюнкции («&»), дизъюнкции («|») и отрицания («!»).

Наравне с буквами логические формулы могут содержать предикаты. Предикат – это функция от одной или нескольких переменных, значения которых выбираются из некоторой заранее заданной предметной области (в данном случае из множества числовых характеристик банковских документов), причем значениями этой функции могут быть только логические константы true и false. Исходя из содержания задачи, ограничимся рассмотрением только одноместных предикатов, то есть логических функций от одной переменной. Этим одноместным предикатам позволим выражать некоторые равенства или неравенства, относящиеся к числовым характеристикам документа. Например: статус равен 15, код источника лежит в промежутке [13000, 14000).

Считая числовые характеристики документа целочисленными переменными, для каждого реестра получим логическую формулу, включающую логические переменные и одноместные предикаты, выражающие принадлежность некоторых целочисленных переменных заданным промежуткам (допускаются промежутки типа [15, 15], состоящие из одной точки). Документ входит в реестр, если подстановка его атрибутов в данную логическую формулу приводит к значению true, и не входит в противном случае.

Тот факт, что два реестра не пересекаются, означает, что конъюнкция соответствующих логических формул является ложной при любых значениях входящих в них булевых и целочисленных переменных. Особо отметим, что ложность полученной конъюнкции обязана выполняться тождественно (при любых значениях переменных), поскольку в разные дни в данные реестры попадают разные документы с разными логическими и числовыми характеристиками, а непересекаемость реестров должна соблюдаться при любых обстоятельствах. Взяв от рассматриваемой конъюнкции отрицание, необходимо получить тождественно истинную логическую формулу.

Полнота заданной совокупности реестров означает, что дизъюнкция всех логических формул, отвечающих реестрам, тождественно истинна.

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

Решение этой задачи основано на следующей лемме.

Напомним, что всякую логическую формулу, содержащую только буквы, можно привести к совершенной дизъюнктивной нормальной форме (см. [Яблонский С.В.]). Совершенная дизъюнктивная нормальная форма представляет собой дизъюнкцию нескольких скобок (они называются элементарными конъюнкциями). В каждой скобке записана конъюнкция n членов, где n – количество переменных, входящих в данную формулу. Каждый из этих членов представляет собой переменную либо отрицание переменной (таким образом, в каждой скобке участвуют все используемые переменные).

Пусть имеется логическая формула F, содержащая только логические предикаты рассматриваемого вида, и пусть количество этих предикатов равно n. Сопоставим каждому предикату, входящему в формулу F, вспомогательную логическую переменную (обозначим эти переменные через a1, a2, …, an) и составим из них все возможные элементарные конъюнкции. Если подставить вместо каждой из переменных ai соответствующий ей предикат, то каждая из элементарных конъюнкций задаст некоторое множество точек в пространстве Rm, где m – количество целочисленных переменных, входящих в формулу F. Некоторые из этих множеств могут оказаться пустыми, а из остальных (пусть их количество равно k, k£2n) выберем по одной точке с целочисленными координатами (поскольку фигурирующие в формуле F одноместные предикаты задают некоторые промежутки с целочисленными концами, то этот выбор можно сделать эффективно). Полученное множество, состоящее из k точек m-мерного пространства, имеющих целочисленные координаты, обозначим через U.

Лемма A. В обозначениях, представленных выше, для того чтобы формула F была тождественно истинна, необходимо и достаточно, чтобы она была истинна на каждом наборе значений переменных, входящем в множество U.

Доказательство. В части необходимости лемма очевидна. Докажем достаточность.

Обозначим через W множество целочисленных точек пространства Rm, дающих значение true при подстановке их координат в формулу F.

Заменим в формуле F каждый предикат соответствующей логической переменной ai и приведем полученную логическую формулу к совершенной дизъюнктивной нормальной форме. Обозначим через M множество элементарных конъюнкций, входящих в эту совершенную дизъюнктивную нормальную форму. Поскольку дизъюнкции элементарных конъюнкций отвечает объединение соответствующих подмножеств пространства Rm, то каждая из элементарных конъюнкций, входящих в M, соответствует некоторому подмножеству множества W.

С другой стороны, конъюнкции элементарных конъюнкций соответствует пересечение соответствующих подмножеств пространства Rm. Хорошо известно (это легко проверить), что конъюнкция любых двух различных элементарных конъюнкций тождественно ложна; следовательно, пересечение соответствующих подмножеств пространства Rm пусто. Отсюда ясно, что каждая из элементарных конъюнкций, не входящих в M, задает подмножество Rm, имеющее с W пустое пересечение.

Таким образом, каждая из 2n элементарных конъюнкций, которые можно составить из логических переменных a1, a2, …, an, соответствует подмножеству пространства Rm, либо полностью содержащемуся в W, либо имеющему с W пустое пересечение. Поскольку при доказательстве достаточности предполагалось, что выполнено включение UÌW, то пересечение множества W с каждым из тех подмножеств Rm, задаваемых элементарными конъюнкциями, которые не пусты, в свою очередь, тоже не пусто. Следовательно, каждое из этих множеств является подмножеством множества W.

Дизъюнкция всех 2n элементарных конъюнкций тождественно истинна (это хорошо известно и легко проверяется). Следовательно, объединение всех 2n подмножеств Rm, соответствующих элементарным конъюнкциям, дает всю целочисленную решетку Zm пространства Rm. Отбрасывая те элементарные конъюнкции, которые соответствуют пустому множеству, получаем, что объединение тех k множеств, представителями которых являются точки множества U, дает всю целочисленную решетку Zm. Поскольку каждое из этих множеств является подмножеством множества W, то W=Zm.

Лемма доказана.

Из этой леммы легко вывести следующий алгоритм.

Алгоритм L. Пусть имеется логическая формула G, содержащая булевы переменные и одноместные предикаты, выражающие принадлежность некоторых целочисленных переменных заданным числовым промежуткам. Для каждой целочисленной переменной отсортируем в порядке возрастания все встречающиеся в формуле G концы промежутков, отвечающих этой переменной. Станем независимо придавать каждой булевой переменной значения false и true, а каждой целочисленной переменной последовательно: одно значение левее первого элемента соответствующего ей отсортированного массива, сам этот элемент, одно целочисленное значение между первым и вторым элементом (если оно есть), второй элемент, ... , последний элемент, одно значение правее последнего элемента. Формула G тождественно истинна тогда и только тогда, когда она принимает значение true на каждом получившемся наборе значений своих переменных.

Доказательство. Присвоив какие-нибудь значения булевым переменным, входящим в формулу G, получим некоторую формулу F, содержащую только предикаты. Для этой формулы построим множество U, как в лемме A. Возьмем какую-нибудь точку x=(x1, x2, …, xm)ÎU.

Каждая координата xj  точки x попадает в одно из описанных в алгоритме подмножеств множества Z целых чисел. Осталось заметить, что в пределах любого из этих подмножеств каждая из логических переменных ai (обозначения леммы A) сохраняет постоянное значение, и применить лемму A.

Алгоритм доказан.

Особенности программной реализации

В проекте ИРБИС реализована возможность описания реестров документов. Для каждого реестра на специально разработанном языке логических формул задается условие отбора документов. Элементами языка являются предопределенные идентификаторы, операции сравнения, логические операции и скобки.

Приведем пример условия отбора:

status=15 & type=100 & home & initial &

& outward & ( srcCode<12000 | ( srcCode³13000 &

& srcCode<14000) | srcCode³15000)

Идентификаторы status, type, home и другие являются предопределенными и соответствуют определенным числовым или булевым характеристикам документа.

Реестры и, соответственно, условия их отбора задаются пользователями в пользовательском интерфейсе.

Реализованы операции проверки группы реестров на полноту и непересекаемость.

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

В проекте ИРБИС в качестве языка программирования используется Java. Кроме того, используется язык Python, в частности, как язык написания пользовательских скриптов. Применяется версия jPython (или jython) – реализация Python под Java-машину.

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

Причина в том, что в алгоритме реализации необходимо вычислять значение логической формулы, отвечающей одному реестру. Соответственно, необходим какой-то интерпретатор языка логических формул. Вместо этого логическая формула транслируется в Python-скрипт и формируется массив функций (такие массивы допускаются синтаксисом языка Python). Затем, используя цикл, перебирающий элементы массива этих функций, можно вычислить значение дизъюнкции всех формул, соответствующих реестрам.

Таким образом, формируется временный Python-скрипт, который тут же транслируется в байт-код Java и выполняется на той же Java-ма­шине, что и сама программа.

Авторы выражают признательность профессору Автономного университета (г. Мадрид, Испания) Д.В. Якубовичу, выведшему алгоритм L из леммы A.

Литература

Яблонский С.В. Введение в дискретную математику. М.: Наука, 1979. 272 с.