Chapter 9
External Objects and IO

We use the object-message system to allow interactions with external objects that represent external entities with state. This section explains Maude’s support for rewriting with external objects and an implementation of sockets, standard streams, files, and meta-interpreters as the first such external objects.

Configurations that want to communicate with external objects must contain at least one portal, where

 
sort Portal .
subsort Portal < Configuration .
op <> : -> Portal [ctor] .

is part of the predefined module CONFIGURATION in the file prelude.maude. From an implementation point of view, the main purpose of having a portal term in a configuration is to avoid the degenerate case of a configuration that consists just of an object waiting for a message from outside of the configuration. This would be problematic because the special behavior for object-message rewriting and exchanging messages with external objects is attached to the configuration constructor.

Rewriting with external objects is started by the external rewrite command erewrite (abbreviated erew) which is like frewrite (see Sections 5.4 and 8.2) except that it allows messages to be exchanged with external objects that do not reside in the configuration. Currently the command erewrite has some severe limitations, which might be fixed in future releases:

1.
Maude only checks for external rewrites when no “internal” rewrites are possible, so if, for example, there is a clock tick rewrite rule that is always enabled, external rewrites won’t take place.
2.
Rewrites that involve messages entering or leaving the configuration do not show up in tracing, profiling, or rewrite counts.
3.
It is possible to have bad interactions with break points and the debugger.
4.
There is a potential race condition with ^C.

Note that, even if there are no more rewrites possible, erewrite may not terminate; if there are requests made to external objects that have not yet been fulfilled because of waiting for external events from the operating system, the Maude interpreter will suspend until at least one of those events occurs, at which time rewriting will resume. While the interpreter is suspended, the command erewrite may be aborted with ^C. External objects created by an erewrite command do not survive to the next erewrite. If a message to an external object is ill-formed or inappropriate, or the external object is not ready for it, it just stays in the configuration for future acceptance or for debugging purposes.

Certain predefined external objects are available and some of them are object managers that can create more ephemeral external objects that represent entities such as files and sockets, and as we will see in Chapter 19, virtual copies of the Maude interpreter itself.

9.1 Standard streams

Each Unix process has three I/O channels, called standard streams: standard input (stdin), standard output (stdout), and standard error (stderr). In Maude, these are represented as three unique external objects, that are defined in a predefined module STD-STREAM in the file.maude file included in the Maude distribution. Because some of the messages that are useful for streams are also useful for file I/O, these messages are pulled out into a module COMMON-MESSAGES.

 
mod COMMON-MESSAGES is
protecting STRING .
including CONFIGURATION .

op gotLine : Oid Oid String -> Msg [ctor msg format (m o)] .
op write : Oid Oid String -> Msg [ctor msg format (b o)] .
op wrote : Oid Oid -> Msg [ctor msg format (m o)] .
endm

 
mod STD-STREAM is
including COMMON-MESSAGES .

op getLine : Oid Oid String -> Msg [ctor msg ...] .
op stdin : -> Oid [special (...)] .
op stdout : -> Oid [special (...)] .
op stderr : -> Oid [special (...)] .
endm

I/O on standard streams is always line-oriented and in text mode. stdout and stderr accept the write() message just like file handlers. They are automatically flushed so this is the only message they can accept. They always return a wrote() message.

The stdin object accepts a three-argument getLine() message:

 
getLine(stdin, ME, PROMPT)

ME is the identifier of the sender object, to which the answer will be sent. PROMPT is a string that will be shown to inform the user that some input is expected. Once the message is processed, when the user hits the return key, stdin replies with a message

 
gotLine(ME, stdin, TEXT)

where TEXT contains just a "\n" character in the case of an empty line, and is empty in the case of an error or end-of-file (^D).

9.1.1 The Hello Word! example

The module HELLO below shows a very simple program implementing an interaction with the user, which is asked to introduce his/her name to be properly greeted. The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and a message to stdin to read a line of text from the keyboard. When stdin has a line of text, it sends the text to the requesting object in a gotLine message.

 
mod HELLO is
including STD-STREAM .

op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .

var O : Oid .
var A : AttributeSet .
var S : String .
var C : Char .

eq run
= <>
< myObj : myClass | none >
getLine(stdin, myObj, "What is your name? ") .

