5872

Формальные методы спецификации программ

Книга

Информатика, кибернетика и программирование

В предлагаемом учебном пособии рассматриваются два основных метода формального описания программных систем: метод алгебраических спецификаций и метод типизированных машин абстрактных состояний. Первый метод предназначен для описания статических аспе...

Русский

2012-12-23

431.5 KB

72 чел.

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

Пособие рассчитано на студентов 3-4 курсов, специализирующихся в области информатики.


Введение

Формальный метод в разработке программы – это математически обоснованная методика описания свойства программы. Альтернативой ему является неформальный метод, основанный, как правило, на опыте и интуиции конкретного программиста. Используя формальный метод, разработчик программы может специфицировать, спроектировать, написать и проверить программу некоторым систематическим образом в противовес использованию неформального метода, чреватому ошибками, двусмысленностями и недомолвками.

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

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

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

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

Во второй главе дается введение в алгебраические спецификации, являющиеся основой большинства функциональных языков спецификаций. Здесь вводятся понятия сигнатуры как средства синтаксического описания основных компонентов предметной области и алгебры как средства задания семантики имен, определенных в сигнатуре. Если сигнатура – это некоторое множество имен множеств и множество имен функций, то алгебра – это семейство конкретных множеств и семейство конкретных функций. В принципе для данной сигнатуры можно построить любое количество алгебр. Чтобы ограничить множество алгебр теми алгебрами, которые могут представлять описываемую предметную область (систему, программу), сигнатуру сопровождают рядом аксиом, задающих свойства, которые должны выполняться в каждой алгебре данной сигнатуры. Пара <сигнатура, множество аксиом> и есть алгебраическая спецификация.

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

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

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


1. Задачи формального метода в разработке программ

Чтобы изучать методы, устанавливающие правильность программы, имеет смысл рассмотреть модель того, что означает правильность программы. Мы разыскиваем некий процесс, устанавливающий правильную реализацию программой некоторой концепции, существующей в мыслях некоторого субъекта. Концепция обычно может быть реализована многими программами, но только небольшое количество из них имеет практическое значение. Эта ситуация изображена на рис. 1.

                                

   

Рис. 1. Концепция и множество реализующих ее программ

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

При формальных методах между концепцией и программой вводится промежуточное звено – спецификация. Цель этого звена –обеспечить математическое описание концепции и позволить установить правильность программы путем доказательства эквивалентности программы этой спецификации. Эта ситуация изображена на рис. 2.

                                

   

Рис. 2. Концепция, ее формальная спецификация и множество реализующих ее программ

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

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

1.1. Категории пользователей спецификаций

Основными пользователями формальной спецификации являются:

1) спецификатор – лицо, составляющее спецификацию;

2) реализатор – лицо, пишущее программу;

3) верификатор – лицо, доказывающее соответствие программы спецификации;

4) клиент – лицо, использующее программу.

Взаимодействие этих лиц изображено на Рис.3.

                                                                                             что

                                                                                             делает

                                                                                            программа?

                                                                                клиент

                                                                                                    

                                                                                                                                              

                                                                                                                                                     

     

   заказчик                      спецификатор       реализатор

                                                                                                                           

                                                                                                                           

                                                                                   реализует

                                                                                   программа

                                                                                       спецификацию?

                                                                      верификатор

Рис. 3. Взаимодействие пользователей спецификации

1.2. Назначение спецификации

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

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

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

4. Определение правильности реализации программы и эквивалентности различных реализаций. При этом совсем не обязательно привлечение аналитических методов проверки. Даже если проверка правильности программы осуществляется методом тестирования, возможно применение методик, основывающихся на сравнении формальной спецификации и реализации. Результатом такой методики может быть множество критических тестовых вариантов, которые устанавливают, что программа правильно реализует данную спецификацию. Формальность спецификации означает возможность привлечения вычислительной машины, например, для проверки шагов доказательства правильности программы или  для генерирования тестовых вариантов.

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

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

1.3. Проблемы формальных спецификаций

Формальная спецификация является всего лишь математическим представлением требований заказчика программы. Составляя ее, спецификатор интерпретирует неформальную постановку задачи заказчиком и записывает ее на некотором формальном языке спецификаций. В этом процессе возникают несколько проблем, которые могут привести к неверной спецификации.

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

Во вторых, спецификатор может допустить ошибки в спецификации. В этом отношении основными являются две следующие проблемы:

а) полнота – спецификатор может «забыть» описать некоторые части программы;

б) непротиворечивость – спецификатор может описать взаимно противоречивые свойства программы.

Чтобы устранить возможные ошибки подобного характера, спецификацию необходимо верифицировать. Эту работу выполняет верификатор (человек или программа).

1.4. Критерии оценки методов спецификаций

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

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

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

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

4. Минимальность. Спецификация должна описывать только те свойства концепции, которые интересуют заказчика, Эти свойства должны описываться точно и недвусмысленно, но так, чтобы при этом добавлялось как можно меньше посторонней информации. В частности, спецификация должна сообщать о том, какую функцию должна выполнять программа, но как можно меньше указывать на то, как эта функция выполняется. Одной из причин желательности этого критерия является то, что свойство минимальности минимизирует доказательство правильности программы путем уменьшения числа свойств, которые должны быть доказаны.

5. Применимость. С каждым методом спецификации может быть связан класс концепций, которые могут быть им описаны наиболее естественным и понятным образом, ведущим к спецификациям, удовлетворяющим критериям 2 и 3. Концепции, не принадлежащие этому классу, могут быть либо описаны только с большим трудом, либо не описаны вообще (например, концепции, содержащие параллелизм, не могут быть описаны методом, не содержащим соответствующих конструкций). Ясно, что чем больше класс концепций, легко описываемых данным методом, тем более он полезен. Универсального метода спецификаций, одинаково хорошо применимого для описания широкого круга разнообразных концепций, однако, не существует.

6. Эластичность. Желательно, чтобы минимальные изменения концепции приводили к столь же минимальным изменениям спецификации. Этот критерий особенно влияет на конструктивность спецификаций.


2. Алгебраические спецификации

Алгебраические спецификации сейчас находят все более широкое применение как мощный и удобный формальный метод описания языков программирования и программных систем. Этот метод основывается на традиционных понятиях многоосновных алгебр и впервые был применен к проблеме спецификации абстрактных типов данных в середине 70-х гг. Позднее он был распространен и на некоторые другие конструкции языков программирования и применен для спецификации баз данных. На основе алгебраическим методов было разработано несколько языков спецификаций, наиболее известными из которых являются CLEAR, ASL, OBJ2 и Larch. Последние разработки в этой области – языки спецификаций  Spectrum, Руслан и CASL. Сначала мы подробно рассмотрим чисто алгебраический подход.

2.1. Основные определения

2.1.1. Сигнатуры и алгебры

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

Определение 1. Пусть

 S есть множество (имен основ),

 профиль операции есть либо имя из S, либо

 S1,S2,...,Sn ® Sn+1, где Si, i = 1,...,n+1,имя из S.

 сигнатура операции есть op: O, где op – символ (знак или имя)

 операции, а  O – профиль операции;

тогда сигнатура S – это пара <S, W>, где W – множество сигнатур операций.

 Нотация:

1) сигнатуры операций разделяются точкой с запятой;

2) если O - профиль операции и op1,...,opn - символы операций,

 пишется op1,...,opn:O вместо op1:O; ... ;opn:O;

3) знаки операций (в противовес именам операций) заключаются в

 кавычки.  

 Пример:

{Boolean, Nat, SeqOfNat

{true, false: Boolean;

"": Boolean ® Boolean;

"|","&": Boolean,Boolean ® Boolean;

"=","<>": Boolean,Boolean ® Boolean;

zero: Nat;

succ: Nat ® Nat;

"+","-": Nat,Nat ® Nat;

"=","<>","<","<=",">",">=": Nat,Nat®Boolean;

empty: SeqOfNat;

append: Nat,SeqOfNat ® SeqOfNat;

head, length: SeqOfNat ® Nat;

tail: SeqOfNat ® SeqOfNat;

has: SeqOfNat,Nat ® Boolean;

 is_empty: SeqOfNat ® Boolean.

Сигнатуры являются чисто синтаксическими образованиями, и от них мало пользы до тех пор, пока не будет придан смысл употребляемым в них именам (т. е. пока не будет задана семантика имен). Именам основ надо сопоставить конкретные множества, а именам операций – конкретные функции. "Осмысление" сигнатуры приводит к алгебре. Задание конкретной алгебры для данной сигнатуры будем называть реализацией сигнатуры. Так, например, реализация части приведенной выше сигнатуры средствами "машинного" языка некоторой ЭВМ могла бы выглядеть следующим образом:

представление Boolean = {0, 1;

Nat = {множество комбинаций битов ячейки памяти};

операции

false: Boolean = 0;

true: Boolean = 1;

"": function(p: Boolean)Boolean =

  "if p = 0 then 1 else 0";

"|": function(p,q: Boolean)Boolean =

 "if p = 0 then (if q = 0 then 0 else 1) else 1;

"&": function(p,q: Boolean)Boolean =

 "if p = 1 then (if q = 1 then 1 else 0) else 0;

"=": function(p,q: Boolean)Boolean =

 "if p = 1 then (if q = 1 then 1 else 0)

  else if q = 0 then 1 else 0;

"<>": function(p,q: Boolean)Boolean =

 "if p = 1 then (if q = 1 then 0 else 1)

  else if q = 0 then 0 else 1;

 zero: Nat = "нулевая ячейка памяти";

 succ: function(n:Nat)Nat = "команды сложения(n,1)";

"+": function(m,n:Nat)Nat = "команды сложения(m,n)";

"-": function(m,n:Nat)Nat = "команды вычитания(m,n)";

"=": function(m,n:Nat)Boolean = "сравнение(m,n)";

 . . . 

Здесь с основой Boolean связывается множество из двух битов 0 и 1, одно из которых затем сопоставляется константе false, а другое – константе true. Основе Nat сопоставляется множество комбинаций битов ячейки памяти, из которых комбинация с нулями по всем битам выбирается в качестве значения константы zero. Каждой сигнатуре операции сопоставляется соответствующая машинная команда. Заметим, что в реализации операций как аргументы, так и результаты операций являются объектами представляющих множеств. Таким образом, выражаясь неформально, можно сказать, что алгебра – это пара функций, одна из которых отображает имена во множества, а другая – символы операций в функции. Если множество S содержит одну основу, алгебра называется одноосновной, в противном случае – многоосновной.

Для иллюстрации одноосновных алгебр образуем следущую сигнатуру целых чисел:

 <{number;

 {zero,one: number;

 plus,times: number,number number>

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

представление number = {0, 1, 2, 3};

операции

zero = 0;

one = 1;

plus =  0  1  2  3

   -----------------

   0 | 0  1  2  3

   1 | 1  2  3  0

   2 | 2  3  0  1

   3 | 3  0  1  2

times =   0  1  2  3

   -----------------

   0 | 0  0  0  0

   1 | 0  1  2  3

   2 | 0  2  0  2

   3 | 0  3  2  1

У этой алгебры всего одна основа number, представляющая множество из четырех объектов.

Определение 2. Алгебра А сигнатуры S = <S, W> строится путем сопоставления

1) множества элементов каждому имени из S;

2) элемента из множества SA – каждому символу операции из

   сигнатуры операции вида op: S, где SA – множество,

  сопоставленное имени S;

3) функции из (S1A  ...  S1A ® Sn+1A) – символу операции из

  сигнатуры операции вида op: S1,S2,...,Sn ® Sn+1, где

   SiA,  i = 1,...,n, – множество, сопоставленное имени Si.

Нотация: Если A есть алгебра сигнатуры S = <S, W>, тогда |A| – семейство множеств, сопоставленных именам из S, называемое носителем A. Любое a|A| называется элементом алгебры A.  Если op - символ операции, тогда opA – элемент носителя или функция, сопоставленная op в алгебре A.

2.1.2. Термы

Для данной сигнатуры S может быть построено сколько угодно алгебр. Среди них выделяется одна специальная алгебра, называемая алгеброй термов. Пусть Xs есть множество переменных основы S. Тогда элементы этой алгебры, называемые термами, определяются следующим образом.

Определение 3. Понятие терма:

1) если x – переменная основы S, тогда x – терм основы S;

2) если op: S – сигнатура операции, тогда op  терм основы S;

