Языки и методы формальной спецификации (1158803), страница 18
Текст из файла (страница 18)
(((x := c? ; c! value_expr) ▌ (c! value_expr ; x := c?))
▌ (x := value_expr))
úù (x := value_expr)
-
Interlocked-композиция (Interlocked composition):
value_expr1 ╫ value_expr2
Два указанных выражения value_expr выполняются, блокируя друг друга по отношению к внешним взаимодействиям (т.е. взаимодействиям с другими какими-то выражениями), до тех пор, пока одно из них не завершится, в то время как другое будет продолжать свое выполнение. Эти выражения могут предложить осуществить взаимодействие посредством каналов, в частности они могут предложить взаимодействие друг с другом (если одно из них производит ввод по какому-то каналу, а другое вывод по тому же каналу). Если выражения будут в состоянии взаимодействовать друг с другом, они выполнят это взаимодействие. Если выражения будут в состоянии взаимодействовать с другими параллельно выполняющимися выражениями, но только не друг с другом, они попадут в тупиковую ситуацию, где и будут пребывать, пока одно из них не сможет завершиться.
Единицей interlocked-композиции является skip, нулем — chaos. Interlocked-композиция обладает свойствами коммутативности и дистрибутивности по отношению к внутреннему выбору:
value_expr ╫ skip º value_expr
value_expr ╫ chaos º chaos
value_expr1 ╫ value_expr2 º value_expr2 ╫ value_expr1
value_expr1 ╫ ( value_expr2 úù value_expr3 ) º
( value_expr1 ╫ value_expr2 ) úù ( value_expr1 ╫ value_expr3)
Заметим, что в отличие от параллельной композиции ║ interlocked-композиция ╫ не является ассоциативной.
Если выражение value_expr сходится и не вызывает взаимодействия и если c1 c2, то справедливы следующие две эквивалентности:
x := c1? ╫ c2! value_expr º stop
x := 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_expr
skip ; value_expr º value_expr
value_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)
Литература для дополнительного чтения
[ADL] http://www.sun.com/960201/cover/language.html
[Eiffel] http://www.eiffel.com
[iContract] R.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 Specification Language. 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-SL Standard. 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 recommendation Z.100.
[Z] J.M.Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd edition, 1992.
Приложение 1. Приоритет операций
| Приоритет операций над значениями (по возрастанию) | ||
| Приоритет | Операции | Ассоциативность |
| 14 | □ | Правая |
| 13 | post | |
| 12 | ▌ ║ ╫ | Правая |
| 11 | ; | Правая |
| 10 | := | |
| 9 | | Правая |
| 8 | | Правая |
| 7 | | Правая |
| 6 | | |
| 5 | \ ^ † | Левая |
| 4 | | Левая |
| 3 | | |
| 2 | : | |
| 1 | ~ prefix_op | |
| Приоритет типовых операций (по возрастанию) | ||
| Приоритет | Operator(s) | Ассоциативность |
| 3 |
| Правая |
| 2 | | |
| 1 | -set -infset | |
Приложение 2. Таблица соответствия RSL символов и их ASCII представления
| ASCII | RSL | ASCII | RSL | ASCII | RSL |
| >< | | isin | | ~isin | |
| || | ║ | ++ | ╫ | -\ | |
| |=| | ▌ | |^| | | -list | |
| ** | | -inflist | | ~= | |
| /\ | | \/ | | +> | ↦ |
| >= | | exists | | all | |
| <= | | union | | !! | † |
| inter | | << | | always | □ |
| -m-> | | <<= | | => | |
| -~-> | | >> | | is | |
| -> | | >>= | | <-> | |
| # | | <. | | .> | |
| :- | • |
Используемые в ASCII представлении символов RSL слова all, exists, union, inter, isin, always являются зарезервированными и не могут использоваться в качестве идентификаторов.
Приложение 3. Ключевые слова RSL
| Ключевые слова RSL | |||
| Bool | class | inds | skip |
| Char | do | initialise | stop |
| Int | dom | int | swap |
| Nat | elems | len | then |
| Real | else | let | tl |
| Text | elsif | local | true |
| Unit | end | object | type |
| abs | extend | of | until |
| any | false | out | use |
| as | for | post | value |
| axiom | forall | pre | variable |
| card | hd | read | while |
| case | hide | real | with |
| channel | if | rng | write |
| chaos | in | scheme | |
Указанные в таблице ключевые слова не могут использоваться в качестве идентификаторов.
Содержание
ВВЕДЕНИЕ 3
1. Вводные замечания 7
1.1. Структура изложения материала 7
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
