1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
\begin{figure}
Compatibility between values, outcomes and return types:
$$\begin{array}{rclr}
"Out_normal", "Tvoid" & \# & "Vundef"& \\
"Out_normal", "Tvoid" & \# & "Vundef"& \\
"Out_return", \, "Tvoid" & \# & "Vundef" & \\
"Out_return" \some v, \, \tau & \# & v & \mbox{when}\,\tau~\not="Tvoid"
\end{array}$$
\numberrules
Function calls:
\begin{pannel}
\irule
G, E |- {a_{fun}}^{\tau}, M \evalexpr v_{fun}, \tr_1, M_1 &
G, E |- a_{args}, M_1 \evalexpr v_{args}, \tr_2, M_2 \\
G[v_{fun}] = \some{f} &
"type_of_fundef" (f) = \tau \\
G |- f(v_{args}), M_2 \evalfunc v_{res}, \tr_3, M_3
--------------------------------------------------
G, E |- {({a_{fun}}^{\tau} (a_{args}))}^{\tau'}, M \evalexpr v_{res}, \cat {\cat {\tr_1} \tr_2} \tr_3, M_3
\end \label{rule:25}
\end{pannel}
Function invocations:
\begin{pannel}
\irule
"alloc" ({\it \emptyset_E}, M, "params" (f) + "vars" (f),E) = (M_1, b) \\
"bind_params" (E, M_1, "params" (f), v_{args}) = M_2 \\
G, E |- "body" (f), M_2 \evalstmt \out, \tr, M_3 \\
\out, \, "fn_return" (f) \, "#" \, v_{res}
--------------------------------------------------
G, E |- f(v_{args}), M \evalstmt v_{res}, \tr, "free" (M_3, b)
\end \label{rule:26}
\irule
v_{args}, v_{res} \cong^{\sigma} e_{args}, e_{res}
--------------------------------------------------
G, E |- <\id \, \sigma>(v_{args}), M \evalstmt v_{res}, [\id \,e_{args}\, e_{res}], M
\end \label{rule:27}
\end{pannel}
\caption{Dynamic semantics of function call}
\label{fig:dynsem3}
\end{figure}
|