3) если op: S1,...,Sn ® S – сигнатура операции и e1,...,en – тер

  мы основ S1,...,Sn соответственно, тогда op(e1,...,en) – терм

  основы S.

Термы часто называют выражениями, а входящие в них символы операций – конструкторами выражений. Алгебра термов сигнатуры S на множестве переменных Х обозначается WS(X). Терм без переменных называется замкнутым термом. Множество всех термов основы S обозначается |WS(X)|s, а множество замкнутых термов основы S|WS|s; множества всех термов и всех замкнутых термов обозначаются |WS(X)| и |WS| соответственно. Примеры:

1. замкнутые термы основы Boolean:

 false,  true,  false & true, zero = Succ(zero),

 has(empty,zero);

2. замкнутые термы основы Nat:

 zero,  succ(zero),  head(append(zero,empty)),

length(append(zero,empty));

3. замкнутые термы основы SeqOfNat:

empty, append(zero,empty),

tail(append(zero,empty)).

 Операции алгебры термов строят более длинные термы из более коротких термов.

Для любой алгебры A данной сигнатуры S функция интерпретации (вычисления) 

 evalA = |WS(X)|s ® SA

определяется следующим образом:

1) для переменной xÎXs и функции означивания v: Xs ® |A|s:

 evalA(x) = v(x);

2) для символа c из сигнатуры операции c:S : evalA(c) = cA,

3) для символа op из сигнатуры операции op: S1,...,Sn ® S и

  термов t1,...,tn соответственно основ S1,...,Sn:

  evalA(op(t1,...,tn)) = opA(evalA(t1) ,...,evalA(tn)).

2.1.3. Гомоморфизмы

Предположим, что имеется функция f из носителя одной S-алгебры в носитель другой S-алгебры (для многоосновной алгебры мы можем считать, что имеется такая функция для каждой основы) с тем свойством, что если вычисление некоторого терма в первой алгебре дает результат а, то вычисление этого терма во второй алгебре дает результат f(a). В общем случае действие такой функции заключается в том, что если в первой алгебре вычисление выражения вида plus(x,times(x,y)) с привязкой переменной х к значению а и y к значению b дает результат с, тогда во второй алгебре вычисление этого терма с привязкой х к f(a) и у к f(b) дает результат f(c). Про такую функцию f говорят, что она является гомоморфизмом из первой алгебры во вторую.

Если, например, в сигнатуре целых чисел создать алгебру Mod2 с {0, 1} в качестве носителя и с очевидными операциями сложения и умножения, тогда гомоморфизм f из алгебры Mod4 в алгебру Mod2

f: Mod4  Mod2

выглядит следующим образом:

 f(0) = 0;  f(1) = 1;  f(2) = 0;  f(3) = 1.

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

 f(zero) в Mod4  =  zero в Mod2;

 f(one) в Mod4  =  one в Mod2;

 f(plus(m,n)) в Mod4  =  plus(f(m),f(n)) в Mod2;

 f(times(m,n)) в Mod4  =  times(f(m),f(n)) в Mod2.

 Это свойство соответствия результатов операций принимается в качестве формального определения гомоморфизма.

