Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:relational_semantics_of_procedures [2009/05/26 17:58] vkuncak |
sav08:relational_semantics_of_procedures [2009/05/26 20:35] vkuncak |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| How can we define semantics for program with recursive procedures? | How can we define semantics for program with recursive procedures? | ||
| + | |||
| + | We consider first the case of procedures without parameters; adding parameters is straightforward. | ||
| ===== One Recursive Procedure ===== | ===== One Recursive Procedure ===== | ||
| Line 133: | Line 135: | ||
| \end{array} | \end{array} | ||
| \] | \] | ||
| - | etc. | + | where $p.\_1$ and $p.\_2$ denote first, respectively, second, element of the pair $p$. |
| The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions. | The results extend to any number of call sites and any number of mutually recursive procedures, we just consider a function $G : {\cal R}^d \to {\cal R}^d$ where $d$ is the number of procedures; this mapping describes how, given one approximation of procedure semantics, compute a better approximation that is correct for longer executions. | ||