rl < myObj : myClass | A >
gotLine(myObj, O, S)
=> < myObj : myClass | A >
if S =/= ""
then write(stdout, myObj, "Hello " + S)
else none
fi .
endm

 
Maude> erew run .
What is your name? Joe
Hello Joe
result Configuration: <> wrote(myObj, stdout) < myObj : myClass | none >

9.1.2 A ROT13 cypher example

As a second example of the use of standard streams, let us consider the specification in the module ROT13 below. The example prints out a banner and then reads lines from the keyboard, encrypts each line using the ROT13 cypher, and finally prints out the result.

 
mod ROT13 is
including STD-STREAM .
protecting INT .

op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .
op rot13 : String -> String .

vars O O2 : Oid .
var A : AttributeSet .
vars S T : String .
var C : Char .

eq rot13(C)
= if C >= "A" and C <= "Z"
then char(ascii("A") + ((13 + (ascii(C) - ascii("A"))) rem 26))
else if C >= "a" and C <= "z"
then char(ascii("a") + ((13 + (ascii(C) - ascii("a"))) rem 26))
else C
fi
fi .
eq rot13(S)
= rot13(substr(S, 0, 1)) + rot13(substr(S, 1, length(S)))
[owise] .

eq run
= <>
< myObj : myClass | none >
write(stdout, myObj, "\nROT13 Encryption\n----------------\n") .

rl < O : myClass | A >
wrote(O, O2)
=> < O : myClass | A >
getLine(stdin, O, "Enter plain text> ") .
rl < O : myClass | A >
gotLine(O, O2, T)
=> < O : myClass | A >
if T =/= ""
then write(stdout, O, "Cypher text: " + rot13(T) + "\n")
else none
fi .
endm

The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and an initial message to stdout to print out the banner. Each time stdout prints out some text, it sends a wrote reply to the requesting object; this is matched in the first rule which then sends a getLine message to stdin to read a line of text from the keyboard. When stdin has a line of text, it sends the text to the requesting object in a gotLine message; the second rule matches this message, calls the equationally defined rot13 function to encrypt the text, and sends a message to stdout to print the encrypted text. When the wrote reply comes back, the sequence repeats.

We can have the following interaction:

 
Maude> erewrite run .
erewrite in ROT13 : run .

ROT13 Encryption
----------------
Enter plain text> Maude
Cypher text: Znhqr
Enter plain text>
rewrites: 107 in 0ms cpu (3364ms real) (149025 rewrites/second)
result Configuration: <> < myObj : myClass | none >

9.1.3 A calculator example

The following program illustrates the use of functions metaReduce and metaParse (from module META-LEVEL, described later in Chapter 17) and functions tokenize and printTokens (from module LEXICAL in Section 7.11) to read Maude arithmetic expressions from the terminal and evaluate them.

 
mod CALCULATOR is
including STD-STREAM .
protecting LEXICAL .
protecting META-LEVEL .

op myClass : -> Cid .
op myObj : -> Oid .
op run : -> Configuration .

vars O O2 : Oid .
var A : AttributeSet .
vars S T : String .

op compute : String -> String .
eq compute(S) = compute2(metaParse([’CONVERSION], tokenize(S), anyType)) .

op compute2 : ResultPair? -> String .
eq compute2({T:Term, Q:Qid}) = compute3(metaReduce([’CONVERSION], T:Term)) .
eq compute2(noParse(N:Nat)) = printTokens(’\r) + "syntax error" + printTokens(’\o) .

op compute3 : ResultPair? -> String .
eq compute3({T:Term, Q:Qid}) = printTokens(metaPrettyPrint([’CONVERSION], T:Term)) .

eq run
= <>
< myObj : myClass | none >
write(stdout, myObj, "\nCalculator\n------------\n") .

rl < O : myClass | A >
wrote(O, O2)
=> < O : myClass | A >
getLine(stdin, O, "Expression> ") .
rl < O : myClass | A >
gotLine(O, O2, T)
=> < O : myClass | A >
if T == ""
then none
else write(stdout, O, "Answer: " + compute(T) + "\n")
fi .
endm

Then we can execute, for example:
 
Maude> erew run .
erewrite in CALCULATOR : run .

Calculator
------------
Expression> 3/6 + 12/32
Answer: 7/8
Expression>

9.2 File I/O

