From Termination-Portal.org
|
|
| (2 intermediate revisions by 2 users not shown) |
| Line 1: |
Line 1: |
| [[Category: Categories]] | | Syntax and semantics of the format are presented in [https://www.microsoft.com/en-us/research/publication/termcomp-proposal-pushdown-systems-as-a-model-for-programs-with-procedures/]. |
| | |
| === Semantics ===
| |
| | |
| 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>
| |
Latest revision as of 11:43, 18 March 2026
Syntax and semantics of the format are presented in [1].