Определение 4. Если S = <S, W>, тогда S-гомоморфизм из S-алгебры А в S-aлгебру А' есть такое семейство отображений f: |A| ® |A'|, что для всех w  Wus и всех а1  S1A,...,an  SnA, имеет место:

 fs(w(a1,...,an)) = w(fS1(a1),...,fSn(an)), где

 u = S1...Sn,  Si  S,  i = 1,...,n,  fs: SA ® SA’,  

 fs1: S1A ® S1A’,..., fsn: SnA ® SnA’.

 Создадим в сигнатуре целых чисел алгебру Четность с {чет, нечет в качестве основы и очевидными операциями сложения и умножения, так что plus(чет,чет) = чет, plus(чет,нечет) = нечет и т. д. Тогда функция f из алгебры Mod2 в алгебру Четность, определяемая как

 f(0) = чет  и f(1) = нечет

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

 g(чет) = 0  и g(нечет) = 1.

В таком случае говорят, что функции f и g определяют изоморфизм между алгебрами Mod2 и Четность. Обозначим через 1A и 1B тождественные функции на носителях алгебр А и В (функция 1A отображает каждый элемент A в самого себя, функция 1B делает то же самое для алгебры В). Тогда изоморфизм между алгебрами A и В представляет собой пару взаимнообратных гомоморфизмов

f: A ® В и g: В ® A таких, что f*g = 1A и g*f = 1B. Другими словами, S-изоморфизм – это биективный S-гомоморфизм.

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

2.1.4. Инициальные и терминальные алгебры

Наличие отношения гомоморфизма между алгебрами естественно

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

Определение 5. I является инициальной S-алгеброй тогда и только тогда, когда для любой S-алгебры A существует единственный гомоморфизм f: I ® A.

Рассмотрим в качестве примера сигнатуру

 <{N,

 {z: N; s: N ® N}>.

Алгебрами этой сигнатуры являются:

Nat |Nat| = {0,1,2,...};

  z = 0; s(x) = x+1;

Mod2 |Mod2| = {0,1};

  z = 0; s(0) = 1; s(1) = 0;

Natnat |Natnat| = {0',1',2',...,

   0",1",2",... };

  z = 0'; s(0') = 1'; s(1') = 2'; ... ;

   s(0") = 1"; s(1") = 2"; ... ;

 Если мы захотим выбрать в качестве инициальной, например, алгебру NatNat, мы должны убедиться, что из нее есть единственный гомоморфизм в любую из других алгебр этой сигнатуры. Рассмотрим отображение NatNat в Nat. Операция z алгебры NatNat должна отображаться в z алгебры Nat, т. е. 0' отображается в 0, и по свойству гомоморфизма s(0') отображается в s(0), т. е. 1' отображается в 1 и т. д. Однако значение 0" алгебры NatNat может быть отображено в любое значение алгебры Nat, так как оно не связано с предыдущим рядом значений (оно вообще не связано ни с каким термом алгебры слов и возглавляет цепочку невычислимых значений алгебры NatNat). Вследствие этого существует больше одного гомоморфизма из NatNat в Nat, и потому NatNat не является инициальной алгеброй. Таким образом, инициальная алгебра не может содержать "хлама", т. е. невычислимых значений. Алгебры с таким свойством принято называть минимальными, или терм-порожденными (term-generated, finately-generated, computation structures).

Определение 6. Алгебра А называется минимальной, если каждый элемент ее носителя может быть получен вычислением некоторого замкнутого терма t|WS|.

В рассмотренном примере минимальными будут, очевидно, алгебры Nat и Mod2. Mod2, однако, не может быть инициальной алгеброй, поскольку из нее вообще не существует гомоморфизма, скажем, в алгебру Nat. Действительно, поскольку z алгебры Mod2 должен отображаться в z алгебры Nat, 0 алгебры Mod2 отображается в 0 алгебры Nat и далее по свойству гомоморфизма s(0) отображается в s(0), 1 отображается в 1, s(1) отображается в s(1) и 0 отображается в 2. Но поскольку 0 уже отображался в 0, получается коллизия, не совместимая с гомоморфизмом. Эта коллизия вызывается тем, что в алгебре Mod2 значение 0 вырабатывается при вычислении двух замкнутых термов: z и s(s(z)). Наилучшим кандидатом на звание инициальной является алгебра Nat, так как у нее нет невычислимых элементов (каждый элемент носителя является результатом вычисления некоторого терма) и нет коллизий (вычисление различных термов дает различные значения). Поскольку мы можем построить взаимно однозначное отображение между алгеброй Nat и алгеброй термов, следует считать алгебру Nat изоморфной алгебре термов. Из этого напрашивается:

Гипотеза 1. Инициальная алгебра изоморфна алгебре термов.

Для подтверждения этой гипотезы докажем две теоремы.

Теорема 1. Если I и I’ являются инициальными S-алгебрами, они изоморфны.

Доказательство. Поскольку I и I’ являются инициальными S-алгебрами, существуют гомоморфизмы f: I ® I’ и g: I’ ® I. Тогда гомоморфизмами являются и композиции f*g: I ® I и g*f: I’ ® I’. Из определения тождественных функций 1I: I ® I и 1I': I’ ® I’ следует, что f*g = 1I и g*f = 1I'. Таким образом, f и g обратны и, следовательно, I и I’  изоморфны.

Теорема 2. Алгебра слов является инициальной алгеброй.

Доказательство. Доказательством является определение функции интерпретации eval (раздел 2.1.2).

Таким образом, гипотеза 1 является верной, и в рассмотренном примере алгебра Nat – инициальная.

Дуальным понятием по отношению к инициальной алгебре является терминальная (финальная) алгебра.

Определение 7. Алгебра J является терминальной S-алгеброй, если для любой S-алгебры A существует единственный гомоморфизм g: A ® J.

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

2.1.5. Аксиомы

При наличии множества алгебр одной и той же сигнатуры естест-

венно возникают вопросы выделения из них таких алгебр, операции которых подчиняются определенным законам, как, например, ассоциативность и коммутативность. Эти законы могут быть выражены в виде равенств. Равенство на множестве переменных данной сигнатуры представляет собой не что иное, как пару термов с переменными. Например, равенство plus(x,y) = plus(y,x) на множестве переменных {x,ynumber} может рассматриваться как тройка

 <{x,ynumber, plus(x,y), plus(y,x)>.

Определение 8. S-равенство E - это тройка <X, t1, t2>, где X - S-индексированное множество (переменных), а t1,t2 - термы одной основы на множестве переменных X.

Равенства дают основу для классификации алгебр. Если в алгебре выполняется, скажем, равенство е1(x,y) = е2(х,y), то это означает, что, каковы бы ни были значения, приданные переменным х и у, при одних и тех же значениях x и у в обеих частях равенства вычисление терма в левой части дает тот же результат, что и вычисление терма в правой части. В общем виде:

Определение 9. В S-алгебре A выполняется S-равенство <X,t1,t2>, если для всех отображений f: X ® A выполняется t1A = t2A.

В дальнейшем мы будем пользоваться более широким понятием аксиомы:

Определение 10. Понятие аксиомы:

  1.  если t1 и t2  термы основы S, тогда t1==t2  это равенство, или  аксиома;
  2.  если A - аксиома, тогда forall x1:S1,...,xn:Sn. A, где xi

переменная и Si - имя основы, есть аксиома;

  1.  если A  аксиома, тогда exist x1:S1,...,xn:Sn.A, где xi

переменная и  Si  имя основы, есть аксиома;

  1.  аксиома содержит только переменные, связанные

квантификаторами forall и exist (т. е. в аксиоме вида t1==t2 и

 t1, и t2  базисные термы).

Определение 11. Аксиома t1==t2 выполняется в данной алгебре, если интерпретация t1 и t2 приводит к одному и тому же элементу соответствующей основы при всех значениях переменной, связанной квантификатором forall, и хотя бы при одном значении переменной, связанной квантификатором exist.

Нотация: все связанные переменные перечисляются в начале списка аксиом.

2.1.6. Теории

Пусть E  множество равенств. Будем говорить, что некоторая алгебра является моделью E, если в ней выполняется каждое равенство из E. Обозначим E* множество моделей E.

При наличии некоторого множества алгебр М мы можем рассматривать множество равенств, выполняющихся в каждой алгебре из этого множества. Обозначим такое множество M*. Тогда E** является множеством всех равенств, описывающих модели E, и называется замыканием E.

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

 основы {лица};

 операции {Иванов, Петров, Сидоров: лица};

 равенства {Иванов == Петров;

  Петров == Сидоров}.

Предположим теперь, что имеются алгебры с элементами p1, p2, p3,... каким-то образом сопоставленными указанным константам. В тех алгебрах, в которых Иванов, Петров и Сидоров имеют одно и то же значение, выполняются данные равенства. Но если в какой-то алгебре выполняется данная пара равенств, в ней выполняется и равенство Иванов == Сидоров. Таким образом, это равенство входит в логическое замыкание.

Сигнатура с множеством равенств называется представлением. Множество равенств называется замкнутым, если его замыканием является само это множество. Сигнатура с замкнутым множеством равенств называется теорией.

Определение 12. Представление это пара <S, E>, где S - сигнатура, а E - множество аксиом.

Определение 13. Теория это такое представление <S, E>, в котором E замкнуто.

Пример.

{Boolean, Nat, SeqOfNat}

{true, false: Boolean;

 "": Boolean ® Boolean;

 "|","&": Boolean,Boolean ® Boolean;

 "=","<>": Boolean,Boolean ® Boolean;

 zero: Nat;

succ: Nat ® Nat;

 "+", "-": Nat,Nat ® Nat;

 "=","<>","<","<=",">",">=": Nat,Nat ® Boolean;

empty: SeqOfNat;

append: Nat,SeqOfNat ® SeqOfNat;

head, length: SeqOfNat ® Nat;

tail: SeqOfNat ® SeqOfNat;

has: SeqOfNat,Nat ® Boolean;

is_empty: SeqOfNat ® Boolean;

"=", "<>": SeqOfNat,SeqOfNat ® Boolean},

{forall p,p1: Boolean, x,y: Nat, s,s1: SeqOfNat.

 true == false;

 false == true;

false & p == false;

true & p == p;

false | p == p;

true | p == true;

p = p == true;

true = false == false;

p <> p1 ==  (p = p1);

x < x == false;

zero < succ(x) == true;

succ(x) < zero == false;

succ(x) < succ(y) == x < y;

x = x == true;

zero = succ(x) == false;

succ(x) = zero == false;

succ(x) = succ(y) == x = y;

x <= y == x < y | x = y;

x > y == y < x;

x >= y == y =< x;

x <> y ==  (x = y);

x + zero == x;

x + succ(y) == succ(x + y);

x - zero == x;

succ(x) - succ(y) == x - y;

is_empty(empty) == true;

is_empty(append(x,s) == false;

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

head(append(x,s)) == x;

has(empty,x) == false;

has(append(y,s),x) == x = y | has(s,x);

tail(append(x,s)) == s;

append(x,s) = empty == false;

empty = append(x,s) == false;

append(x,s) = append(y,s1) == x = y & s = s1;

 s <> s1 ==  (s = s1)}.

Когда задается множество аксиом как в приведенном выше примере фактически строится представление, так как многие аксиомы могут быть выведены из заданных. Например, если в алгебре выполняется аксиома, скажем, false&p == false, в ней также выполняется аксиома, скажем, false&(true&p) == false. Так что обычно имеется в виду представление, когда говорится о теории. Ниже для этих целей используется более нейтральный термин спецификация. Спецификации, аксиомы которых используют только равенства, принято называть эквациональными.

Определение 14. S-алгебра A называется моделью спецификации U = <S, E>, если в ней выполняется каждая аксиома из Е.

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

2.1.7. Модели спецификаций

Мы можем теперь определить понятия, аналогичные инициальной и терминальной алгебре, по отношению к моделям данной спецификации. В приведенном выше примере при отсутствии равенств термы false и true&false в алгебре термов данной сигнатуры рассматривались бы как различные. В соответствии с этим любая инициальная алгебра данной сигнатуры должна была бы иметь разные элементы для этих термов, а терминальная - один и тот же элемент. Наличие приведенной системы аксиом заставляет считать моделями данной спецификации только такие алгебры, у которых термы, подобные термам false и true&false, отображаются в один и тот же элемент носителя. Таким образом, задание системы аксиом позволяет сформировать классы эквивалентности термов и тем самым определить в качестве инициальных и терминальных "более реальные" алгебры, отвечающие тому, что разработчик спецификации "имел в виду". Определения инициальной и терминальной алгебры будут в этом случае выглядеть следующим образом:

Определение 15. Алгебра I является инициальной алгеброй данной теории тогда и только тогда, когда для любой алгебры А этой теории существует единственный гомоморфизм f: I  A.

Определение 16. Алгебра J является терминальной алгеброй данной спецификации тогда и только тогда, когда  для любой алгебры A этой теории существует единственный гомоморфизм g: A  J.

Наиболее простой способ получения инициальной алгебры данной теории заключается в том, чтобы на основе заданной системы аксиом сформировать в алгебре термов классы эквивалентности по отношению конгруэнтности (т. е. если термы t1 и t2 принадлежат одному классу эквивалентности, то для любого унарного w термы w(t1) и w(t2) также принадлежат одному классу эквивалентности; то же самое для операций с несколькими аргументами). Каждому классу эквивалентности в инициальной алгебре сопоставляется отдельный элемент носителя, вследствие чего инициальная алгебра имеет "наибольший" носитель среди всех алгебр данной теории. В этом смысле инициальная алгебра является наиболее расточительной в смысле расхода ресурсов.

В зависимости от подхода к определению множества моделей данной спецификации различают мягкие (loose), минимальные (generated) и свободные (free) модели. Моделью мягкой спецификации является любая алгебра, в которой удовлетворяются аксиомы спецификации. Такая алгебра может, напрмер, содержать мусорные элементы, которые не соответствуют никаким термам данной сигнатуры. Моделью минимальной спецификации может являться только алгебра, не содержащая мусорных элементов (т.е. алгебра, содержащая минимально возможное количество элементов носителя). Моделью свободной спецификации может являться только инициальная алгебра данной теории, в которой разным классам эквивалентности термов сопоставляются разные элементы носителя. Например, если приведенная выше спецификация считается минимальной, то допустима модель, в которой термы true и false отображаются в один и тот же элемент носителя; в модели свободной спецификации это невозможно.

2.1.8. Обработка ошибок

Операция может произвести неопределенный результат в двух случаях:

1) она не применима к некоторым аргументам (классическим примером является top(empty) для стеков);

2) она применяется к неопределенному аргументу (в случае стека это может быть push(top(empty)),x).

В приведенном выше примере если Nat  это множество натуральных чисел, а SeqOfNat  множество последовательностей натуральных чисел, не определены результаты вычисления выражений x-y, если x<y, head(empty) и tail(empty).

Таким образом, составляя спецификацию, необходимо каким-то способом явно указать все случаи неприменимости операции. Существует несколько подходов к решению данной проблемы. Среди них наиболее известны алгебры с ошибочными элементами (error algebras), частичные алгебры (partial algebras) и алгебры с упорядоченными основами (order-sorted algebras).

Алгебры с ошибочными элементами

Основная идея снабдить каждую основу константой error и каждую алгебру так называемым предикатом ОК, сообщающим, что данный элемент алгебры не является ошибочным. Пусть SP = <S, E>, где S = <S, W>, некоторая эквациональная спецификация, содержащая эквациональную спецификацию булевских значений в качестве подспецификации. Тогда спецификация с ошибочными константами S = < Sе, Eе> определяется на Sе = <S, Wе>, где  Wе расширяет W добавлением следующих сигнатур операций к каждой основе S  S:

 errors: S   константа “error” ;

oks: S ® Boolean  предикат ОК ;

ifes: Boolean, S, S ® S  if-then-elSe.

содержит следующие аксиомы:

ifes(true, x, y) == x;

ifes(false, x, y) == y;

ifes(errorbool, x, y) == errors;

oks(errors) == false;

oks(f(x1,...,xn)) == oks1(x1)&...&oksn(xn)&

   c(x1,...,xn),

 где c(x1,..., xn)|WS({x1,..., xn})|Boolean  

 предикат OK, примененный к терму f(x1,...,xn),

выполняется, если он выполняется для каждого

аргумента и истинен булевский терм c(x1,...,xn),

определяющий домен функции f.

f(x1,...,  errorsi,..., xn) == errors;  для

каждой f: S1,..., Sn ® S.

 Пример. Дополним фрагмент предыдущей спецификации ошибочными элементами для основы SeqOfNat:

{empty,errorson: SeqOfNat;

append: Nat,SeqOfNat ® SeqOfNat;

head,length: SeqOfNat ® Nat;

tail: SeqOfNat ® SeqOfNat;

has: SeqOfNat,Nat ® Boolean;

is_empty,okson: SeqOfNat ® Boolean;

ifeson: Boolean,SeqOfNat,SeqOfNat ® SeqOfNat},

{forall p: Boolean, x,y: Nat, s,s1: SeqOfNat.

is_empty(errorson) == errorbool;

is_empty(empty) == true;

is_empty(append(x,s)) ==

 ifebool(oknat(x)&okson(s), false, errorbool);

length(errorson) == errornat;

length(empty) == 0;

length(append(x,s)) ==

ifenat(oknat(x)&okson(s), length(s)+1, errornat);

head(errorson) == errornat;

head(empty) == errornat;

head(append(x,s)) ==

 ifebool(oknat(x)&okson(s), s, errornat);

has(empty,x) == ifebool(oknat(x), false, errorbool);

has(append(y,s),x) ==

 ifebool(oknat(x)&oknat(y)&okson(s),

  (x=y|has(s,x)), errorbool);

tail(errorson) == errorson;

tail(empty) == errorson;

tail(append(x,s)) ==

 ifeson(oknat(x)&okson(s), s, errorson);

ifeson(errorbool,s,s1) == errorson;

ifeson(true,s,s1) == s;

ifeson(false,s,s1) == s1;

okson(errorson) == false;

okson(empty) == true;

okson(append(x,s)) == oknat(x) & okson(s);

oknat(head(s)) == okson(s) & is_empty(s);

okson(tail(s)) == okson(s) & is_empty(s)}.

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

Частичные алгебры

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

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

для символа op из сигнатуры операции op: S1,...,Sn ® S и

 термов t1,...,tn основ S1,...,Sn соответственно:

а) evalA(op(t1,...,tn)) =

 opA(evalA(t1),..., evalA(tn)),

 если evalA определена для терма ti и opA определена для

 кортежа evalA(t1),...,evalA(tn));

 б) evalA(op(t1,...,tn)) не определено в противном случае.

Терм, интерпретация которого в данной алгебре не определена, называется неопределенным.

Следующая проблема частичных алгебр - интерпретация булевых термов (мы по-прежнему считаем, что каждая спецификация содержит основы Boolean с введенными выше константами true и false и соответствующими операциями). Пусть, например, мы имеем булев терм iS_empty(tail(empty)). Если tail - частичная функция, то терм tail(empty) не определен и в соответствии с пунктом 3 функции интерпретации не определен терм is_empty(tail(empty)). Таким образом, мы получаем трехзначную логику (интерпретация терма может выработать true или false, или она может быть не определена). В этом случае необходимо как-то обозначать неопределенное значение и переопределять обычные булевы операции для учета третьего значения. Все это существенно усложняет спецификацию. Чтобы остаться в рамках двузначной логики, мы будем считать все булевы функции тотальными и введем специальное правило интерпретации булевых термов:

для символа op: S1,...,Sn ® Boolean и термов t1,...,tn основ S1,...,Sn соответственно:

а) evalA(op(t1,...,tn)) = trueA, если evalA определена

 для всех ti, и (evalA(t1),..., evalA(tn)) opA;

б) evalA(op(t1,...,tn)) = falseA в противном случае.

