rsl.formal.specifications.conspect (811084), страница 17

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

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

Максимальный тип идентификатора или операции,представляющей некоторый тип, значение, переменную или канал,определяется соответствующим определением данного идентификатора илиоперации.8811.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Результат равен сумме двух вещественных значений.89• Целочисленное вычитание:− : Int × Int → IntРезультат равен разности первого и второго целочисленных значений.• Вещественное вычитание:− : Real × Real → RealРезультат равен разности первого и второго вещественных значений.• Целочисленное умножение:∗ : Int × Int → IntРезультат равен произведению двух целочисленных значений.• Вещественное умножение:∗ : Real × Real → RealРезультат равен произведению двух вещественных значений.• Целочисленное возведение в степень:~ Int↑ : Int × Int →Предусловие: второе целочисленное значение должно бытьнеотрицательным, и оно не должно быть равным 0, если первоецелочисленное значение равно 0.Результатом является первое целочисленное значение, возведенное встепень второго целочисленного значения.• Вещественное возведение в степень:~ Real↑ : Real × Real →Предусловие: если второе вещественное значение отрицательно илиравно нулю, то первое вещественное значение должно быть отличнымот нуля (0.0); если второе вещественное значение не является целымчислом, то первое должно быть неотрицательным.Результатом является первое вещественное значение, возведенное встепень второго вещественного значения.• Композиция функций:~ a T ) × (T →~ a′ T ) → (T →~ a″ T )° : (T2 →31213где a″ представляет собой объединение a и a′.Результат равен композиции двух функций, определяемой следующимобразом:f1 ° f2 ≡ λx : T1 • f1(f2(x))• Композиция отображений:° : (T2 ⎯⎯→m T3) × (T1 ⎯⎯m→ T2) → (T1 ⎯⎯m→ T3)90Результат равен композицииследующим образом:двухотображений,определяемойm1 ° m2 ≡ [x ↦ m1(m2(x)) | x : T1 • x ∈ dom m2 ∧ m2(x) ∈ dom m1]• Целочисленное деление:~ Int/ : Int × Int →Предусловие: второе целочисленное значение должно быть отличнымот нуля (0).Абсолютным значением (без учета знака) результата являетсяколичество раз, которое абсолютное значение второго целочисленногозначения содержится в абсолютном значении первого целочисленногозначения.

Знак результата равен произведению знаков аргументов.• Вещественное деление:~ Real/ : Real × Real →Предусловие: второе вещественное значение должно быть отличным отнуля (0.0).Результат получается путем деления первого вещественного значенияна второе вещественное значение.• Ограничение отображения на подмножестве (Map restriction to):/ : (T1 ⎯⎯→m T2) × T1-infset → (T1 ⎯⎯m→ T2)Результатом является отображение, полученное из исходного путемограничения его домена элементами указанного множества.• Остаток от целочисленного деления:~ Int\ : Int × Int →Предусловие: второе целочисленное значение должно быть отличнымот нуля (0).Абсолютным значением результата является остаток от деленияабсолютного значения второго целочисленного значения наабсолютное значение первого целочисленного значения.

Знакрезультата равен знаку первого аргумента. Справедливо следующеесоотношение:a = (a / b)∗b + (a \ b)где a и b — целочисленные значения, b отлично от нуля.• Разность множеств:\ : T-infset × T-infset → T-infsetРезультатом является множество, все элементы которого входят впервое множество и не входят во второе.91• Усечение отображения (Map restriction by):\ : (T1 ⎯⎯→m T2) × T1-infset → (T1 ⎯⎯m→ T2)Результатом является отображение, полученное из исходного путемисключения из его домена элементов указанного множества.• Целочисленное больше:> : 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 → Bool92Результат равен 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Результатом является множество, состоящее из всех элементов,которые входят хотя бы в одно из указанных множеств.93• Объединение отображений:∪ : (T1 ⎯⎯→m T2) × (T1 ⎯⎯m→ T2) → (T1 ⎯⎯m→ T2)Результатом является отображение, состоящее из всех пар первогоотображения и всех пар второго отображения.• Конкатенация списков:~ Tω^ : T ω × Tω →Предусловие: первый список должен быть конечным.Результатом является конкатенация указанных списков, т.е.результирующий список состоит из всех элементов первого и второгосписков, взятых в своем порядке, причем элементы первого спискастоят первыми.• Перекрытие отображений:† : (T1 ⎯⎯→m T2) × (T1 ⎯⎯m→ T2) → (T1 ⎯⎯m→ T2)Результатом является первое отображение, перекрытое вторымотображением.

Для всех элементов, принадлежащих одновременнодоменам обоих указанных отображений, второе отображениеперекрывает (замещает) первое.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, считается недоспецифицированным, если не указано ничегодругого.94Далее приведены значения конкретных префиксных операций (Т обозначаеттиповую переменную, представляющую произвольный тип).• Целочисленное абсолютное значение:abs : Int → IntРезультатом является абсолютное значение целочисленного аргумента.Для отрицательных целых возвращается значение с обратным знаком.Операцияявляетсятождественнойдлянеотрицательныхцелочисленных значений.• Вещественное абсолютное значение:abs : Real → RealРезультатом является абсолютное значение вещественного аргумента.Для отрицательных вещественных значений возвращается значение собратным знаком.

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

Список файлов учебной работы