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