Языки и методы формальной спецификации (1158803), страница 17

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

Текст из файла (страница 17)

11.3. Префиксные операции (Prefix Operators)

Синтаксис.

prefix_op ::=

abs ½ int ½ real ½ card ½ len ½ inds ½ elems ½ hd ½ tl ½ dom ½ rng

Контекстные условия. Контекстные условия для префиксных операций описаны в разделе 11.1.

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

Семантика. Семантика префиксной операции prefix_op определяется ее соответствующим определением. Предопределенные значения (семантика) применения префиксных операций prefix_op перечислены ниже.

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

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

• Целочисленное абсолютное значение:

abs : Int ® Int

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

• Вещественное абсолютное значение:

abs : Real ® Real

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

• Преобразование вещественного в целое:

int : Real ® Int

Абсолютным значением результата является наибольшее целое, которое меньше или равно абсолютного значения вещественного аргумента. Знаком результата является знак аргумента.

• Преобразование целого в вещественное:

real : Int ® Real

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

int real a = a

где а — произвольное целочисленное значение.

• Кардинальность множества:

card : T-infset Int

Результат равен количеству элементов указанного множества. Эффект применения операции card к бесконечному множеству представляет собой расходящийся процесс.

• Длина списка:

len : T^ Int

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

• Индексы списка:

inds : T^  Int-infset

Результатом является множество индексов указанного списка. Пусть f_list обозначает некоторый конечный список и i_list — бесконечный список, тогда:

inds f_list = { i  i : Int • i  1  i  len f_list }

inds i_list = { i ½ i : Int • i ³ 1 }

• Элементы списка:

elems : T^w  T-infset

Результатом является множество элементов указанного списка.

• Головной элемент списка:

hd : T^w T

Предусловие: список должен быть непустым.

Результатом является первый элемент указанного списка.

• Исключение головного элемента из списка:

tl : T^w T^

Предусловие: список должен быть непустым.

Результатом является список, который получается из исходного списка путем удаления его первого элемента.

• Домен отображения:

dom : (T₁ T₂)  T₁-infset

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

• Область значений отображения:

rng : (T₁ T₂)  T₂-infset

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

1. Связки

12.1. Инфиксные связки (Infix Connectives)

Синтаксис.

infix_connective ::=

    

Контекстно-независимые расширения. Инфиксные связки infix_connective предназначены для составления новых булевских выражений из уже имеющихся булевских выражений.

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

• Логическое и:

value_expr₁  value_expr₂

является сокращенной формой записи выражения:

if value_expr₁ then value_expr₂ else false end

• Логическое или:

value_expr₁  value_expr₂

является сокращенной формой записи выражения:

if value_expr₁ then true else value_expr₂ end

• Импликация:

value_expr₁  value_expr₂

является сокращенной формой записи выражения:

if value_expr₁ then value_expr₂ else true end

12.2. Префиксные связки (Prefix Connectives)

Синтаксис.

prefix_connective ::=



Контекстно-независимые расширения. Префиксная связка prefix_connective предназначена для построения новых булевских выражений из уже имеющихся булевских выражений.

• Логическое отрицание:

Аксиоматическое префиксное выражение axiom_prefix_expr вида:

 value_expr

является сокращенной формой записи выражения:

if value_expr then false else true end

1. Инфиксные комбинаторы (Infix Combinators)

Синтаксис.

infix_combinator ::=

▌ 

úù 

║ ½

╫ ½

;

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

• Внешний выбор (External choice):

value_expr₁ ▌ value_expr₂

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

Единичным элементом (единицей) внешнего выбора является stop, нулевым элементом (нулем) — chaos. Внешний выбор обладает свойствами идемпотентности, коммутативности, ассоциативности и дистрибутивности по отношению к внутреннему выбору:

value_expr ▌ stop  value_expr

value_expr ▌ chaos  chaos

value_expr ▌ value_expr º value_expr

value_expr₁ ▌ value_expr₂ º value_expr₂ ▌ value_expr₁

value_expr₁ ▌ ( value_expr₂ ▌ value_expr₃ ) º

( value_expr₁ ▌ value_expr₂ ) ▌ value_expr₃

value_expr₁ ▌ ( value_expr₂ úù value_expr₃ ) º

( value_expr₁ ▌ value_expr₂ ) úù ( value_expr₁ ▌ value_expr₃)

• Внутренний выбор (Internal choice):

value_expr₁ úù value_expr₂

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

Нулевым элементом (нулем) внутреннего выбора является chaos. Внутренний выбор обладает свойствами идемпотентности, коммутативности и ассоциативности:

value_expr úù chaos  chaos

value_expr úù value_expr º value_expr

value_expr₁ úù value_expr₂ º value_expr₂ úù value_expr₁

value_expr₁ úù ( value_expr₂ úù value_expr₃ ) º

( value_expr₁ úù value_expr₂ ) úù value_expr₃

• Параллельная композиция (Concurrent composition):

value_expr₁ ║ value_expr₂

Два указанных выражения value_expr выполняются параллельно друг с другом до тех пор, пока одно из них не завершится, в то время как другое будет продолжать свое выполнение. Эти выражения могут предложить произвести взаимодействие посредством каналов, в частности они могут предложить взаимодействие друг с другом (если одно из них производит ввод по какому-то каналу, а другое вывод по тому же каналу). Если выражения в состоянии взаимодействовать друг с другом, они могут сделать внешний выбор, который предписывает им произвести это взаимодействие. Альтернативной возможностью является внешний выбор, который оставляет указанным выражениям свободу произвести взаимодействие друг с другом или с другими параллельно выполняющимися выражениями. Если выражения не могут взаимодействовать друг с другом, но в состоянии осуществить взаимодействие с другими параллельно выполняющимися выражениями, им предоставляется возможность выполнить это взаимодействие.

Единичным элементом (единицей) параллельной композиции является skip, нулевым элементом (нулем) — chaos. Параллельная композиция обладает свойствами коммутативности, ассоциативности и

дистрибутивности по отношению к внутреннему выбору:

value_expr ║ skip º value_expr

value_expr ║ chaos º chaos

value_expr₁ ║ value_expr₂ º value_expr₂ ║ value_expr₁

value_expr₁ ║ ( value_expr₂ ║ value_expr₃ ) º

( value_expr₁ ║ value_expr₂ ) ║ value_expr₃

value_expr₁ ║ ( value_expr₂ úù value_expr₃ ) º

( value_expr₁ ║ value_expr₂ ) úù ( value_expr₁ ║ value_expr₃)

Если выражение value_expr сходится и не вызывает взаимодействия и если c₁  c₂, то выполняются следующие две эквивалентности:

x := c₁? ║ c₂! value_expr º

(x := c₁? ; c₂! value_expr) ▌ (c₂! value_expr ; x := c₁?)

x := c? ║ c! value_expr 

Характеристики

Список файлов книги