Unlike standard streams, of which there are exactly three, a Unix process may have many different files open at any one time. Thus, in order to create new file handle objects as needed, we have a unique external object called fileManager. To open a file, the fileManager is sent a message openFile. On success, an openedFile message is returned, with the name of an external object that is a handle on the open file as one of its arguments. Messages to read and write the file can be directed to the handle object. On failure, a fileError message is returned, with a text explanation of why the file could not be opened as one of its arguments. These messages are defined in the module FILE, which is distributed as part of the Maude system in the file.maude file.

 
mod FILE is
including COMMON-MESSAGES .
protecting INT .

sort Base .
ops start current end : -> Base [ctor] .

op file : Nat -> Oid [ctor] .

op openFile : Oid Oid String String -> Msg [ctor msg format (b o)] .
op openedFile : Oid Oid Oid -> Msg [ctor msg format (m o)] .

op getLine : Oid Oid -> Msg [ctor msg format (b o)] .

op getChars : Oid Oid Nat -> Msg [ctor msg format (b o)] .
op gotChars : Oid Oid String -> Msg [ctor msg format (m o)] .

op flush : Oid Oid -> Msg [ctor msg format (b o)] .
op flushed : Oid Oid -> Msg [ctor msg format (m o)] .

op setPosition : Oid Oid Int Base -> Msg [ctor msg format (b o)] .
op positionSet : Oid Oid -> Msg [ctor msg format (m o)] .
op getPosition : Oid Oid -> Msg [ctor msg format (b o)] .
op positionGot : Oid Oid Nat -> Msg [ctor msg format (m o)] .

op closeFile : Oid Oid -> Msg [ctor msg format (b o)] .
op closedFile : Oid Oid -> Msg [ctor msg format (m o)] .

op fileError : Oid Oid String -> Msg [ctor msg format (m o)] .

op fileManager : -> Oid [special (...)] .
endm

This API basically wraps the C stdio library. To open a file you send fileManager a message

 
openFile(fileManager, ME, PATH, MODE)

where ME is the name of the object the reply should be sent to, PATH is the path of the file you want to open, and MODE is one of: r, r+, w, w+, a, a+.

The reply is either

 
openedFile(ME, fileManager, FILE-HANDLE)

or
 
fileError(ME, fileManager, REASON)

where FILE-HANDLE is the name of the object used to access the file, and REASON is a textual explanation from the operating system of what went wrong.

If the file was opened for writing you can send

 
write(FILE-HANDLE, ME, DATA)

to write data to the file, and receive a reply

 
wrote(ME, FILE-HANDLE)

or
 
fileError(ME, FILE-HANDLE, REASON)

A file that is opened for writing can also be sent

 
flush(FILE-HANDLE, ME)

to flush any buffered data and receive a reply

 
flushed(ME, FILE-HANDLE)

or
 
fileError(ME, FILE-HANDLE, REASON)

A file that is opened for reading can be read on a line-by-line basis using the message:

 
getLine(FILE-HANDLE, ME)

where the reply is either

 
gotLine(ME, FILE-HANDLE, TEXT)

or
 
fileError(ME, FILE-HANDLE, REASON)

Here TEXT includes the newline character (if present, since end-of-file also ends the current line). TEXT is empty to indicate end-of-file with no more characters to read.

