Аксиоматический метод доказательства соответствия формализованных в различных моделях данных запросов
Аннотация
Аксиоматический метод в программировании используется давно и с целью более формального и точного описания процессов. Основное направление аксиоматизации в программировании было направлено на доказательство частичной правильности (верификацию) программ. Вместе с тем, ряд работ был ориентирован на обработку больших потоков данных – файлов. В них рассматриваются алгоритмы как унарных, так и бинарных операций и на основе аксиом доказывается их частичная правильность. Кроме того, аксиоматический подход позволил решить ряд задач в области разработки программного обеспечения для различных системных и прикладных областей. В статье рассматриваются аксиоматический метод, который позволяет формализовать объекты обработки данных и операции преобразования объектов посредством специального описания исходных объектов, и объекта – результата преобразования. В статье рассматривается возможность преобразования на основе аксиоматики для массовой обработки данных алгебраических выражений запросов, формализованных в одной модели данных, в частности в многомерно-матричной в другую – реляционную модель данных. Необходимость такого преобразования состоит в том, что выражение в многомерно-матричной модели значительно проще, чем в реляционной. Его проще преобразовывать с целью оптимизации запроса, и оно позволяет решить проблему распараллеливания запроса как на уровне задачи, так и на уровне отдельных операций. Для этой цели даны теоретико-множественные алгебраические определения двух основных операций обработки данных, соответствующих слиянию строго и нестрого упорядоченных файлов. На основе этих определений приведены аксиоматические описания этих операций. Приведены определения операций сложения и умножения многомерных матриц. Сконструированы соответствующие им операции-запросы в реляционной модели данных. Это соответствие доказано на основе аксиоматического метода. Показано, что каждый запрос на обработку данных есть теорема, и сделан вывод о эквивалентности моделей как аксиоматических теорий. Приведен пример, который показывает, как устанавливается такое соответствие.
![Лицензия Creative Commons](http://i.creativecommons.org/l/by/4.0/88x31.png)
Это произведение доступно по лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная.
Редакционная политика журнала основывается на традиционных этических принципах российской научной периодики и строится с учетом этических норм работы редакторов и издателей, закрепленных в Кодексе поведения и руководящих принципах наилучшей практики для редактора журнала (Code of Conduct and Best Practice Guidelines for Journal Editors) и Кодексе поведения для издателя журнала (Code of Conduct for Journal Publishers), разработанных Комитетом по публикационной этике - Committee on Publication Ethics (COPE). В процессе издательской деятельности редколлегия журнала руководствуется международными правилами охраны авторского права, нормами действующего законодательства РФ, международными издательскими стандартами и обязательной ссылке на первоисточник.
Журнал позволяет авторам сохранять авторское право без ограничений. Журнал позволяет авторам сохранить права на публикацию без ограничений.
Издательская политика в области авторского права и архивирования определяются «зеленым цветом» в базе данных SHERPA/RoMEO.
Все статьи распространяются на условиях лицензии Creative Commons «Attribution» («Атрибуция») 4.0 Всемирная, которая позволяет другим использовать, распространять, дополнять эту работу с обязательной ссылкой на оригинальную работу и публикацию в этом журналe.