|
|
| Line 1: |
Line 1: |
| | [[Category: Categories]] | | [[Category: Categories]] |
| | | | |
| − | === Semantics ===
| + | Syntax and semantics of the format are presented in [http://research.microsoft.com/apps/pubs/?id=219529]. |
| − | | |
| − | We define a (global) transition relation <math>\mathit{next}</math> as follows:
| |
| − | <math>
| |
| − | \begin{array}[t]{@{}l@{}}
| |
| − | ((x \cdot \mathit{xs}), (y \cdot \mathit{ys})) \in \mathit{next} \text{ iff } \\[\jot]
| |
| − | \qquad\qquad
| |
| − | \exists p \in \mathit{Proc} :
| |
| − | \begin{array}[t]{@{}r@{}l@{}}
| |
| − | &\mathit{step}_p(x, y) \land \mathit{xs} = \mathit{ys} \\[\jot]
| |
| − | \mathrel{\lor}& \exists q \in \mathit{Proc}:
| |
| − | \begin{array}[t]{@{}r@{}l@{}}
| |
| − | &\mathit{call}^p_q(x, y) \land (x \cdot \mathit{xs}) = \mathit{ys} \\[\jot]
| |
| − | \mathrel{\lor} &\mathit{return}^p_q(x, z, y) \land \mathit{xs} = (z \cdot \mathit{ys})
| |
| − | \end{array}
| |
| − | \end{array}
| |
| − | \end{array}
| |
| − | </math>
| |
Revision as of 09:10, 16 June 2014
Syntax and semantics of the format are presented in [1].