A file that is opened for reading can also be read on a character basis (which is more appropriate for binary files) using the message

 
getChars(FILE-HANDLE, ME, #CHARS-TO-GET)

where the reply is either

 
gotChars(ME, FILE-HANDLE, DATA)

or
 
fileError(ME, FILE-HANDLE, REASON)

Here if DATA is shorter than requested, it indicates the end-of-file was reached.

Reading and writing share a common position into the file where the next read or write takes place. This position in bytes from the start of the file can be obtained by sending the message

 
getPosition(FILE-HANDLE, ME)

where the reply is either

 
positionGot(ME, FILE-HANDLE, OFFSET)

or
 
fileError(ME, FILE-HANDLE, REASON)

The position may be changed with the message

 
setPosition(FILE-HANDLE, ME, OFFSET, BASE)

Here the OFFSET is relative to BASE, where BASE can take one of three values: start, the start of the file, current, the current position, or end, the end of the file. In the current and end cases, negative values of OFFSET are allowed. The reply is either

 
positionSet(ME, FILE-HANDLE)

or
 
fileError(ME, FILE-HANDLE, REASON)

Finally, an open file can be closed with the message

 
closeFile(FILE-HANDLE, ME)

Since it is always OK to close an open file, the response is always

 
closedFile(ME, FILE-HANDLE)

Note that messages that are not recognized or that are sent to nonexistent objects will be silently ignored and left in the configuration. Messages that are recognized but are not appropriate for the object they are sent to or which have bad arguments will similarly be ignored but will generate a “message declined” advisory.

9.2.1 A file copy example

The COPY-FILE module below illustrates the basic use of files. It specifies a simple algorithm to copy files. In this case, the run operator takes two arguments, namely the name of the file to be copied and the name of the new file. The equation for run produces a starting configuration, containing the portal, a user object to receive messages, and an initial message to open the original file. Once it is opened, the new file is created. Notice the "w" argument of the openFile message. Once both files are opened, a loop in which a line is read from the original file and written in the copy file is initiated. This loop ends when the end of the file is reached. Both files are then closed.

 
view Oid from TRIV to CONFIGURATION is
sort Elt to Oid .
endv

 
fmod MAYBE{X :: TRIV} is
sort Maybe{X} .
subsort X$Elt < Maybe{X} .
op maybe : -> Maybe{X} [ctor] .
endfm

 
mod COPY-FILE is
including FILE .
protecting (MAYBE * (op maybe to null)){Oid} .

op myClass : -> Cid .
op myObj : -> Oid .
ops in:_ out:_ : Maybe{Oid} -> Attribute .
ops inFile:_ outFile:_ : String -> Attribute .

op run : String String -> Configuration .
vars Text Original Copy : String .
vars FHIn FHOut : Oid .
var Attrs : AttributeSet .

eq run(Original, Copy)
= <>
< myObj : myClass | in: null, inFile: Original,
out: null, outFile: Copy >
openFile(fileManager, myObj, Original, "r") .

rl < myObj : myClass | in: null, outFile: Copy, Attrs >
openedFile(myObj, fileManager, FHIn)
=> < myObj : myClass | in: FHIn, outFile: Copy, Attrs >
openFile(fileManager, myObj, Copy, "w") .
rl < myObj : myClass | in: FHIn, out: null, Attrs >
openedFile(myObj, fileManager, FHOut)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
getLine(FHIn, myObj) .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
gotLine(myObj, FHIn, Text)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
if Text == ""
then closeFile(FHIn, myObj)
closeFile(FHOut, myObj)
else write(FHOut, myObj, Text)
fi .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
wrote(myObj, FHOut)
=> < myObj : myClass | in: FHIn, out: FHOut, Attrs >
getLine(FHIn, myObj) .
rl < myObj : myClass | in: FHIn, out: FHOut, Attrs >
closedFile(myObj, FHIn)
closedFile(myObj, FHOut)
=> none .
endm

You can then execute the program to copy a file "in.txt" with the following command:

 
Maude> erew run("in.txt", "out.txt") .

9.3 Sockets

The sockets external objects are accessed using the messages declared in the following SOCKET module, included in the file socket.maude which is part of the Maude distribution.

 
mod SOCKET is
protecting STRING .
including CONFIGURATION .

op socket : Nat -> Oid [ctor] .

op createClientTcpSocket : Oid Oid String Nat -> Msg
[ctor msg format (b o)] .
op createServerTcpSocket : Oid Oid Nat Nat -> Msg
[ctor msg format (b o)] .
op createdSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .

op acceptClient : Oid Oid -> Msg [ctor msg format (b o)] .
op acceptedClient : Oid Oid String Oid -> Msg
[ctor msg format (m o)] .

op send : Oid Oid String -> Msg [ctor msg format (b o)] .
op sent : Oid Oid -> Msg [ctor msg format (m o)] .

op receive : Oid Oid -> Msg [ctor msg format (b o)] .
op received : Oid Oid String -> Msg [ctor msg format (m o)] .

op closeSocket : Oid Oid -> Msg [ctor msg format (b o)] .
op closedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .

op socketError : Oid Oid String -> Msg [ctor msg format (r o)] .

op socketManager : -> Oid [special (...)] .
endm

Currently only IPv4 TCP sockets are supported; other protocol families and socket types may be added in the future. The external object named by the constant socketManager is a factory for socket objects.

To create a client socket, you send socketManager a message

 
createClientTcpSocket(socketManager, ME, ADDRESS, PORT)

where ME is the name of the object the reply should be sent to, ADDRESS is the name of the server you want to connect to (say “www.google.com”), and PORT is the port you want to connect to (say 80 for HTTP connections). You may also specify the name of the server as an IPv4 dotted address or as “localhost” for the same machine where the Maude system is running on.

The reply will be either

 
createdSocket(ME, socketManager, NEW-SOCKET-NAME)

or

 
socketError(ME, socketManager, REASON)

where NEW-SOCKET-NAME is the name of the newly created socket and REASON is the operating system’s terse explanation of what went wrong.

You can then send data to the server with a message

 
send(SOCKET-NAME, ME, DATA)

which elicits either

 
sent(ME, SOCKET-NAME)

or

 
closedSocket(ME, SOCKET-NAME, REASON)

Notice that all errors on a client socket are handled by closing the socket.

Similarly, you can receive data from the server with a message

 
receive(SOCKET-NAME, ME)

which elicits either

 
received(ME, SOCKET-NAME, DATA)

or

 
closedSocket(ME, SOCKET-NAME, REASON)

When you are done with the socket, you can close it with a message

 
closeSocket(SOCKET-NAME, ME)

with reply

 
closedSocket(ME, SOCKET-NAME, "")

Once a socket has been closed, its name may be reused, so sending messages to a closed socket can cause confusion and should be avoided.

Notice that TCP does not preserve message boundaries, so sending "one" and "two" might be received as "on" and "etwo". Delimiting message boundaries is the responsibility of the next higher-level protocol, such as HTTP. We will present an implementation of buffered sockets in Section 9.4 which solves this problem.

9.3.1 An HTTP/1.0 client example

The following modules implement an updated version of the five rule HTTP/1.0 client from the paper “Towards Maude 2.0” [27] that is now executable. The first module defines some auxiliary operations on strings.

 
fmod STRING-OPS is
protecting STRING .
var S : String .
op extractHostName : String -> String .
op extractPath : String -> String .
op extractHeader : String -> String .
op extractBody : String -> String .

eq extractHostName(S)
= if find(S, "/", 0) == notFound
then S
else substr(S, 0, find(S, "/", 0))
fi .

eq extractPath(S)
= if find(S, "/", 0) == notFound
then "/"
else substr(S, find(S, "/", 0), length(S))
fi .

eq extractHeader(S)
= substr(S, 0, find(S, "\r\n\r\n", 0) + 4) .
eq extractBody(S)
= substr(S, find(S, "\r\n\r\n", 0) + 4, length(S)) .
endfm

The second module requests one web page from an HTTP server.

 
mod HTTP/1.0-CLIENT is
protecting STRING-OPS .
including SOCKET .
sort State .
ops idle connecting sending receiving closing : -> State [ctor] .
op state:_ : State -> Attribute [ctor] .
op requester:_ : Oid -> Attribute [ctor] .
op url:_ : String -> Attribute [ctor] .
op stored:_ : String -> Attribute [ctor] .

op HttpClient : -> Cid .
op httpClient : -> Oid .
op dummy : -> Oid .

op getPage : Oid Oid String -> Msg [msg ctor] .
op gotPage : Oid Oid String String -> Msg [msg ctor] .

vars H R R TS : Oid .
vars U S ST : String .

First, we try to connect to the server using port 80, updating the state and the requester attribute with the new server.

 
rl [getPage] :
getPage(H, R, U)
< H : HttpClient |
state: idle, requester: R’, url: S, stored: "" >
=> < H : HttpClient |
state: connecting, requester: R, url: U, stored: "" >
createClientTcpSocket(socketManager, H,
extractHostName(U), 80) .

Once we are connected to the server (we have received a createdSocket message), we send a GET message (from the HTTP protocol) requesting the page. When the message is sent, we wait for a response.

 
rl [createdSocket] :
createdSocket(H, socketManager, TS)
< H : HttpClient |
state: connecting, requester: R, url: U, stored: "" >
=> < H : HttpClient |
state: sending, requester: R, url: U, stored: "" >
send(TS, H, "GET " + extractPath(U) + " HTTP/1.0\r\nHost: " +
extractHostName(U) + "\r\n\r\n") .

rl [sent] :
sent(H, TS)
< H : HttpClient |
state: sending, requester: R, url: U, stored: "" >
=> < H : HttpClient |
state: receiving, requester: R, url: U, stored: "" >
receive(TS, H) .

While the page is not complete, we receive data and append it to the string on the stored attribute. When the page is completed, the server closes the socket, and then we show the page information by means of the gotPage message.

 
rl [received] :
received(H, TS, S)
< H : HttpClient |
state: receiving, requester: R, url: U, stored: ST >
=> receive(TS, H)
< H : HttpClient | state: receiving,
requester: R, url: U, stored: (ST + S) > .

rl [closedSocket] :
closedSocket(H, TS, S)
< H : HttpClient |
state: receiving, requester: R, url: U, stored: ST >
=> gotPage(R, H, extractHeader(ST), extractBody(ST)) .

We use a special operator start to represent the initial configuration. It receives the server URL we want to connect to. Notice the occurrence of the portal <> in such initial configuration.

 
op start : String -> Configuration .
eq start(S)
= <>
getPage(httpClient, dummy, S)
< httpClient : HttpClient | state: idle, requester: dummy,
url: "", stored: "" > .
endm

Now we can get pages from servers, say “www.google.com”, by using the following Maude command (note the ellipsis in the output):

 
Maude> erew start("www.google.com") .
result Configuration: <> gotPage(dummy, httpClient, "HTTP/1.0 ... </html>")

It is also possible to have optional bounds on the erewrite command, and then use the continuation commands to get more results, like, for example,

 
Maude> erew [1, 2] start("www.google.com") .
result Configuration:
<>
< httpClient : HttpClient |
state: connecting,
requester: dummy,
url: "www.google.com",
stored: "" >
createClientTcpSocket(socketManager, httpClient, "www.google.com", 80)

 
Maude> cont 1 .
result Configuration:
<>
< httpClient : HttpClient |
state: connecting,
requester: dummy,
url: "www.google.com",
stored: "" >

To have communication between two Maude interpreter instances, one of them must take the server role and offer a service on a given port; generally ports below 1024 are protected. You cannot in general assume that a given port is available for use. To create a server socket, you send socketManager a message

 
createServerTcpSocket(socketManager, ME, PORT, BACKLOG)

where PORT is the port number and BACKLOG is the number of queue requests for connection that you will allow (5 seems to be a good choice). The response is either

 
createdSocket(ME, socketManager, SERVER-SOCKET-NAME)

or

 
socketError(ME, socketManager, REASON)

Here SERVER-SOCKET-NAME refers to a server socket. The only thing you can do with a server socket (other than close it) is to accept clients, by means of the following message:

 
acceptClient(SERVER-SOCKET-NAME, ME)

which elicits either

 
acceptedClient(ME, SERVER-SOCKET-NAME, ADDRESS, NEW-SOCKET-NAME)

or

 
socketError(ME, socketManager, REASON)

Here ADDRESS is the originating address of the client and NEW-SOCKET-NAME is the name of the socket you use to communicate with that client. This new socket behaves just like a client socket for sending and receiving. Note that an error in accepting a client does not close the server socket. You can always reuse the server socket to accept new clients until you explicitly close it.

The following modules illustrate a very naive two-way communication between two Maude interpreter instances. The issues of port availability and message boundaries are deliberately ignored for the sake of illustration (and thus if you are unlucky this example could fail).

The first module describes the behavior of the server.

 
mod FACTORIAL-SERVER is
inc SOCKET .
pr CONVERSION .
op _! : Nat -> NzNat .
eq 0 ! = 1 .
eq (s N) ! = (s N) * (N !) .

op Server : -> Cid .
op aServer : -> Oid .

vars O LISTENER CLIENT : Oid .
var A : AttributeSet .
var N : Nat .
vars IP DATA S : String .

Using the following rules, the server waits for clients. If one client is accepted, the server waits for messages from it. When the message arrives, the server converts the received data to a natural number, computes its factorial, converts it into a string, and finally sends this string to the client. Once the message is sent, the server closes the socket with the client.

 
rl [createdSocket] :
< O : Server | A > createdSocket(O, socketManager, LISTENER)
=> < O : Server | A > acceptClient(LISTENER, O) .

rl [acceptedClient] :
< O : Server | A > acceptedClient(O, LISTENER, IP, CLIENT)
=> < O : Server | A > receive(CLIENT, O)
acceptClient(LISTENER, O) .

rl [received] :
< O : Server | A > received(O, CLIENT, DATA)
=> < O : Server | A >
send(CLIENT, O, string(rat(DATA, 10)!, 10)) .

rl [sent] :
< O : Server | A > sent(O, CLIENT)
=> < O : Server | A > closeSocket(CLIENT, O) .

rl [closedSocket] :
< O : Server | A > closedSocket(O, CLIENT, S)
=> < O : Server | A > .
endm

The Maude command that initializes the server is as follows, where the configuration includes the portal <>.

 
Maude> erew <>
< aServer : Server | none >
createServerTcpSocket(socketManager, aServer, 8811, 5) .

The second module describes the behavior of the clients.

 
mod FACTORIAL-CLIENT is
inc SOCKET .
op Client : -> Cid .
op aClient : -> Oid .

vars O CLIENT : Oid .
var A : AttributeSet .

Using the following rules, the client connects to the server (clients must be created after the server), sends a message representing a number,1 and then waits for the response. When the response arrives, there are no blocking messages and rewriting ends.

 
rl [createdSocket] :
< O : Client | A > createdSocket(O, socketManager, CLIENT)
=> < O : Client | A > send(CLIENT, O, "6") .

rl [sent] :
< O : Client | A > sent(O, CLIENT)
=> < O : Client | A > receive(CLIENT, O) .
endm

The initial configuration for the client will be as follows, again with portal <>.

 
Maude> erew <>
< aClient : Client | none >
createClientTcpSocket(socketManager,
aClient, "localhost", 8811) .

Almost everything in the socket implementation is done in a nonblocking way; so, for example, if you try to open a connection to some webserver and that webserver takes 5 minutes to respond, other rewriting and transactions happen in the meanwhile as part of the same command erewrite. The one exception is DNS resolution, which is done as part of the createClientTcpSocket message handling and which cannot be nonblocking without special tricks.

9.4 Buffered sockets

As we said before, TCP does not preserve message boundaries; to guarantee it we may use a filter class BufferedSocket, defined in the module BUFFERED-SOCKET, which is described here. We interact with buffered sockets in the same way we interact with sockets, with the only difference that all messages in the module SOCKET have been capitalized to avoid confusion. Thus, to create a client with a buffered socket, you send socketManager a message

 
CreateClientTcpSocket(socketManager, ME, ADDRESS, PORT)

instead of a message

 
createClientTcpSocket(socketManager, ME, ADDRESS, PORT).

All the messages have exactly the same declarations, the only difference being their initial capitalization:

 
op CreateClientTcpSocket : Oid Oid String Nat -> Msg
[ctor msg format (b o)] .
op CreateServerTcpSocket : Oid Oid Nat Nat -> Msg
[ctor msg format (b o)] .
op CreatedSocket : Oid Oid Oid -> Msg [ctor msg format (m o)] .

op AcceptClient : Oid Oid -> Msg [ctor msg format (b o)] .
op AcceptedClient : Oid Oid String Oid -> Msg
[ctor msg format (m o)] .

op Send : Oid Oid String -> Msg [ctor msg format (b o)] .
op Sent : Oid Oid -> Msg [ctor msg format (m o)] .

op Receive : Oid Oid -> Msg [ctor msg format (b o)] .
op Received : Oid Oid String -> Msg [ctor msg format (m o)] .

op CloseSocket : Oid Oid -> Msg [ctor msg format (b o)] .
op ClosedSocket : Oid Oid String -> Msg [ctor msg format (m o)] .

op SocketError : Oid Oid String -> Msg [ctor msg format (r o)] .

Thus, apart from this small difference, we interact with buffered sockets in exactly the same way we do with sockets, the boundary control being completely transparent to the user.

When a buffered socket is created, in addition to the socket object through which the information will be sent, a BufferedSocket object is also created on each side of the socket (one in each one of the configurations between which the communication is established). All messages sent through a buffered socket are manipulated before they are sent through the socket underneath. When a message is sent through a buffered socket, a mark is placed at the end of it; the BufferedSocket object at the other side of the socket stores all messages received on a buffer, in such a way that when a message is requested the marks placed indicate which part of the information received must be given as the next message.

An object of class BufferedSocket has two attributes: read, of sort String, which stores the messages read, and bState, which indicates whether the filter is idle or active.

 
op BufferedSocket : -> Cid [ctor] .
op read :_ : String -> Attribute [ctor gather(&)] .
op bState :_ : BState -> Attribute [ctor gather(&)] .
sort BState .
ops idle active : -> BState [ctor] .

The identifiers of the BufferedSocket objects are marked with a b operator, i.e., the buffers associated with a socket SOCKET have identifier b(SOCKET). Note that there is a BufferedSocket object on each side of the socket, that is, there are two objects with the same identifier, but in different configurations.

 
op b : Oid -> Oid [ctor] .

A buffered socket object understands capitalized versions of the messages a socket object understands. For most of them, it just converts them into the corresponding uncapitalized message. There are messages AcceptClient, CloseSocket, CreateServerTcpSocket, and CreateClientTcpSocket with the same arities as the corresponding socket messages, with the following rules.

 
vars SOCKET NEW-SOCKET SOCKET-MANAGER O : Oid .
vars ADDRESS IP IP DATA S S REASON : String .
var Atts : AttributeSet .
vars PORT BACKLOG N : Nat .

rl [createServerTcpSocket] :
CreateServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG)
=> createServerTcpSocket(SOCKET-MANAGER, O, PORT, BACKLOG) .