В частичной алгебре возникает также проблема интерпретации равенства t1==t2. Дело в том, что если в состав термов t1 и t2 входят символы частичных функций, то один из этих термов или оба терма могут быть неопределенными в данной алгебре. Естественный вопрос как считать, удовлетворяется ли такое равенство в данной алгебре или нет. Существует два подхода к ответу на этот вопрос, называемые соответственно строгостью равенства (strong equation) и существованием равенства (existential equation). При строгости равенства  считается, что оно удовлетворяется в данной алгебре, если обе его части не определены или определены обе и их интерпретация приводит к одному и тому же элементу алгебры. При существовании равенства  считается, что оно удовлетворяется в данной алгебре, если только обе его части определены и их интерпретация приводит к одному и тому же элементу алгебры. Мы впредь будем работать только со строгими равенствами.

 Замечание: интересно отметить, что знак равенства «=» определятся в типах данных согласно принципу существования, так как любая булева функция вырабатывает значение false, если хотя бы один ее аргумент неопределен.  

При составлении аксиом спецификации часто пользуются специальным предикатом D, служащим для записи формулы определенности D(t), где t|WS(X)|. Формула определенности D(t) истинна в частичной алгебре A, если интерпретация t в A определена. Мы будем интенсивно использовать формулы определенности в разделе 4, посвященном методам спецификации динамических систем.

Аксиому вида

 D(t1) == t2

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

 dom t1: t2;

Согласно общей семантике аксиом такое утверждение определенности удовлетворяется в данной алгебре А тогда и только тогда, когда из определенности t1 следует истинность t2 и наоборот.

 Замечание: если спецификация домена для какой-то операции отсутствует, соответствующая ей функция считается тотальной.

В соответствии с этой методикой приведенная выше спецификация (в части аксиом) должна быть дополнена следующими фразами:

 dom x-y: y <= x;

 dom head(s): is_empty(s);

 dom tail(s): is_empty(s).

2.2. Алгебраические структуры

Алгебраическая структура (или просто структура) является понятием, расширяющим понятие алгебры. В ней в дополнение к функциям вводятся предикаты, или отношения. Вследствие этого в сигнатуре структуры кроме сигнатур операций имеют место сигнатуры предикатов, записываемые следующим образом:

 p: S1,…,Sn;

где p – символ (имя) предиката, а S1,…,Sn – имена основ. В конкретной структуре М сигнатуре предиката p: S1,…,Sn сопоставляется отношение pМ: |S1|  |Sn|.

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

а) если p: S1,…,Sn – это сигнатура предиката и t1,…,tn – термы основ S1,…,Sn соответственно, тогда p(t1,…,tn) – это атомарная формула, называемая предикацией;

б) если t – это терм, тогда D(t) – это атомарная формула, называемая формулой определенности.

Предикация p(t1,…,tn) удовлетворяется в данной структуре М, если все термы t1,…,tn определены в ней и (t1M,…, tnM)  pM. Формула определенности D(t) удовлетворяется в данной структуре М, если терм t определен в ней.

Заметим, что, как и в случае интерпретации булевых термов, данной в предыдущем разделе, приведенная интерпретация предикации приводит нас к обычной двузначной логике (предикация не выполняется в структуре, т. е. вырабатывает false, если хотя бы один из аргументов не определен).

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

{sort Nat, SeqOfNat}

{func zero: Nat;

 func succ: Nat ® Nat;

 func "+", "-": Nat,Nat ® Nat;

 pred "=", "<>", "<", "<=", ">", ">=": Nat,Nat;

 func empty: SeqOfNat;

 func append: Nat,SeqOfNat ® SeqOfNat;

 func head,length: SeqOfNat ® Nat;

 func tail: SeqOfNat ® SeqOfNat;

 pred has: SeqOfNat,Nat;

 pred is_empty: SeqOfNat;

 pred "=", "<>": SeqOfNat,SeqOfNat},

{forall x,y,z: Nat, s,s1: SeqOfNat.

 (x < x);

zero < succ(x);

 (succ(x) < zero);

x < y    succ(x) < succ(y);

x = x;

 (zero = succ(x));

 (succ(x) = zero);

x = y    succ(x) = succ(y);

x = y & y = z    x = z;

x < y | x = y    x <= y;

x > y    y < x;

x >= y    y =< x;

x <> y    (x = y);

x + zero == x;

x + succ(y) == succ(x + y);

x - zero == x;

x >= y     succ(x) - succ(y) == x - y;

is_empty(empty);

 is_empty(append(x,s));

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

 D(head(empty));

head(append(x,s)) == s;

 has(empty,x);

has(append(y,s), x)    x = y | has(s,x);

 D(tail(empty));

tail(append(x,s)) == s;

 (append(x,s) = empty);

 (empty = append(x,s));

append(x,s) = append(y,s1)   x = y & s = s1;

 s <> s1    (s = s1)}.

Из примера видно, что при использовании формул нет необходимости приравнивать термы к константам true и false, что имеет место при использовании алгебр. В то же время расширяется круг используемых символов: кроме метасимвола равенства “==” используются метасимвол эквивалентности “” и метасимвол импликации “”. Заметим, что введение предикатов в алгебраическую структуру фактически эквивалентно введению в алгебру стандартной основы Boolean с соответствующими операциями. Однако предикаты не всегда заменяют булевы функции. Если, например, будет необходимо описать язык программирования, в котором имеется тип данных Boolean и возможность описания булевых функций, придется вводить в спецификацию соответствующую основу и  соответствующие операции, дублируя тем самым метаоперации, используемые для построения формул. Современным языком спецификаций, основанном на алгебраических структурах, является CASL (язык, созданный сообществом европейских ученых). Мы же в дальнейшем будем основываться на алгебрах, чтобы легче устанавливать параллели со структурами типов данных, свойственных современным языкам программирования.


3. Структурированные спецификации

Приведенную выше спецификацию не очень удобно конструировать и понимать, потому что она не структурирована, т. е. в ней сначала приведены все имена основ, затем – все сигнатуры операций и, наконец, – все аксиомы. Поэтому каждый язык спецификаций предоставляет возможность построения структурированных спецификаций, т. е. спецификаций, построенных из отдельных фрагментов. Так, например, CLEAR  содержит операторы для объединения теорий, являющихся основными структурными единицами языка. Модули (module expressions) языка OBJ2 могут импортировать другие модули. Язык ASL предоставляет несколько операций для построения более сложных спецификаций на основе более простых; то же самое относится и к языку CASL. Основное различие между способами структурирования заключается в выборе фрагмента спецификации.

Дополнительными возможностями структурирования спецификаций обладает язык Spectrum, позволяющий вводить классы основ (sort classes) и затем использовать их для построения параметризованных спецификаций. Еще большими возможностями структурирования спецификаций обладает язык Руслан, предоставляющий средства вертикального и горизонтального структурирования в виде спецификаций типов данных, объединенных типовыми родами (вертикальное структурирование) и типовыми классами (горизонтальное структурирование). Ниже будут рассмотрены средства горизонтального структурирования спецификаций в Руслане.

3.1. Типы данных

Рассматривая  приведенные  примеры  спецификаций,  нетрудно

заметить, что фактически с каждой основой связан определенный набор символов операций. Например, можно выделить набор операций, связанный с основой Boolean, набор операций, связанный с основой Nat, и набор операций, связанный с основой SeqOfNat.

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

<Boolean = spec 

[true, false: Boolean;

 "": Boolean ® Boolean;

"|", "&", "=>": Boolean,Boolean ® Boolean;

"=", "<>": Boolean,Boolean ® Boolean]

{forall p,p1: Boolean.

 true == false;

 false == true;

false & p == false;

true & p == p;

false | p == p;

true | p == true;

 false => p == true;

true => p == p;

p = p == true;

true = false == false;

p <> p1 == (p = p1)};

Nat = spec 

[zero: Nat;

succ: Nat ® Nat;

"+","-": Nat,Nat ® Nat;

"=","<>","<","<=",">",">=": Nat,Nat ® Boolean]

{forall x,y: Nat.

 dom x-y: y <= x;

x < x == false;

zero < succ(x) == true;

succ(x) < zero == false;

succ(x) < succ(y) == x < y;

x = x == true;

zero = succ(x) == false;

succ(x) = zero == false;

succ(x) = succ(y) == x = y;

x <= y == x < y | x = y;

x > y == y < x;

x >= y == y =< x;

x <> y == (x = y);

x + zero == x;

x + succ(y) == succ(x + y);

x - zero == x;

succ(x) - succ(y) == x – y};

SeqOfNat = spec 

[empty: SeqOfNat;

append: Nat,SeqOfNat ® SeqOfNat;

head,length: SeqOfNat ® Nat;

tail: SeqOfNat ® SeqOfNat;

has: SeqOfNat,Nat ® Boolean;

is_empty: SeqOfNat ® Boolean;

"=", "<>": SeqOfNat,SeqOfNat ® Boolean]

