rsl.formal.specifications.conspect (811084), страница 18
Текст из файла (страница 18)
Операция являетсятождественнойдлянеотрицательных вещественных значений.• Преобразование вещественного в целое:int : Real → IntАбсолютным значением результата является наибольшее целое,которое меньше или равно абсолютного значения вещественногоаргумента. Знаком результата является знак аргумента.• Преобразование целого в вещественное:real : Int → RealРезультат идентичен аргументу, изменяется только его тип. Дляфункций преобразования типов справедливо соотношение:int real a = aгде а — произвольное целочисленное значение.• Кардинальность множества:~ Intcard : T-infset →Результат равен количеству элементов указанного множества. Эффектприменения операции card к бесконечному множеству представляетсобой расходящийся процесс.• Длина списка:~ Intlen : Tω →Результат равен длине указанного списка.
Эффект примененияоперации len к бесконечному списку представляет собой расходящийсяпроцесс.95• Индексы списка: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ω → T-infsetРезультатом является множество элементов указанного списка.• Головной элемент списка:~ Thd : Tω →Предусловие: список должен быть непустым.Результатом является первый элемент указанного списка.• Исключение головного элемента из списка:~ Tωtl : Tω →Предусловие: список должен быть непустым.Результатом является список, который получается из исходного спискапутем удаления его первого элемента.• Домен отображения:dom : (T1 ⎯⎯→m T2) → T1-infsetРезультатом является домен указанного отображения: значения, длякоторых определено это отображение.• Область значений отображения:rng : (T1 ⎯⎯→m T2) → T2-infsetРезультатом является область значений указанного отображения:значения, которые могут быть получены путем применения этогоотображения к значениям из его домена.12.
Связки12.1. Инфиксные связки (Infix Connectives)Синтаксис.infix_connective ::=⇒⏐∨⏐∧96Контекстно-независимые расширения. Инфиксные связки infix_connectiveпредназначены для составления новых булевских выражений из ужеимеющихся булевских выражений.При определении результирующего воздействия аксиоматическогоинфиксного выражения axiom_infix_expr, в котором встречается инфикснаясвязка infix_connective, используется общее правило, заключающееся в том,что второе выражение вычисляется только в том случае, когда значениепервого выражения не определяет однозначно значение всего выраженияaxiom_infix_expr. Это позволяет обойти в ряде случаев возможноерасхождение или тупиковую ситуацию во втором выражении.
Значениеаксиоматических инфиксных выражений axiom_infix_expr задается в терминахif-выражений, сокращениями которых и являются аксиоматическиеинфиксные выражения.• Логическое и:value_expr1 ∧ value_expr2является сокращенной формой записи выражения:if value_expr1 then value_expr2 else false end• Логическое или:value_expr1 ∨ value_expr2является сокращенной формой записи выражения:if value_expr1 then true else value_expr2 end• Импликация:value_expr1 ⇒ value_expr2является сокращенной формой записи выражения:if value_expr1 then value_expr2 else true end12.2.
Префиксные связки (Prefix Connectives)Синтаксис.prefix_connective ::=∼Контекстно-независимые расширения. Префиксная связка prefix_connectiveпредназначена для построения новых булевских выражений из ужеимеющихся булевских выражений.97• Логическое отрицание:Аксиоматическое префиксное выражение axiom_prefix_expr вида:∼ value_exprявляется сокращенной формой записи выражения:if value_expr then false else true end13.
Инфиксные комбинаторы (Infix Combinators)Синтаксис.infix_combinator ::=⏐⎥⎤ ⏐║ ⏐╫ ⏐;Семантика. Инфиксные комбинаторы infix_combinator применяются дляпостроения выражений, которые либо взаимодействуют, либо оказываютвоздействие на переменные. С каждым инфиксным комбинаторомinfix_combinator связан ряд простых правил доказательства, поясняющихсемантику соответствующего инфиксного комбинатора.• Внешний выбор (External choice):value_expr1value_expr2Внешнийвыборпроизводитсямеждурезультирующимивоздействиями двух указанных выражений value_expr.
На выбор можетповлиять возможный эффект от параллельного выполнения некотороготретьего выражения.Единичным элементом (единицей) внешнего выбора является stop,нулевым элементом (нулем) — chaos. Внешний выбор обладаетсвойствами идемпотентности, коммутативности, ассоциативности идистрибутивности по отношению к внутреннему выбору:value_exprstop ≡ value_exprvalue_exprchaos ≡ chaosvalue_exprvalue_expr ≡ value_exprvalue_expr1value_expr2 ≡ value_expr2value_expr1value_expr1( value_expr2value_expr3 ) ≡( value_expr1value_expr2 )value_expr398value_expr1( value_expr2 ⎥ ⎤ value_expr3 ) ≡( value_expr1value_expr2 ) ⎥ ⎤ ( value_expr1value_expr3)• Внутренний выбор (Internal choice):value_expr1 ⎥ ⎤ value_expr2Внутренний — недетерминированный — выбор производится междурезультирующими воздействиями двух указанных выраженийvalue_expr.
Возможный эффект от параллельного выполнениянекоторого третьего выражения не может оказать влияние навнутренний выбор.Нулевым элементом (нулем) внутреннего выбора является chaos.Внутреннийвыборобладаетсвойствамиидемпотентности,коммутативности и ассоциативности:value_expr ⎥ ⎤ chaos ≡ chaosvalue_expr ⎥ ⎤ value_expr ≡ value_exprvalue_expr1 ⎥ ⎤ value_expr2 ≡ value_expr2 ⎥ ⎤ value_expr1value_expr1 ⎥ ⎤ ( value_expr2 ⎥ ⎤ value_expr3 ) ≡( value_expr1 ⎥ ⎤ value_expr2 ) ⎥ ⎤ value_expr3• Параллельная композиция (Concurrent composition):value_expr1 ║ value_expr2Два указанных выражения value_expr выполняются параллельно друг сдругом до тех пор, пока одно из них не завершится, в то время какдругое будет продолжать свое выполнение.
Эти выражения могутпредложить произвести взаимодействие посредством каналов, вчастности они могут предложить взаимодействие друг с другом (еслиодно из них производит ввод по какому-то каналу, а другое вывод потому же каналу). Если выражения в состоянии взаимодействовать другс другом, они могут сделать внешний выбор, который предписываетим произвести это взаимодействие.
Альтернативной возможностьюявляется внешний выбор, который оставляет указанным выражениямсвободу произвести взаимодействие друг с другом или с другимипараллельно выполняющимися выражениями. Если выражения немогут взаимодействовать друг с другом, но в состоянии осуществитьвзаимодействиесдругимипараллельновыполняющимисявыражениями, им предоставляется возможность выполнить этовзаимодействие.Единичным элементом (единицей) параллельной композиции являетсяskip, нулевым элементом (нулем) — chaos. Параллельная композицияобладаетсвойствамикоммутативности,ассоциативностии99дистрибутивности по отношению к внутреннему выбору:value_expr ║ skip ≡ value_exprvalue_expr ║ chaos ≡ chaosvalue_expr1 ║ value_expr2 ≡ value_expr2 ║ value_expr1value_expr1 ║ ( value_expr2 ║ value_expr3 ) ≡( value_expr1 ║ value_expr2 ) ║ value_expr3value_expr1 ║ ( value_expr2 ⎥ ⎤ value_expr3 ) ≡( value_expr1 ║ value_expr2 ) ⎥ ⎤ ( value_expr1 ║ value_expr3)Если выражение value_expr сходится и не вызывает взаимодействия иесли c1 ≠ c2, то выполняются следующие две эквивалентности:x := c1? ║ c2! value_expr ≡(x := c1? ; c2! value_expr)x := c? ║ c! value_expr ≡(((x := c? ; c! value_expr)(x := value_expr))⎥ ⎤ (x := value_expr)(c2! value_expr ; x := c1?)(c! value_expr ; x := c?))• Interlocked-композиция (Interlocked composition):value_expr1 ╫ value_expr2Два указанных выражения value_expr выполняются, блокируя другдруга по отношению к внешним взаимодействиям (т.е.взаимодействиям с другими какими-то выражениями), до тех пор, покаодно из них не завершится, в то время как другое будет продолжатьсвое выполнение.
Эти выражения могут предложить осуществитьвзаимодействие посредством каналов, в частности они могутпредложить взаимодействие друг с другом (если одно из нихпроизводит ввод по какому-то каналу, а другое вывод по тому жеканалу). Если выражения будут в состоянии взаимодействовать друг сдругом, они выполнят это взаимодействие. Если выражения будут всостояниивзаимодействоватьсдругимипараллельновыполняющимися выражениями, но только не друг с другом, онипопадут в тупиковую ситуацию, где и будут пребывать, пока одно изних не сможет завершиться.Единицей interlocked-композиции является skip, нулем — chaos.Interlocked-композиция обладает свойствами коммутативности идистрибутивности по отношению к внутреннему выбору:value_expr ╫ skip ≡ value_exprvalue_expr ╫ chaos ≡ chaos100value_expr1 ╫ value_expr2 ≡ value_expr2 ╫ value_expr1value_expr1 ╫ ( value_expr2 ⎥ ⎤ value_expr3 ) ≡( value_expr1 ╫ value_expr2 ) ⎥ ⎤ ( value_expr1 ╫ value_expr3)Заметим, что в отличие от параллельной композиции ║ interlockedкомпозиция ╫ не является ассоциативной.Если выражение value_expr сходится и не вызывает взаимодействия иесли c1 ≠ c2, то справедливы следующие две эквивалентности:x := c1? ╫ c2! value_expr ≡ stopx := c? ╫ c! value_expr ≡ x := value_exprКомбинатор interlocked-композиции иллюстрирует различие междувнешним и внутренним выборами.
Если выражения value_expr1 иvalue_expr2 сходятся и не вызывают взаимодействия и если c1 ≠ c2, тоимеют место следующие две эквивалентности:(x := c1?c2! value_expr2) ╫ c1! value_expr1 ≡ x := value_expr1(x := c1?c2! value_expr2) ╫ c1! value_expr1 ≡ (x := value_expr1) ⎥ ⎤ stop• Последовательная композиция:value_expr1 ; value_expr2Второе выражение value_expr принуждается к выполнению послевыполнения первого выражения value_expr.
В качестве результатавыполнения последовательной композиции возвращается значениевторого выражения value_expr.Единицей последовательной композиции является skip, кроме того,даннаякомпозицияассоциативнаиобладаетсвойствомдистрибутивности по первому аргументу по отношению к внутреннемувыбору:value_expr ; skip ≡ value_exprskip ; value_expr ≡ value_exprvalue_expr1 ; (value_expr2 ; value_expr3) ≡(value_expr1 ; value_expr2) ; value_expr3(value_expr1 ⎥ ⎤ value_expr2) ; value_expr3 ≡(value_expr1 ; value_expr3) ⎥ ⎤ ( value_expr2 ; value_expr3)101Литература для дополнительного чтения[ADL][Eiffel][iContract]http://www.sun.com/960201/cover/language.htmlhttp://www.eiffel.comR.Kramer. iContract – The Java Design by Contract Tool.Fourth conference on OO technology and systems (COOTS),1998.[IFAD]http://www.ifad.dk[ISPRAS]http://www.ispras.ru/[Jones]C.B.
Jones. Systematic Software Development Using VDM.Prentice Hall International, 1986.[Larch]J.Guttag et al. The Larch Family of Specification Languages.IEEE Software, Vol. 2, No.5, September 1985, pp.24-36.[OMG]http://www.omg.org[RAISE-language] The RAISE Language Group. The RAISE SpecificationLanguage. Prentice Hall Europe, 1992.[RAISE-method] ftp://ftp.iist.unu.edu/pub/RAISE/method_book[RUP]http://www.rational.com[VDM_SL]N.Plat, P.G.Larsen. An Overview of the ISO/VDM-SLStandard.
SIGPLAN Notes, Vol. 27, No. 8, August 1992.[VDM++]http://www.csr.ncl.ac.uk/vdm/[MSC]Message Sequence Charts. ITU recommendation Z.120.[SDL]Specification and Design Language. ITU recommendationZ.100.[Z]J.M.Spivey. The Z Notation: A Reference Manual. PrenticeHall, 2nd edition, 1992.102Приложение 1. Приоритет операцийПриоритет операций над значениями (по возрастанию)Приоритет1413121110987654321Операции□ λ ∀ ∃ ∃!≡ post⎡⎢ ║ ╫;:=⇒∨∧=≠><≥≤⊂⊆⊃⊇∈∉+−\^∪†∗/°∩↑:~ prefix_opАссоциативностьПраваяПраваяПраваяПраваяПраваяПраваяЛеваяЛеваяПриоритет типовых операций (по возрастанию)Operator(s)ПриоритетАссоциативностьПравая~⎯⎯m→ → →×-set -infset ∗ ω321Приложение 2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