rl [acceptClient] :
AcceptClient(SOCKET, O)
=> acceptClient(SOCKET, O) .

rl [closeSocket] :
CloseSocket(b(SOCKET), SOCKET-MANAGER)
=> closeSocket(SOCKET, SOCKET-MANAGER) .

rl [createClientTcpSocket] :
CreateClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT)
=> createClientTcpSocket(SOCKET-MANAGER, O, ADDRESS, PORT) .

Note that in these cases the buffered-socket versions of the messages are just translated into the corresponding socket messages.

A BufferedSocket object can also convert an uncapitalized message into the capitalized one. The rule socketError shows this:

 
rl [socketError] :
socketError(O, SOCKET-MANAGER, REASON)
=> SocketError(O, SOCKET-MANAGER, REASON) .

BufferedSocket objects are created and destroyed when the corresponding sockets are. Thus, we have rules

 
rl [acceptedclient] :
acceptedClient(O, SOCKET, IP’, NEW-SOCKET)
=> AcceptedClient(O, b(SOCKET), IP’, b(NEW-SOCKET))
< b(NEW-SOCKET) : BufferedSocket |
bState : idle, read : "" > .

rl [createdSocket] :
createdSocket(O, SOCKET-MANAGER, SOCKET)
=> < b(SOCKET) : BufferedSocket | bState : idle, read : "" >
CreatedSocket(O, SOCKET-MANAGER, b(SOCKET)) .