{forall x,y: Nat, s,s1: SeqOfNat.

 dom head(s): is_empty(s);

 dom tail(s): is_empty(s);

is_empty(empty) == true;

is_empty(append(x,s) == false;

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

head(append(x,s)) == x;

has(empty,x) == false;

has(append(y,s),x) == x = y | has(s,x);

tail(append(x,s)) == s;

append(x,s) = empty == false;

empty = append(x,s) == false;

append(x,s) = append(y,s1) == x = y & s = s1;

 s <> s1 == (s = s1)}>.

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

Мы можем заметить в примере, что каждая сигнатура типа данных содержит сигнатуры операций, каждая из которых использует и/или производит значение своего типа данных. Этот факт позволяет ответить на вопрос, какие сигнатуры операций должны быть включены в сигнатуру типа данных (было бы очень странно связывать с типом данных операцию, которая и не использует, и не производит его значения). Мы можем также заметить, что фактически нет необходимости употреблять имя типа данных внутри его спецификации, и потому можно использовать для этой цели специальный символ. Пусть это будет символ "@". Тогда наша спецификация приобретает следующий вид:

<Boolean = spec 

[true, false: @;

 "": @ ® @;

"|", "&", "=>": @,@ ® @;

"=", "<>": @,@ ® @]

{forall p,p1: @.

 true == false;

 false == true;

false & p == false;

true & p == p;

false | p == p;

true | p == true;

false => p == true;

true => p == p;

p = p == true;

true = false == false;

p <> p1 == (p = p1)};

Nat = spec 

[zero: @;

succ: @ ® @;

"+","-": @,@ ® @;

"=","<>","<","<=",">",">=": @,@ ® Boolean]

{forall x,y: @.

 dom x-y: y <= x;

x < x == false;

zero < succ(x) == true;

succ(x) < zero == false;

succ(x) < succ(y) == x < y;

x = x == true;

zero = succ(x) == false;

succ(x) = zero == false;

succ(x) = succ(y) == x = y;

x <= y == x < y | x = y;

x > y == y < x;

x >= y == y =< x;

x <> y == (x = y);

x + zero == x;

x + succ(y) == succ(x + y);

x - zero == x;

succ(x) - succ(y) == x – y};

SeqOfNat = spec 

[empty: @;

append: Nat,@ ® @;

head,length: @ ® Nat;

tail: @ ® @;

has: @,Nat ® Boolean;

is_empty: @ ® Boolean;

"=", "<>": @,@ ® Boolean]

{forall x,y: Nat, s,s1: @.

 dom head(s): is_empty(s);

 dom tail(s): is_empty(s);

is_empty(empty) == true;

is_empty(append(x,s) == false;

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

head(append(x,s)) == x;

has(empty,x) == false;

has(append(y,s),x) == x = y | has(s,x);

tail(append(x,s)) == s;

append(x,s) = empty == false;

empty = append(x,s) == false;

append(x,s) = append(y,s1) == x = y & s = s1;

 s <> s1 == (s = s1)}>.

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

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

Определение 17. Пусть

 TYPE есть множество имен (типов данных);

 профиль операции есть либо имя из TYPE, либо

 T1,T2,...,Tn ® Tn+1, где Ti – имя из TYPE; Ti называется

 символом домена, а Tn+1символом кодомена;

 сигнатура операции есть пара op:O, где op – символ операции, а

 O – профиль операции;

 сигнатура типа данных есть множество сигнатур операций,

 построенных как описано выше с расширением множества TYPE

 символом "@", означающим "я сам" и используемым по крайней

 мере один раз в качестве символа домена  и/или кодомена в

 каждой сигнатуре операции;

тогда типизированная сигнатура S – это тройка <TYPE, F, tsig>, где F – множество сигнатур типов данных, а tsig – функция, отображающая TYPE в F. Для каждого имени T  TYPE и сигнатуры типа данных f  F мы говорим, что f обозначено T, если tsig(T) = f.

К сигнатуре типа данных предъявляются следующие требования.

1. В ней должна быть хотя бы одна сигнатура операции с “@” в качестве символа кодомена. Операция с такой сигнатурой называется конструктором.

2. В сигнатуре операции с символом кодомена, отличным от “@”, символ “@” должен хотя бы раз использоваться в качестве символа домена. Операция с такой сигнатурой называется анализатором.

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

Пусть С будет множеством сигнатур конструкторов в сигнатуре типа данных Т. К нему дополнительно предъявляются следующие требования.

1. Множество С состоит из двух непересекающихся подмножеств ВС и SC.

2. Множество ВС не пусто, и существует хотя бы одна сигнатура операции

 с ВС, не имеющая  “@” в качестве символа домена.

3. В каждой с SC по крайней мере один символ домена есть “@”.

Элемент множества ВС называется базисным конструктором, а элемент множества SCвторичным конструктором. Таким образом, во множестве конструкторов всегда выбирается некоторое минимальное подмножество базисных конструкторов, способных породить любое значение данного типа. Эти конструкторы являются обязательным атрибутом типа данных. Вторичные конструкторы (если они есть) служат в основном для удобства пользователей. В приведенном выше примере спецификации типа данных Nat zero и succ – базисные конструкторы, "+" и "-" – вторичные конструкторы, а остальные операции – анализаторы. В будущем мы будем перечислять имена базисных конструкторов в специальной фразе generated by в конце сигнатуры типа данных. Отсутствие такой фразы будет означать, что все конструкторы – базисные.

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

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

 [op1: @ ® @;

  op2: @, @ ® Boolean]

бессмысленна, потому что не вводит операцию, способную породить некоторое исходное значение данного типа, а сигнатура типа данных

 [op1: @;

 op2: @ ® @]

бессмысленна, потому что не вводит операцию, способную проанализировать значения данного типа.

Сигнатура, построенная таким образом, обладает следующими преимуществами:

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

2. без особых проблем могут использоваться одни и те же символы операций в разных сигнатурах;

3. использование специального символа вместо имени типа данных в его сигнатуре позволяет анализировать сигнатуру типа данных, не привязываясь к конкретному имени типа данных, что дает возможность легко ввести понятия типового класса (раздел 3.4) и родового типа данных (раздел 3.5);

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

Нотация. Конструируя конкретную типизированную сигнатуру, мы фактически строим только функцию tsig как множество пар следующего вида: имя типа данных = sig сигнатура типа данных. Множество сигнатур операций в сигнатуре типа данных заключается в квадратные скобки.

Определение 18. Aлгебра A сигнатуры S = <TYPE, F, tsig> строится путем сопоставления:

1) множества элементов – каждому имени из TYPE;

2) элемента  из  множества  TA – каждому  символу  операции  ви-

 да op: T из сигнатуры типа данных T, где TA – множество,    сопоставленное имени T;

3) частичной функции из (T1A  ...  TnA ® Tn+1A) – символу опе

  рации вида op: T1,T2,...,Tn ® Tn+1 из множества fT, где fT 

  сигнатура типа данных T, модифицированная таким образом,

  что каждое вхождение символа "@" в T1,T2,...,Tn ® Tn+1 

  заменено на T.

Множество элементов, сопоставленное имени типа данных TTYPE, называется носителем значений типа T. Это множество вместе с функциями, сопоставленными символам операций из fT, называется реализацией типа T и обозначается Т(A). Носитель алгебры типизированной сигнатуры – это семейство носителей значений типов данных.

Определение 19. Пусть f: S1  Sn  S - частичная функция, определенная на множествах S, S1,…,Sn. Множество результатов функции Ran(f) образуется следующим образом: для каждого элемента ai  Si, i = 1,…,n, если f(a1,...,an) определено, тогда f(a1,..., an)  Ran(f). Для каждой константы c в данной алгебре A: Ran(cA) = {cA}.

Определение 20. Пусть c1A,…,cnA будут базисными конструкторами в реализации типа данных Т(A). Множество элементов Val(T)A = Ran(c1A) Ran(cnA) называется множеством значений типа данных Т в алгебре А.

Заметим, что в общем случае Val(T)A  ТA, т. е. не каждый элемент носителя типа данных может принадлежать множеству значений этого типа. Примером может служить представление значений типа Character посредством байта памяти, так как количество кодов, представляющих множество символов может быть меньше 256.

К реализации типа данных предъявляются следующие требования:

1. для каждого вторичного конструктора сA в реализации типа данных Т(A) должно быть Ran(cA)  Val(T)A, т. е. вторичный конструктор не может вырабатывать в качестве результата элемент носителя, не принадлежащий к множеству значений данного типа данных;

2. для каждого анализатора obA в реализации типа данных Т(A), вырабатывающего значение типа данных Т1, должно быть Ran(obA)  Val(T)A, т. е. анализатор не может вырабатывать в качестве результата элемент носителя, не принадлежащий к множеству значений типа данных, указанного в качестве кодомена.

В связи с тем, что мы заменили основы типами данных, переформулируем понятие терма, введя вместо понятия “терм основы S” понятие “терм типа Т”.

1) если x – переменная типа Т, тогда x – терм типа Т;

2) если c: @ сигнатура операции из сигнатуры типа данных,

  обозначенной именем Т, тогда c и T'c – термы типа Т,

3) если op: T1,...,Tn  @ сигнатура операции из сигнатуры

  типа данных, обозначенной именем T, и e1,...,en – термы

  типов T,...,Tn, соответственно, тогда op(e1,...,en) и

  T'op(e1,...,en) – термы типа T;

4) если op: T,...,Tn  Tn+1 сигнатура операции из сигнатуры

  типа данных, обозначенной именем T, и e1,...,en – термы

  типов T,...,Tn, соответственно, тогда op(e1,..., en) и

  T'op(e1,...,en) – термы типа Tn+1.

Замечание: иногда мы префиксируем терм именем типа данных, чтобы избежать неоднозначности (подобно тому как компонент класса в С++ может префиксироваться именем этого класса).

Множество всех термов типа Т сигнатуры S обозначается |WS(X)|T, а множество замкнутых термов типа Т|WS|T; множества всех термов и всех замкнутых термов обозначаются |WS(X)| и |WS| соответственно.

Для каждой сигнатуры типа данных Т с множеством сигнатур базисных конструкторов С(Т) множество генерирующих термов типа Т, GW(S)T, определяется следующим образом:

а) если (c: T)  С(Т), то c  GW(S)T;

б) если (с: T1,...,Tn  T)  С(Т) и е1,…,en – генери

 рующие термы типов T1,..., Tn соответственно, тогда

 с(е1,…, en)  GW(S)T.

Таким образом, генерирующими термами являются константы, обозначенные как базисные конструкторы (в общем случае не каждая константа – базисный конструктор) и затем термы, полученные применением конструкторов к генерирующим термам. Множество всех генерирующих термов типизированной сигнатуры S обозначается GW(S).

Имея в наличии множество генерирующих термов, мы можем при интерпретации термов отображать переменные в генерирующие термы, тем самым вовлекая в рассмотрение только значимые элементы алгебры. Функцию  интерпретации термов сигнатуры S в алгебре A на множестве переменных Х

 еvalA = |WS(X)|  |А|

определяем теперь следующим образом (для простоты определения считаем, что символ «@» в сигнатурах операций заменен на имя соответствующего типа данных):

1) для переменной xÎXT и функции подстановки v: XT ® GW(S)T:

 evalA(x) = evalA(v(x));

 2) для символа c: Т:   evalA(c) = cA,

3) для символа op: Т1,...,Т ® T , где T не Boolean, и термов

  t1,...,tn типов Т1,...,Т соответственно:

  a) evalA(op(t1,...,tn)) = opA(evalA(t1),...,evalA(tn)),

 если evalA определена для терма ti, i = 1,...,n и opA

 определена для (evalA(t1),...,evalA(tn));

 б) evalA не определена в противном случае;

4) для символа op: Т1,...,Т ® Boolean

  и термов t1,...,tn типов Т1,...,Т соответственно:

 а) evalA(op(t1,...,tn)) = trueA, если evalA определена

 для терма ti и opA(evalA(t1),...,evalA(tn)) = trueA;

 б) evalA(op(t1,..., tn)) = falseA в противном случае.

Заметим, что в отличие от раздела 2.1.2, где мы употребляли при интерпретации термов функцию означивания v: XS ® SA, т. е. отображали переменные в элементы алгебры, теперь мы употребляем функцию подстановки v: XT ® GW(S)T, т. е. отображаем переменные в генерирующие термы. Это дает возможность избежать отображения в «мусорные» элементы алгебры, т. е. элементы, не принадлежащие множествам значений типов данных.

Факт 1. Для каждого терма t Î GW(S)T, если t определен, тогда

tA Î Val(T)A. Доказательство очевидно.

Определение 21. Пусть S есть типизированная сигнатура, а Ef - множество аксиом, связанных с сигнатурой типа данных fT так, что каждое равенство в Ef содержит по крайней мере один символ операции из fT. Тогда пара <fT, Ef > - это спецификация типа данных, а тройка <TYPE, {<f, Ef>}, tspec>, где tspec - функция из TYPE в {<f, Ef >},  есть типизированная спецификация.

 Нотация. Конструируя конкретную типизированную спецификацию, мы фактически строим только функцию tspec как множество пар следующего вида: имя типа данных = spec спецификация типа данных. Множество сигнатур операций в сигнатуре типа данных заключается в квадратные скобки, а множество аксиом - в фигурные скобки. Конкретная пара <имя типа данных,  спецификация типа данных> впредь будет называться фрагментом спецификации. Пример такой спецификации приведен выше.

3.2. Иерархические спецификации

Определение 22.

1) спецификация одноосновной алгебры есть иерархическая спецификация;

2) иерархическая спецификация и фрагмент спецификации есть иерархическая спецификация.

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

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

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

 type Stack = spec

[empty: @;

push: Nat, @ ® @;

pop: @ ® @;

top: @ ® Nat;

is_empty: @ ® Boolean;

 generated by empty, push];

{forall x: Nat, s: @.

 dom top(s): is_empty(s);

 dom pop(s): is_empty(s);

 is_empty(empty) == true;

 is_empty(push(x,s)) == false;

 top(push(x,s)) == s;

 pop(push(x,s)) == s}.

Если мы теперь рассмотрим типичную реализацию стека посредством первоначально пустого массива чисел и указателя на верхний элемент p с начальным значением, равным нулю, то терм empty естественно отобразить в пару <{}, 0>. Однако после помещения в стек числа 1 и последующего прменения к нему операции pop стек в реализации будет иметь следующий вид: <{1},0>, считаясь при этом пустым стеком. Таким образом, элементы носителя <{},0> и <{1},0> (как и многие другие) являются эквивалентными, что, впрочем, следует из аксиом.

Заметим также, что при поведенческом подходе мы должны принять свободную семантику типа данных Boolean, согласно которой базисные конструкторы true и false обязательно отображаются в разные элементы носителя (поскольку тип Boolean находится в основании иерархии типов данных, нет никакой возможности указать посредством аксиом, что эти конструкторы производят различные значения).

 

Определение 23. Пусть TS будет типизированной спецификацией сигнатуры S. Множество специфицированных термов типа Т в спецификации TSSW(TS)T – определяется следующим образом:

1) если t  GW(S)T, тогда t  SW(TS)T;

