1. Наука
  2. Видання
  3. Збірник наукових праць Харківського національного університету Повітряних Сил
  4. 3(21)'2009
  5. Верификация интерпретаторов алгебраических операций в расширениях многосортных алгебр

Верификация интерпретаторов алгебраических операций в расширениях многосортных алгебр

М.С. Львов
Аннотации на языках:

Разработка алгоритмов выполнения алгебраических вычислений – одна из основных задач, возникающих при реализации математических систем, основанных на символьных преобразованиях. Математическая модель этой задачи - многосортные алгебраические системы. В данной работе рассмотрен подход к верификации интерпретаторов многосортных алгебраических операций по их спецификациям, основанный на конструктивном уточнении понятия расширения многосортной алгебраической системы и доказательстве аксиом алгебраической системы. Этот подход проиллюстрирован примерами верификации интерпретаторов операций поля рациональных чисел, многочленов одной переменной и алгебры высказываний. Практика использования этого подхода при разработке математических систем учебного назначения показала его эффективность и даже универсальность.
Ключевые слова: математическая система, символьные преобразования, многосортные алгебраические системы, расширения алгебраических систем, верификация, интерпретаторы алгебраических операций