rl [closedSocket] :
< b(SOCKET) : BufferedSocket | Atts >
closedSocket(SOCKET, SOCKET-MANAGER, DATA)
=> ClosedSocket(b(SOCKET), SOCKET-MANAGER, DATA) .

Once a connection has been established, and a BufferedSocket object has been created on each side, messages can be sent and received. When a Send message is received, the buffered socket sends a send message with the same data plus a mark2 to indicate the end of the message.

 
rl [send] :
< b(SOCKET) : BufferedSocket | bState : active, Atts >
Send(b(SOCKET), O, DATA)
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
send(SOCKET, O, DATA + "#") .

rl [sent] :
< b(SOCKET) : BufferedSocket | bState : active, Atts >
sent(O, SOCKET)
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
Sent(O, b(SOCKET)) .

The key is then in the reception of messages. A BufferedSocket object is always listening to the socket. It sends a receive message at start up and puts all the received messages in its buffer. Notice that a buffered socket goes from idle to active in the buffer-start-up rule. A Receive message is then handled if there is a complete message in the buffer, that is, if there is a mark on it, and results in the reception of the first message in the buffer, which is removed from it.

 
rl [buffer-start-up] :
< b(SOCKET) : BufferedSocket | bState : idle, Atts >
=> < b(SOCKET) : BufferedSocket | bState : active, Atts >
receive(SOCKET, b(SOCKET)) .

rl [received] :
< b(SOCKET) : BufferedSocket |
bState : active, read : S, Atts >
received(b(SOCKET), O, DATA)
=> < b(SOCKET) : BufferedSocket |
bState : active, read : (S + DATA), Atts >
receive(SOCKET, b(SOCKET)) .

crl [Received] :
< b(SOCKET) : BufferedSocket |
bState : active, read : S, Atts >
Receive(b(SOCKET), O)
=> < b(SOCKET) : BufferedSocket |
bState : active, read : S’, Atts >
Received(O, b(SOCKET), DATA)
if N := find(S, "#", 0)
/\ DATA := substr(S, 0, N)
/\ S := substr(S, N + 1, length(S)) .

The BUFFERED-SOCKET module is used in the specification of Mobile Maude, a mobile agent language based on Maude, which is discussed in detail in [29, Chapter 16].