2) если t1  SW(TS)T, в спецификации есть равенство Е на множестве переменных Х, и можно найти функцию подстановки v: X  GW(S), превращающую Е в равенство t2 == t1, тогда t2  SW(TS)T. Таким образом, каждый генерирующий терм является специфицированным и каждый терм, приравненный к генерирующему, является специфицированным.

Факт 2. Пусть TS будет типизированной спецификацией сигнатуры S и А - алгеброй этой спецификации. Тогда tA  Val(T)A, если t  SW(TS)T и t определен в А. Доказательство очевидно с использованием факта 1.

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

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

Если S - сигнатура, полученная при расширении сигнатуры S0 сигнатурой типа данных T, то замкнутый терм t  |WS0| называется примитивным термом. Замкнутый терм t  |WS|T0 называется термом примитивного типа, если T0 - имя примитивного типа. Соответственно терм t  |W(S)|T (т. е. замкнутый терм, составленный только из конструкторов сигнатуры типа данных T), называется термом определяемого типа.

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

Определение 24. Спецификация типа данных T непротиворечива, если она не устанавливает новых отношений для примитивных термов.

Согласно этому определению, спецификация типа Nat была бы противоречива, если бы содержала аксиому true == false.

Факт 4. Иерархическая спецификация, построенная согласно определениям 21 и 22, непротиворечива.

3.3. Независимые функции

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

 Замечание: впредь типизированная сигнатура будет обозначаться символом TS, а вместо термина “имя типа данных” будет употребляться более широкий термин “типовый терм”.

Определение 25. Пусть TS = <TYPE, F, tsig> будет иерархической типизированной сигнатурой, FUNC – множеством имен функций, а D – множеством профилей операций, построенных с использованием типовых термов из TYPE. Тогда тройка FS = <FUNC, D, fsig>, где fsig  (FUNC  D) – отношение, есть множество сигнатур функций, пара <f, d>  fsig – сигнатура функции, а  S = < TS, FS> – иерархическая сигнатура.

Требование: fsig не может содержать две такие пары <f, (T1,...,Tn  T11)> и <f, (T1,...,Tn  T12)>, в которых T11 и T12 – разные типовые термы. Это означает, что имена функций могут быть совмещены, но нужная функция всегда может быть однозначно идентифицирована по набору типов аргументов.

Алгебра A’ сигнатуры <TS, FS> строится путем расширения алгебры A сигнатуры TS следующим образом:

а) с каждым именем функции с с профилем Т может быть связан элемент из множества TA или не связано никакого элемента, при этом с с обязательно связывается либо trueA, либо falseA, если T – это Boolean; в этом случае функция называется константой;

б) с каждым именем функции f: T1,...,Tn  T связывается (частичная) функция fA’: T1A  ...  Tn A  T A .

Заметим, что булева константа всегда определена, а другие константы могут быть неопределенными.

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

Определение 26.  Пусть  SP  будет  иерархической  спецификацией,

FS = <FUNC, D, fsig> – основанном на ней множеством сигнатур функций, <f, d>  fsig – cигнатурой функции, а Ef – множеством аксиом, связанных с профилем функции f и построенных с использованием имен функций и операций из SP  и/или имен функций из FUNC. Тогда пара <f, <d, Ef>> – это спецификация функции, а тройка <FUNC, Fspec, fspec>, где Fspec = {<d, Ef> | <f, d>  fsig} и fspec = {<f, <d, Ef>>  | <f, d>  fsig}, – это множество спецификаций функций. В каждой алгебре функция, связанная с именем функции f, должна удовлетворять аксиомам из Ef.

Нотация: пара <f, <d, Ef>> изображается в спецификациях следующим образом: function f: d{Ef}, если f - функция, и const f: d = t, где d - типовый терм T, а t - замкнутый терм типа T, если f - константа.

Примеры:

const one: Nat = 1;

function natmax: Nat, Nat  Nat

