Download Extending Java for High-Level Web Service Construction
Transcript
Extending Java for High-Level Web Service Construction
·
37
{white}
color
contents
<html>...</html>
what
Welcome ...
<b>BRICS</b>
c1
c1
<em>Hello World!</em>
<b><[g ]></b>
g
U*
Implicitly in this illustration, the gap presence map maps everything to (∅, {CLOSED},
{CLOSED}), and the string edge map maps to the empty language by default. Because of the simple flow in the example program, the language of this summary
graph is precisely the set of XML documents that may occur at runtime. In general, the summary graphs are conservative since they they may denote languages
that are too large. This means that the subsequent analyses can be sound but not
complete.
5. PROVIDING STATIC GUARANTEES
The remaining analyses are independent of both the original JWIG program and
the flow graphs. All the relevant information is at this stage contained in the
inferred summary graphs. This is a modular approach where the “front-end” and
“back-end” analyses may be improved independently of each other. Also, summary
graphs provide a good context for giving intuitive error messages.
5.1 Plug Analysis
We first validate plug consistency of the program, meaning that gaps are always
present when subjected to the plug operation and that XML templates are never
plugged into attribute gaps. This information is extracted from the summary graph
of the template being plugged into.
In earlier work [Sandholm and Schwartzbach 2000] a similar check was performed
directly on the flow graphs. Our new approach has the same precision, even though
it relies exclusively on the summary graphs. Furthermore, we no longer require the
flow graph to agree on the gap information for all incoming branches in the join
points, as mentioned in Section 4.2.
For a specific plug operation x <[ g = y ] at a program point `, consider the summary graph summary ` (x) = (R, T, S, P ) given by the data-flow analysis described
in the previous section. Let (p, t, a) = P (g). We now check consistency of the plug
operation simply by inspecting that the following condition is satisfied:
t = {OPEN} ∨ a = {OPEN}
if y has type STRING, and
t = {OPEN} ∧ a = {CLOSED} if y has type XML.
This captures the requirement that string plug operations are allowed on all gaps
that are present, while template plug operations only are possible for template gaps.
If a violation is detected, a precise error message can be generated: for instance, if
y has type XML, t = {OPEN}, and a = {OPEN,CLOSED}, we report that, although