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

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

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

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

11.2. Инфиксные операции (Infix Operators)

Синтаксис.

infix_op ::=

= ½  ½  ½  ½  ½  ½  ½  ½  ½  ½  ½  ½  ½  ½ \ ½ ^ ½  ½ † ½  ½ / ½

 ½  ½

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

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

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

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

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

• Равенство:

= : T  T  Bool

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

• Неравенство:

 : T  T  Bool

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

• Целочисленное сложение:

 : Int ´ Int ® Int

Результат равен сумме двух целочисленных значений.

• Вещественное сложение:

 : Real ´ Real ® Real

Результат равен сумме двух вещественных значений.

• Целочисленное вычитание:

 : Int ´ Int ® Int

Результат равен разности первого и второго целочисленных значений.

• Вещественное вычитание:

 : Real ´ Real ® Real

Результат равен разности первого и второго вещественных значений.

• Целочисленное умножение:

 : Int ´ Int ® Int

Результат равен произведению двух целочисленных значений.

• Вещественное умножение:

 : Real ´ Real ® Real

Результат равен произведению двух вещественных значений.

• Целочисленное возведение в степень:

 : Int ´ Int Int

Предусловие: второе целочисленное значение должно быть неотрицательным, и оно не должно быть равным 0, если первое целочисленное значение равно 0.

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

• Вещественное возведение в степень:

 : Real ´ Real Real

Предусловие: если второе вещественное значение отрицательно или равно нулю, то первое вещественное значение должно быть отличным от нуля (0.0); если второе вещественное значение не является целым числом, то первое должно быть неотрицательным.

Результатом является первое вещественное значение, возведенное в степень второго вещественного значения.

• Композиция функций:

 : (T₂ a T₃) ´ (T₁ a T₂) ® (T₁ a T₃)

где a представляет собой объединение a и a.

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

f₁  f₂  x : T₁ • f₁(f₂(x))

• Композиция отображений:

 : (T₂ T₃) ´ (T₁ T₂) ® (T₁ T₃)

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

m₁  m₂  [x ↦ m₁(m₂(x))  x : T₁ • x  dom m₂  m₂(x)  dom m₁]

• Целочисленное деление:

/ : Int ´ Int Int

Предусловие: второе целочисленное значение должно быть отличным от нуля (0).

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

• Вещественное деление:

/ : Real ´ Real Real

Предусловие: второе вещественное значение должно быть отличным от нуля (0.0).

Результат получается путем деления первого вещественного значения на второе вещественное значение.

• Ограничение отображения на подмножестве (Map restriction to):

/ : (T₁ T₂) ´ T₁-infset ® (T₁ T₂)

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

• Остаток от целочисленного деления:

\ : Int ´ Int Int

Предусловие: второе целочисленное значение должно быть отличным от нуля (0).

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

a = (a / b)b + (a \ b)

где a и b — целочисленные значения, b отлично от нуля.

• Разность множеств:

\ : T-infset  T-infset  T-infset

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

• Усечение отображения (Map restriction by):

\ : (T₁ T₂) ´ T₁-infset ® (T₁ T₂)

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

• Целочисленное больше:

 : Int ´ Int  Bool

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

• Вещественное больше:

 : Real ´ Real  Bool

Результат равен true тогда и только тогда, когда первое вещественное значение больше второго вещественного значения.

• Целочисленное меньше:

 : Int ´ Int ® Bool

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

• Вещественное меньше:

 : Real ´ Real  Bool

Результат равен true тогда и только тогда, когда первое вещественное значение меньше второго вещественного значения.

• Целочисленное больше или равно:

 : Int ´ Int ® Bool

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

• Вещественное больше или равно:

 : Real ´ Real ® Bool

Результат равен true тогда и только тогда, когда первое вещественное значение больше или равно второго вещественного значения.

• Целочисленное меньше или равно:

 : Int ´ Int ® Bool

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

• Вещественное меньше или равно:

 : Real ´ Real ® Bool

Результат равен true тогда и только тогда, когда первое вещественное значение меньше или равно второго вещественного значения.

• Включение в качестве подмножества (строгое):

 : T-infset ´ T-infset ® Bool

Результат равен true тогда и только тогда, когда второе множество является строгим подмножеством первого множества (т.е. совпадение множеств не допускается).

• Вхождение в качестве подмножества (строго):

 : T-infset ´ T-infset ® Bool

Результат равен true тогда и только тогда, когда первое множество является строгим подмножеством второго множества (т.е. совпадение множеств не допускается).

• Включение в качестве подмножества:

 : T-infset ´ T-infset ® Bool

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

• Вхождение в качестве подмножества:

 : T-infset ´ T-infset ® Bool

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

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

 : T ´ T-infset ® Bool

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

• Отрицание принадлежности множеству:

 : T ´ T-infset ® Bool

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

• Пересечение множеств:

 : T-infset ´ T-infset ® T-infset

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

• Объединение множеств:

 : T-infset ´ T-infset ® T-infset

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

• Объединение отображений:

 : (T₁ T₂) ´ (T₁ T₂) ® (T₁ T₂)

Результатом является отображение, состоящее из всех пар первого отображения и всех пар второго отображения.

• Конкатенация списков:

^ : T^ ´ T^ T^

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

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

• Перекрытие отображений:

† : (T₁ T₂) ´ (T₁ T₂) ® (T₁ T₂)

Результатом является первое отображение, перекрытое вторым отображением. Для всех элементов, принадлежащих одновременно доменам обоих указанных отображений, второе отображение перекрывает (замещает) первое.

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

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