{forall x, y: Nat.

natmax(x, y) == if x <= y then y else x.

Определение 27. Множество спецификаций функций  это фрагмент спецификации. Заметим, что в пределах этого множества функции могут специфицироваться рекурсивно.

3.4. Типовые классы

Рассматривая приведенные выше спецификации типов данных, мы можем заметить, что одна и та же сигнатура операции и некоторые аксиомы могут быть повторены в спецификациях нескольких типов данных. Например, все сигнатуры типов данных приведенного выше примера содержат сигнатуры операций "=" и "<>" с одними и теми же аксиомами. Мы можем использовать этот факт для классификации типов данных в соответствии с общими (или схожими) для них операциями. Типовые подтипы и типовые классы были предложены и внедрены в некоторые языки программирования (Atlant,  Haskel) для классификации типов данных в соответствии с наличием в них определенных операций.

Подобная классификация помогает формально определить языковые конструкции, требующие данных определенных типов. Например, параметр цикла FOR, имеющегося во многих языках программирования, должен принадлежать некоторому типу перечисления, конкретными представителями которого являются типы  Integer, Character и т. п. Следовательно, полезен класс перечислимых типов данных. Аналогично может быть полезен класс арифметических типов или класс типов с упорядоченными значениями. По этим причинам введение в спецификации типовых классов может придать им дополнительные возможности.

Определение 28. Пусть TS = <TYPE, F, tsig> – типизированная сигнатура, CLASS – множество имен, не пересекающееся с TYPE, и  C  – имя из CLASS. Тогда пара <C, <q, Eq>> (где q - множество сигнатур операций, а Eq - множество аксиом над q) спецификация типового класса С, а пара , q>сигнатура типового класса С. Тройка  <CLASS, Q, csig> (где Q  – множество сигнатур типовых классов, а csig – функция, отображающая CLASS в Q) – это множество сигнатур типовых классов, а тройка <CLASS, Spec, cspec> (где Spec = {<q, Eq> | q  Q} и cspec – функция из CLASS в Spec) – это множество спецификаций типовых классов.

Определение 29. Пусть TS, FS и CS – это соответственно типизированная сигнатура, множество сигнатур функций и  множество сигнатур типовых классов. Алгебра сигнатуры <TS, FS, CS> совпадает с алгеброй сигнатуры <TS, FS>, т. е. введение в спецификацию типового класса не изменяет алгебру.

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

Определение 30. Тип данных T принадлежит классу С, если

 cspec(C)  tspec(T),

т. е. если множество сигнатур операций класса С является подмножеством множества сигнатур операций типа данных T и множество аксиом класса С является подмножеством множества аксиом типа данных T.

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

 class C = spec C1,…,Cn csp’;

 type T = spec C1,…,Cn tsp’;

где C1,…,Cn - имена наследуемых типовых классов, csp’ - локальная спецификация типового класса и tsp’ - локальная спецификация типа данных. Если n не равно нулю, тогда

 cspec(C) = cspec(C1)  cspec(Cn)  csp’ и

 tspec(T) = cspec(C1)  cspec(Cn)  tsp’.

 

Определение 31. Спецификация типового класса - это фрагмент спецификации.

Примеры:

 class EQUAL = spec 

["=", "<>": @, @  Boolean]

{forall x, y, z: @.

x = x == true;

x = y == y = x;

x = z & z = y    x = y == true;

x <> y == (x = y)};

class ORDERED = spec EQUAL

 --– наследует спецификацию EQUAL

["<=", ">=", "<", ">": @, @  Boolean]

 {forall x, y, z: @.

x <= x == true;

x <= z & z <= y    x <= z == true;

x <= y & y <= x == x = y;

x < y == x <= y & (x = y);

x >= y == (x < y);

x > y == (x <= y)};

type Nat = spec ORDERED --– наследует ORDERED

[zero: @;

succ: @  @;

"+", "-": @, @  @;

generated by zero, succ]

{forall x, y: @.

 dom x-y: y <= x;

zero < succ(x) == true;

succ(x) < zero == false;

succ(x) < succ(y) == x < y;

succ(x) = zero == false;

succ(x) = succ(y) == x = y;

x + zero == x;

x + succ(y) == succ(x + y);

x - zero == x;

succ(x) - succ(y) == x – y};

 type SeqOfNat = spec EQUAL – наследует EQUAL

[empty: @;

append: Nat, @  @;

 head,length: @  Nat;

 tail: @  @;

 has: @, Nat  Boolean;

 is_empty: @  Boolean;

generated by empty, append]

{forall x, y: Nat, s, s1: @.

 dom head(s): is_empty(s);

 dom tail(s): is_empty(s);

is_empty(empty) == true;

is_empty(append(x,s) == false;

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

head(append(x,s)) == x;

has(empty,x) == false;

has(append(y,s),x) == x = y | has(s,x);

tail(append(x,s)) == s;

append(x,s) = empty == false;

append(x,s) = append(y,s1) == x = y & s = s1}.

3.5. Родовые типы данных

Мы предлагаем следующий способ конструирования имен из множества TYPE (которые отныне будут называться  типовыми термами).

Определение 32. Пусть S и R будут непересекающимися множествами имен (конкретных и родовых типов данных соответственно), не содержащими символов "(" и ")". Тогда если Т  S, то Т  TYPE и если T1,...,Tn – типовые термы из S и R  R, то R(T1,...,Tn)  TYPE.

 Определение 33. Пусть теперь tspec(R(T11,...,T1n))=spec1 и tspec(R(T21,...,T2n)) = spec2, где R(T11,...,T1n) и R(T21,...,T2n)  типовые термы, а spec1 и spec2  спецификации типов данных. Мы говорим, что тип данных R(T11,...,T1n) – это родственник типа данных R(T21,..., T2n), если замена каждого  T1i в spec1 на T2i, i = 1,...,n, превращает ее в  Spec2.  

Мы можем предложить специальный способ построения части функции  tspec для семейства родственных типов данных. Пусть q1,...,qn  имена (типовых параметров), индексированные именами классов  C1,...,Cn соответственно. Пара

 <R(q1:C1,...,qn:Cn),spec>,

где R  R, а spec  спецификация типа данных, использующая дополнительно имена  q1,...,qn в сигнатурах операций и символы операций из C1,...,Cn в аксиомах, есть такая часть функции tspec, что для каждого типового терма Ti класса Ci 

 tspec(R(T1,...,Tn)) = spec[T1/q1,...,Tn/qn],

где spec[T1/q1,...,Tn/qn] - спецификация типа данных, полученная заменой каждого qi в spec на Ti.

Пара <R(q1:C1,...,qn:Cn),spec> называется спецификацией родового типа данных R, а сам R часто называется родовым типом или конструктором типов. Замена типовых параметров типовыми термами в обеих частях спецификации родового типа данных называется конкретизацией родового типа данных. Заметим, что благодаря использованию функции tspec мы избегаем необходимости в особой семантике родового типа данных. Спецификация родового типа данных в нашем случае лишь одна из форм задания этой функции. Такой подход полностью соответствует практике тех языков программирования, в которых родовые типы данных рассматриваются просто как шаблоны (типичный пример С++).

Два типовых терма R(T11,...,T1n) и R(T21,...,T2n) считаются эквивалентными, если T1i и T2i, i = 1,...,n, одно и тоже имя типа данных или эквивалентные типовые термы.

Спецификация родового типа данных – это фрагмент спецификации. Пример:

type Seq(T: EQUAL) = spec EQUAL

[empty: @;

append: T, @  @;

head: @  T;

length: @  Nat;

tail: @  @;

has: @, T  Boolean;

is_empty: @  Boolean;

generated by empty, append]

{forall x, y: T, s, s1: @.

 dom head(s): is_empty(s);

 dom tail(s): is_empty(s);

is_empty(empty) == true;

is_empty(append(x,s) == false;

length(empty) == 0;

length(append(x,s)) == length(s) + 1;

head(append(x,s)) == s;

has(empty,x) == false;

has(append(y,s),x) == x = y | has(s,x);

tail(append(x,s)) == s;

append(x,s) = empty == false;

append(x,s) = append(y,s1) == x = y & s = s1}.

 Конкретизация Seq(Nat) приводит к спецификации типа данных SeqOfNat, приведенной в предыдущем разделе.

3.6. Встроенные конструкторы типов

Некоторые конструкторы типов являются встроенными, т. е. они подчиняются специальным правилам построения типовых термов. К ним относятся конструкторы типов перечислений, типов записей и типов объединений.

Типовый терм (p1,p2,...,pm,pn), где pi,i = 1,...,n, – некоторое имя, обозначает следующую спецификацию типа данных, называемого типом перечисления:

spec ORDERED --- наследует спецификацию ORDERED

[p1,p2, ...,pm,pn: @;

first,last: @;

succ,pred: @  @;

generated by p1,p2,...,pm,pn]

{forall x,y: @.

dom pred(x): x > p1;

dom succ(x): x < pn;

first == p1;

last == pn;

succ(p1) == p2; ... ; succ(pm) == pn;

pred(succ(x)) == x;

succ(x) = x == false;

x < succ(x) == true}.

Типовый терм Record(p1: T1; p2: T2; ... ; pn: Tn), где pi, i = 1,...,n, – некоторое имя (проектирующей функции), а Ti – типовый терм, обозначает следующую спецификацию типа данных, называемого типом записи:

spec

[create_rec: T1, T2,..., Tn  @;

p1: @  T1;

p2: @  T2;

. . .

pn: @  Tn]

{forall x1:T1, x2:T2,...,xn:Tn.

p1(create_rec(x1,x2,...,xn)) == x1;

p2(create_rec(x1,x2,...,xn)) == x2;

. . .

pn(create_rec(x1,x2,...,xn)) == xn}.

 Нотация: если r – запись, а p – проектирующая функция, мы обычно пишем r.p вместо p(r).

Типовый терм Union(p1:T1, p2:T2,..., pn:Tn), где pi – имя, а  Ti (i = 1,...,n) – типовый терм, обозначает следующую спецификацию родового типа данных, называемого типом объединения:

spec

[p1: T1  @;

p2: T2  @;

 . . .

pn: Tn  @;

get_p1: @  T1;

get_p2: @  T2;

 . . .

get_pn: @  Tn;

is_p1: @  Boolean;

is_p2: @  Boolean;

 . . .

is_pn: @  Boolean]

{forall x1:T1, x2:T2,...,xn:Tn, u:@.

dom get_p1(u): is_p1(u);

dom get_p2(u): is_p2(u);

. . .

dom get_pn(u): is_pn(u);

get_p1(p1(x1)) == x1;

get_p2(p2(x2)) == x2;

. . .

get_pn(pn(xn)) == xn;

is_p1(p1(x1)) == true;  is_p1(p2(x2)) == false;

 ... is_p1(pn(xn)) == false;

is_p2(p1(x1)) == false;  is_p2(p2(x2)) == true;

 ... is_p1(pn(xn)) == false;

    . . .

is_pn(p1(x1)) == false;  is_pn(p2(x2)) == false;

 ... is_pn(pn(xn)) == true}.

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

Если T – типовый терм, x – переменная типа T, а b – булев терм, не содержащий других переменных, кроме х, тогда

 subtype x: T when b

является типовым термом, называемым определением подтипа, который обозначает следующую спецификацию:

spec

[into: T  @;

 out: @  T]

{forall x:T.

 dom into(x): b;

 out(into(x)) == x};

Примеры:

subtype x: Nat when x >= 0 & x <= 10;

subtype x: String when head(x) = "a".

3.7. Родовые функции

Определение 34. Родовой профиль операции - это пара

 <(q1:C1,...,qk:Ck), oTq>,

где q1:C1,...,qk:Ck – имена (типовых параметров), помеченные именами типовых классов, а oTq – профиль операции, построенный из типовых термов и/или имен q1,...,qk.

Определение 35. Сигнатура родовой функции – это пара op: goT, где op – символ операции, а goT – родовой профиль операции.

Нотация: мы заключаем типовые параметры родовой функции в скобки gen ... op.

Пример: if: gen T: TYPE op Boolean, T, T  T.

Определение 36. Если opq:<(q1:C1,...,qk:Ck),oTq>  сигнатура родовой функции, а  T1,....Tk  типовые термы, такие, что каждый Ti, i = 1,...,k, принадлежит классу Ci, тогда opq(T1,...,Tk):oT – это конкретизированная сигнатура функции, где oT  профиль операции, полученный из oTq заменой каждого qi на Ti; opq(T1,...,Tk) называется конкретизированным именем функции.

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

if(Nat)(p,x,y).

В соответствии с расширением множества сигнатур независимых функций сигнатурами родовых функций любая алгебра A данной сигнатуры расширяется множеством функций mapAq по одной на каждую сигнатуру родовой функции opq:<(q1:C1,...,qk:Ck), oTq>; каждая mapAq сопоставляет некоторую функцию каждому конкретизированному имени функции opq(T1,...,Tk).

Определение функции интерпретации evalA расширяется теперь следующим образом: если opq(T11,...,T1k): T1,...,Tn ® T  конкретизированное имя функции и   t1,...,tn   термы типов T1,..., Tn соответственно, тогда:

evalA(opq(T11,...,T1k)(t1,...,tn)) =

mapAq(opq(T11,...,T1k)(evalA(t1),...,evalA(tn)).

 Нотация: Вместо opq(T11,...,T1k)(t1,...,tn)) мы пишем opq(t1,...,tn)), если это это не вызывает недоразумений.

Спецификация родовой функции – это сигнатура родовой функции и множество аксиом. Спецификация родовой функции является фрагментом спецификации.


4. Императивные спецификации динамических систем

4.1. Понятие состояния

Пусть S0 будет типизированной сигнатурой, как описано выше. Образуем ее приращение Ddin = (Tdin,Fdin), где Tdin – множество имен основ, а Fdin – множество сигнатур функций, в профилях которых используются имена из TYPETdin. Алгебра A сигнатуры S = S0ÈDdin образуется путем расширения S0-алгебры A0 следующим образом: множество элементов TA сопоставляется каждому имени T из Tdin и частичная функция fA: T1A ...´ TnA  TA сопоставляется каждой сигнатуре функции f: T1,...,Tn ® T из Fdin. Любая S0-алгебра A0 называется ниже статической, а S-алгебра Aдинамической. Соответственно любое множество и любая функция из A0 называются статическими, а любое множество и любая функция из приращения алгебры A0динамическими. Заметим, что константа введенная в Fdin, также может быть частичной, т.е. она может быть не определена в некоторой алгебре данной сигнатуры.

Нотация: динамические множества и функции вводятся в Ddin посредством служебного слова dynamic.

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

System  ID_TABLE

use Nat, Name, Defdata

-- используемые типы данных

dynamic 

function id_table: Name,Nat ® Defdata;

 const cur_level: Nat;

Во втором примере строится набор кругов на экране таким образом, что для каждый круг характеризуется своими координатами, радиусом и цветом (красный или зеленый). Количество кругов может быть разным в разных состояниях системы.

System  CIRCLES

use Real, Colour

--- используемые типы данных, где COLOUR

--- тип перечисления, имеющий только два

--- значения "green" и "red"

dynamic sort Circle;

function X, Y: Circle ® Real;

function radius: Circle ® Real;

function col: Circle ® Colour;

Определение 37. S-состояние – это S-алгебра, где S = S0 È Ddin.

Ограничение S-состояния A на S0 – это статическая алгебра A|_S0, называемая базой состояния A. Несколько состояний могут иметь одну и ту же базу. Мы обозначаем множество S-состояний с одной и той же базой B как statesB(S) и понимаем под SB-состо-

янием любое S-состояние с базой B. Таким образом, множество значений любого типа данных T TYPE в SB-состоянии A то же самое, что и в алгебре B, т.е. TA = TB для любого T Î TYPE.

4.2. Обновления

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

Определение 38. Обновление функции в SB-состоянии A  это тройка (f,a,a), где f имя динамической функции (константы) с профилем T1,…,Tn ® T, a = a1,...,an>, ai Î TiA, (a пусто, когда n равно нулю), а a  это либо элемент из множества TA, либо символ . Обновление функции a = (f,a,a) служит для преобразования SB-состояния A в SB-состояние Aa следующим образом:

gAa = gA для любого g, отличного от f;

fAa(a) = a, если a не символ ^,

fAa(a) не определено в противном случае;

fAa(a') = fA(a') для любого кортежа a'= <a'1,…, a'n >,

 отличного от a;

TAa = TA для любого T Î Tdin.

Мы говорим, что состояние A мутирует в Aa путем совершения в нем обновления a. Этим обновлением функция либо переопределяется в заданной точке, либо определяется в ней заново, либо делается неопределенной в ней.

Определение 39. Обновление основы в SB-состоянии A – это тройка (, Т, id), где  – это либо знак "+", либо знак "-", T – имя динамической основы, id элемент, такой что id TA, когда  = "+", и id Î TA, когда = "-".

Обновление основы d = ("+", Т, id) служит для преобразования SB-состояния A в SB-состояние Ad следующим образом:

· TAd = TA È {id},

· T1Ad = T1A  для любого T1 Î Tdin, отличного от T, и

· fAd = fA для любого f Î Fdin.

Обновление основы d = ("-", Т, id) служит для преобразования SB-состояния A в SB-состояние Ad следующим образом:

· TAd = TA \ {id},

· T1Ad = T1A  для любого T1 Î Tdin, отличного от T, и

·  для любой динамической функции fA: T1A ´ ... ´ TnA ® Tn+1A,

 если TiA, i = 1, ... , n+1,– множество, связанное с именем

основы T, тогда для каждого кортежа <a1, ... , an | an+1> Î fA,

  в котором некоторое ai, i = 1, ... , n+1, равно id,

 fAd = fA \{<a1, ... , an | an+1>};

fAd = fA в противном случае.

В последних двух случаях состояние A мутирует в g путем совершения в нем обновления d. Когда d = ("+", Т, id), основа T расширяется путем добавления в нее элемента id, а когда d = ("-", Т, id), основа T сокращается путем удаления из нее элемента id, при этом каждая динамическая функция становится неопределенной в любой точке, в которой id либо используется, либо вырабатывается.

Определение 40. Множество обновлений G противоречиво, если оно содержит либо

·  два конфликтующих обновления функции следующего вида:

a1= (f, a, a) и a2= (f, a, a'), где a a' (два 

  конфликтующих обновления функции определяют функцию по-

  разному в одной и той же точке), либо

·  два конфликтующих обновления основы следующего вида:

  d1 = ("+", T, id) и d2 = ("-", T, id) (один и

  тот же элемент одновременно добавляется в основу и удаляется

  из нее), либо

·  конфликтующиe обновление функции и обновление основы сле-

   дующего вида: a =(f, < a1,…, an>, an+1) для функции с

   сигнатурой f: T1,..., Ti ® Ti+1 и d = ("-", T, id),

 где T – это одно из Ti, i = 1, ... , n+1, а id = ai 

 (удаляется элемент основы, в то время как обновление функции

   должно его использовать);

множество обновлений непротиворечиво в противном случае.

Модификатор состояния m, примененный в SB-состоянии A к непротиворечивому G преобразует A в SB-состояние AG путем одновременного совершения всех обновлений a Î G и всех обновлений D Î G. Если G противоречиво, новое состояние не определено. Если G пусто, AG то же самое, что и A. В дальнейшем мы обозначаем применение модификатора m к непротиворечивому G в состоянии A как AG. Множество всех непротиворечивых множеств обновлений в stateB(S) обозначается ниже как updateB(S).

Определение 41. Пусть G1 и G2 будут двумя непротиворечивыми множествами обновлений в cостоянии A, a1 =(f,<a1,…, an>,a), a2 = (f,<a1, … , an>,a'), d1 = ("+", T, id) и d2 = ("-", T, id), где a a'. Последовательное объединение множеств G1 и G2, обозначаемое G1;G2,определяется следующим образом: u ΠG1;G2 если  uÎG1 или  uÎG2 за исключением следующих случаев:

· если a1 Î G1 и a2 Î G2, тогда  a2 Î G1;G2 и a1  G1;G2;

· если d2 Î G2, тогда для любого a = (g,<a1,…, an>,an+1) Î G1

 (где g имеет профиль T1, ..., Tn ® Tn+1), если  T – это одно

 из Ti, i = 1,…, n+1, и ai = id, то  a  G1;G2 и, если D1 Î G1,

 то оба D1  G1;G2  и  D2  G1;G2.

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

Нетрудно доказать следующие утверждения.

Факт 5. Если G1ÈG2 не противоречиво, тогда для любого непротиворечивого G выполняется: G;G1ÈG;G2 = G;(G1ÈG2).

Факт 6. Для любого SB-состояния A и всех непротиворечивых множеств обновлений G1 и G2 выполняется:

A(G1;G2) = (AG1)G2.

Непосредственным следствием указанного выше является тот факт, что для любой последовательности множеств обновлений G1,…, Gn и любого SB-состояния A, состояние AG, где G = G1;…;Gn, может быть получено применением G к A.

4.3. Динамическая система

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

Результат, вырабатываемый операцией анализа текущего состояния

системы, естественно, зависит от состояния, и потому мы будем называть такую операцию зависимой функцией. Сигнатуры этих функций вводятся в третьей части сигнатуры системы, Ddep, с использованием имен типов данных и имен основ из S в их профилях. Например, следующие зависимые функции могут быть определены для системы ID_TABLE:

depend function

defined_current: Name ® Boolean;

name_defined: Name, Nat ® Boolean;

 find: Name, Nat® Defdata;

Предполагается, что результат функции defined_current зависит от того, находится ли ее аргумент в текущем блоке таблицы

идентификаторов, результат функции name_defined – от того,

находится ли ее аргумент в каком-либо блоке таблицы

идентификаторов вообще, а функция find выдает данные, связанные в таблице с ее аргументом.

Определение 42. S'B-состояние – это S'-алгебра с базой B,где S'= S È Ddep.

Таким образом, зависимые функции расширяют SB-состояние к  S'B-состоянию. Множество всех S'B-состояний с базой B обозначается stateB(S').

Определение 43. S'-терм – это терм, построенный с использованием имен статических операций и функций из S0, имен динамических функций из Ddin и имен зависимых функций из Ddep.

S'-термы интерпретируются в S'-состояниях. Их использование в дополнение к S-термам позволяет нам повышать уровень спецификаций.

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

proc

initialize; --- конструирование пустой таблицы

 --- идентификаторов

insert_entry: Name, Defdata;

 --- вставка элемента в таблицу

new_level; --- создание нового блока в таблице

delete_level; --- удаление текущего блока

Следующие процедуры могут быть объявлены для системы CIRCLES:

proc

start; --- создание одного круга с параметрами

  --- по умолчанию

move: Circle, Real, Real;

 --- изменение координат круга

moveAll: Real, Real;

 --- изменение координат всех кругов

resize: Circle, Real;

 --- изменение радиуса круга

changeCol: Circle; --- изменение цвета круга

copy: circle --- cоздание нового круга с

 --- параметрами некоторого

 --- существующего круга

delCreen; --- удаление всех зеленых кругов

Определение 44. Динамическая система DS(B)сигнатуры DS = (S', Dproc),  где S' = S È Ddep и S = S0 È Ddyn, состоит из

·   множества состояний |DS(B)| stateB(S) с базой B,

называемого носителем системы;

·  функции mapDS(B): |DS(B)| ® stateB(S'), сопоставляю- щей некоторое S'B-состояние каждому SB-состоянию таким об-

разом, что для каждого A Î |DS(B)|), mapDS(B)(A)|S = A

(т.е. состояние mapDS(B)(A) есть расширение состояния A

зависимыми функциями);

·  (частичной) функции pDS(B) для каждого имени процедуры

p: Т1,…, Тn, сопоставляющей некоторое множество обновле-

ний G Î updateB(S) каждой паре <A,< a1, …, an> > , где

 A Î |DS(B)| и ai Î TiA, i = 1, …, n.

Заметим, что процедура производит множество обновлений.

Мы пишем pDS(B)(A, a) для применения процедуры pDS(B) к <A,a>, где A Î |DS(B)| и a = <a1, ... , an>. Когда n=0, n-ка a отсутствует.

Процедура p является константной, если результат применения pDS(B)(A, a) не зависит от A. Такая процедура может использоваться для инициализации системы.

4.4. Термы перехода

Обновления состояния задаются посредством специальных термов перехода. Они подразделяются на правила перехода и вызовы процедур.  Интерпретация терма перехода R в динамической системе DS(B) в состоянии A производит множество обновлений G. Соответствующее состояние A1 может быть получено как A1 = AG. При этом если A1 |DS(B)|, то интерпретация не определена. Мы пишем tA’ для интерпретации S'-терма t в S'B-состоянии A', полученным расширением SB-состояния A зависимыми функциями, и [t]A(B) – для интерпретации терма перехода t в системе DS(B) в SB-состоянии A.

4.4.1. Вызов процедуры

Если p: Т1, ... , Тn – имя процедуры, а t1, ... , tnтермы типов (основ) Т1, ... , Тn соответственно, тогда p(t1, ... , tn) – это терм перехода, называемый вызовом процедуры.

Интерпретация. Пусть DS(B) – динамическая система сигнатуры DS =(S0,Ddyn,Ddep,Dproc), а p(t1,… , tn) – вызов процедуры. Пусть также A – состояние из |DS(B)|, а A' = mapDS(B)(A) – расширение состояния A зависимыми функциями. Тогда 

[p(t1, ... , tn))]A(B) = pDS(B)(A, <t1A’, ... , tnA’>),

если каждый tiA’, i = 1, … , n, определен и результат pDS(B) определен для <t1A’, ... , tnA’> в состоянии A; интерпретация [p(t1, ... , tn))]A(B) не определена в противном случае.

4.4.2. Базисные правила перехода

Определение 45. Пусть f: T1, ... , Tn ® T – сигнатура динамической функции, ti, i = 1, … , n, – замкнутый терм типа Ti и t – замкнутый терм типа T. Тогда

 f(t1, ... , tn) := t и  f(t1, … , tn) := undef

правила перехода, называемые командами примитивного обновления.

Интерпретация. Если A' – расширенное состояние динамической системы DS(B) и ti, i = 1, … , n, определены в A', тогда

 [f(t1, ... , tn) := t]A(B) = {a1},

 [f(t1, ... , tn) := undef]A(B) = {a2}, где

a1 = (f,<t1A’, … , tnA’>,tA’) и a2 = (f,<t1A’, … , tnA’>,^).

Если хотя бы один из ti, i = 1, … , n, не определен в A', тогда обе интерпретации [f(t1, ... , tn) := t]A(B)  и

[g(t1, . . . , tn) := undef]A(B) не определены.

Примеры. Пусть c – динамическая константа типа Nat, а f – динамическая функция из Nat в Nat. Правило перехода

f(c) := f(c) + 1

преобразует алгебру A в алгебру A1 так, что:

fA1(cA) = fA(cA) + 1.

Правило перехода

c := undef

сделает c неопределенной в новом состоянии.

Команда сокращения основы. Если t – терм динамической основы Т, тогда drop t – это терм перехода, называемый командой сокращения основы.

Интерпретация. [drop t]A(B) = {("-", Т, tA’)}.

Правило перехода skip не вызывает смены состояния, т.е. [skip]A(B) = .

4.4.3. Конструкторы правил

Более сложные правила перехода строятся рекурсивно из базисных правил перехода и вызовов процедур посредством нескольких конструкторов правил.

Конструктор последовательности. Если R1, R2, ... , Rnтермы перехода, тогда seq R1, R2, … , Rn end есть терм перехода, называемый последовательностью термов перехода.

Интерпретация. Пусть A – SB-состояние, G1 = [R1]A(B), A1= AG1, G2 = [R2]A1(B), A2   = A1G2, ... ,  Gn = [Rn]An-1(B). Тогда

 [seq R1, R2, … , Rn end]A(B)= G,

где G = G1;G2;…;Gn, если каждое Gi непротиворечиво; в противном случае интерпретация [seq R1, R2, … , Rn end]A(B) не определена.

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

Конструктор множества. Если R1, ... , Rn – термы перехода, тогда set R1, ... , Rn end есть терм перехода, называемый множеством термов перехода.

Интерпретация. Пусть A – SB-состояние и G1 = [R1]A(B),…, Gn = [Rn]A(B). Тогда

 [set R1,… , Rn end]A(B)= G1 ÈÈ Gn,

если каждая [Ri]A(B) определена и G1 ÈÈ Gn непротиворечиво; в противном случае интерпретация не определена.

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

Пример: Пусть x, y, z – динамические константы типа Nat и f – функция из Nat в Nat. Тогда в результате исполнения множества правил перехода

 set f(x) := y, y := x, x := z end

получим:

fA1(xA) = yA       yA1 = xA      xA1 = zA

При исполнении множества правил перехода 

set f(x) := y, f(x) = y+1 end 

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

Конструктор условия. Если k – натуральное число, b0,…, bk – булевы термы, а R0, ... , Rk – термы перехода, тогда следующее выражение есть терм перехода, называемый правилом условного перехода:

if b0 then R0

elseif b1 then R1

 .

.

.

elseif bk then Rk

endif

Если терм bk – это булева константа true, тогда последнее elseif может быть заменено на "else Rk".

Интерпретация. Пусть A  – SB-состояние, A' = mapDS(B)(A), и R – правило условного перехода, тогда  [R]A(B) = [Ri]A(B) если bi истинно в A', а каждое bj при j < i ложно в A'. [R]A(B) = , если каждое bi ложно в A'.

Контролируемое обновление. Если b – булев терм, а R - терм перехода, тогда следующее выражение

 if b then R.

есть терм перехода, называемый командой контролируемого обновления: 

Интерпретация. Пусть R1 = if b then R. Тогда [R1]A(B) = [R]A(B) если b истинно в A'; [R1]A(B) =  в противном случае. Другими словами, следует исполнить команду, если условие выполняется, и не следует ничего делать в противном случае.

Конструкторы циклов. Команда контролируемого обновления вместе с конструктором последовательности дает нам возможность определить некоторые конструкторы циклов. Если R – терм перехода, а  b – булев терм, тогда

 while b do R   и  do R until b

термы перехода, называемые циклами.

Интерпретация.

 [while b do R]A(B) =

 [if b then seq R, while b do R end]A(B);

[do R until b]A(B) =

 [seq R, if b then do R until b]A(B).

Конструктор выбора варианта. Если R1, R2, ... , Rk – термы перехода, u – терм типа Union(p1:T1, p2:T2, ... , pn:Tn), и k <= n, тогда следующее выражение есть терм перехода, называемый правилом выбора варианта:

tagcase u of

p1: R1,

p2: R2,

 . . .

pk: Rk

endtag

Интерпретация. Пусть R – правило выбора варианта, построенное как указано выше, и истинно is_pi(u), где i <= k. Тогда [R]A(B) = [Ri[get_pi(u)/u]]A(B), где Ri[get_pi(u)/u] обозначает терм Ri, в котором каждое вхождение u заменено на get_pi(u) (т.е. значение типа объединения заменено на его вариантное значение). Если нет такого  i <= k, что истинно is_pi(u), тогда [R]A(B) = . Таким образом, правило выбора варианта позволяет рассматривать объединенное значение как вариантное значение требуемого типа (эта возможность не обеспечивается правилом условного перехода).

Конструктор импорта. Если x – переменная, T – имя динамической основы, а R – терм перехода, тогда

 import x: T in R

терм перехода, называемый правилом импорта.

Интерпретация. 

 [import x: T in R]A(B) = {d È [R]A(B),s},