Для постановки сложных математических задач (суммирование бесконечных рядов, теоретикомножественных операций с бесконечными множествами, гильбертов оператор и др.) и задач искусственного интеллекта (игры, распознавание образов и др.) предложен общематематический процедурный язык, так называемый концепторный язык - КЯ [6.17]. В этом языке процесс описания сложной задачи проводится путем обоснования решения задачи с математической точки зрения, затем формального описания постановок задач и, наконец, делается переход к алгоритмическому описанию.
Средства спецификации сложных задач.Основу КЯ составляет теоретикомножественный язык, который содержит декларативные и императивные средства теории множеств ЦермелоФренкеля. Ядро содержит набор элементов (типы, выражения, операторы) и средства определения новых типов, выражений и операторов.
Декларативные средства КЯ - это типизированный, многосортный логикоматематический язык задания выражений и структуризации множества значений (денотат). Выражения состоят из термов и формул, термы обозначают объекты ПрО, а формулы - утверждения об объектах и отношениях между ними. К конструкторам составных типов и формул относятся функторы, предикаты, конекторы и субнекторы.
Функтор - это конструктор, преобразующий термы в термы. Предикаты превращают термы в формулы, конекторы включают в себя логические связки и кванторы для преобразования одной формулы в другую. Субнектор (дескриптор) - это конструктор построения термов из выражений и формул. Конструкторы термов - это традиционные арифметические и алгебраические операции над числовыми множествами и вещественными функциями. Конструкторы формул включают в себя предикаты, состоящие из предикатных и числовых символов, а также конекторы, состоящие из логических связок, кванторов и конструкторов теории множеств.
Императивные средства КЯ - это операторы и процедуры для описания объектов ПрО с помощью концепторов, состоящих из разделов для определения объектов решаемой задачи и действий над ними. Каждый концептор - это именованный набор определений и действий со следующей структурой описания:
концептор К (< список параметров >) <список импортных параметров> <определение констант, типов, предикатов> <описание глобальных переменных> <определение процедур> начало К <тело концептора> конец К. Концептор - это декларативное описание объектов и императивное описание операторов вычисления выражений тела. Рассматривается два случая:
1. декларативный концептор состоит из определений параметров и типов;
2. императивный концептор - это тело из операторов задач.
Декларативный концептор задает описание объектов и понятий, связанных с математической постановкой задачи, а описание метода ее решения с помощью императивных концепторов. Концепторное описание - это формальная спецификация задачи, которую можно трансформировать до алгоритмического описания и верификации.
Если полученный концептор неэффективен, то для повышения эффективности строится алгоритм, эквивалентный данному концептору. Он строится аппроксимацией концепторного решения путем замены неконструктивных объектов и неэффективных операций конструктивными и более эффективными аналогами.
Формализация КЯ. Общая схема формализации декларативной и императивной частей КЯ расширяется логикоматематическим языком, традиционными структурными операторами (присваивание, последовательность, цикл и т.п.), а также теоретикомодельными (денотационными) и аксиоматическими средствами формализации неконструктивной семантики КЯ.
Денотационный подход состоит в определении семантики языка путем подстановки каждому выражению соответствующего элемента из множества денотатов функции интерпретации символов сигнатуры языка. Каждой константе , функциональному символу и предикатному символу сопоставляется объект из множества денотат. Этот способ интерпретации семантики выражений и операторов языка аналогичен денотационной семантики ЯП. Главное отличие семантики КЯ от семантики программ - это ее неконструктивность. С каждым КЯ можно связать некоторую дедуктивную теорию, которая отражает свойства концепторов.
Формальная дедуктивная теория строится путем выделения из множества всех формул подмножества аксиом и правил вывода. Для каждой пары , формул дедуктивной теории и каждого оператора создается операторная формула с утверждением, что если истинно перед выполнением оператора , то завершение оператора обеспечивает истинность , т.е. формула - предусловие, а - постусловие оператора . С помощью неконструктивных объектов и неразрешимых формул этой теории можно адекватно описывать свойства неэффективных процедур.
Аксиоматическое описание КЯ - это аксиомы и утверждения относительно концепторного описания и проведения дедуктивного доказательства и верификации этого описания.
Логико-алгебраические спецификации.При использовании этих спецификаций ПрО представляется в виде алгебраической системы с помощью соответствующих носителей, сигнатуры и трех принципов. Первый принцип - логико-алгебраическая спецификация ПрО и уточнение понятий ПрО, второй принцип - описание свойств ПрО в виде аксиом, которые формулируются вязыке предикатов первого порядка и хорновских атомарных формул, и, наконец, третий принцип - это определение термальных моделей из основных термов спецификации. Логико-алгебраические спецификации можно ограничить хорновскими формулами из-за простоты аксиом и для упрощения процесса автоматического доказательства теорем. Отношения в сигнатурах спецификаций заменяются булевыми функциями.
Техника доказательного проектирования. Средства концепторной спецификации сложных, алгоритмически не разрешимых задач положены в основу формализованного описания поведения дискретных систем. Для описания свойств аппаратнопрограммных средств динамических систем применяются логико-алгебраические спецификации КЯ, техника описания которых включает два этапа.
На первом этапе дискретная система рассматривается как черный ящик с конечным набором входов, выходов и состояний. Области значений входов и выходов - произвольные, а функционирование системы S - это набор частичных отображений и операций алгебраической системы. Они образуют частичную алгебру,формальное описание которой выполняется с помощью алгебраических спецификаций и является программой моделирования состояний дискретной системы.
На втором этапе система детализируется в виде совокупности взаимозависимых подсистем , каждая из которой описывается алгебраической спецификацией. В результате получается спецификация системы из функций переходов и выходов, для которых необходимо доказывать корректность. Процесс детализации выполняется на уровне элементной базы или элементарных программ и сопровождается доказательством их корректности. В конечном итоге получается система S, эквивалентная исходной спецификации. Примеры доказательства систем приведены в [6.17]. Рассмотрим один из них.
Пусть требуется построить спецификацию натуральных чисел из множества этих чисел с сигнатурой операций . При построении используется число и функция следования . Спецификация состоит из следующих аксиом:
1. ,
2. ,
3. ,
4. ,
5. ,
6.
7.
При этом алгебраические системы становятся многоосновными алгебрами, а аксиомы - спецификациями: тождественными и квазитождественными. Алгебраические спецификации - наиболее используемые, поскольку для них существуют эффективные алгоритмы выполнения, которые преобразуют спецификации в ЯП высокого уровня. Поэтому такие языки называют языками выполняемых логико-алгебраических спецификаций. Их операционная семантика основана на переписывании термов, а создаваемая алгебраическая спецификация получает логическую семантику, используемую при доказательстве теорем.