Download Developing of a Web Cube prototype

4.4. WEB CUBE CONTRACTS
21
application HelloWorld {
cube home {
n : Int = 0;
writer method home() {
respond("hello world! <@ n @>");
n := n+1
}
}
}
Figure 4.4: Web Cube program
complicated code mixing as in the latter. In ASP and JSP code mixing is untyped, which
is of course not a good practice of programming. There are techniques to allow typed
code mixing, but this is beyond the scope of this project. Web Cube offers the possibility
to embed program expressions into the response string using the symbols <@ and @>.
Web Cube has also another special form of inlining. Let m is a method name in cube
with name c. In order to obtain the URI address of the method, we could write the following expression address.c.m. For example, a link to the home method can be made with:
respond("<a href=<@address.home.home@>>home</a>")
4.4
Web Cube Contracts
Since a resource can be a large and complicated system, it is represented as a black box
specified by a contract. Such a contract includes a Seuss box that abstractly (and thus incompletely) specifies the resource behaviour as a reactive system. An application relies on
the assumption that its resources behave according to their contracts. The responsibility
for correct contracts is more likely to be given to the component developers, than to the
application developer.
Essentially, a Web Cube application is just a Seuss system. Its properties can be expressed in terms of Seuss (temporal) operators. The original Seuss logic cannot however
deal with black box components (the resources). Therefore Web Cube uses an extension
[5]. The extension defines a notion of contract as a partial specification of a system, and
extend the operators (unless, ensures, and 7→) accordingly. Of course since we now allow
partial specifications, not all actual properties of a system can be verified.