From Termination-Portal.org
|
|
| 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].
