Specifying Web Architecture with Larch

Dan Connolly
9th International World Wide Web Conference
Amsterdam
May 2000

Why Formal Systems?

They help me...

Why Larch?

Some Results

in Specifying Web Architecture with Larch:

The Semantic Web needs a model of State in the Web

A Simple Model of State in the Web

cf discussion with Paul Burchard, circa 1995:

GET : URI -> Literal

e.g.

GET("http://example.com") =
	"<html><head><title>Example</title> ...</html>"

Multiple Formats

GET("http://example.com/logo") = ...GIF data...

but... hmm... later, I find

GET("http://example.com/logo") = ...PNG data...

so I've got

GET("http://example.com/logo") != GET("http://example.com/logo")

so how about

GET : URI -> Set[Literal]

e.g.

GET("http://example.com/logo") =
	{...GIF data..., ...PNG data...}

The Web Varies over Time

one day I find:

GET("http://example.com", t1) =
	{"<html><head><title>Example</title> ...</html>", ...}

and the next:

GET("http://example.com", t2) =
	{"<html><head><title>Example Company</title> ...</html>", ... }

so how about

GET : URI, Time -> Set[Literal]

but:

The HTTP Trait

HTTP trait

...
   introduces
      http: absoluteURI, Message, Message, HTTPFormat, HTTPFormat -> Bool
        % for http(i, q, p, qf, pf) read:
        %  the message q, the request, and the message p, the reply,
        %  constitute a conforming HTTP transaction; the parsed data
        %  in the request and the reply are pf and pf respectively,
        %  and the request URI is i.

The 200 OK Axiom

        http(i, mq, mp, reqData, repData)
        /\ method(reqData) = GET
        /\ status(repData) = OK
        => represents(mp, i, content(repData));

The Origin Server Axiom, TCP/IP/DNS case

        % 
        % If you make a TCP connection to the origin server, whatever
        % it says is valid/authoritative, as long as its formatted correctly.
        i.scheme = HTTPURISchemeID
        /\ account(i) = nil   % leave http://user@host/ unspecified for now

        /\ says(ma, [URIOfDomain(host(i)), RRTypePropertyID(A), lit1])
        /\ hostAddr(lit1) = ip1
        /\ fresh(ma, mq, TTL(ma))

        /\ host(callee(conn(mq))) = ip1
        /\ port(callee(conn(mq))) = port(i)

        /\ conn(mq) = conn(mp)
        /\ idx(mq) = idx(mp)
        /\ httpParseReqs(callerBytes(conn(mq)), cmsgs)
        /\ httpParseReps(calleeBytes(conn(mp)), smsgs)

        /\ path(cmsgs[idx(mq)]) = i.path
        /\ host(cmsgs[idx(mq)]) = host(i) % HTTP 1.1-ism

        => http(i, mq, mp, cmsgs[idx(mq)], cmsgs[idx(mp)]);


The Conditional GET Axiom, If_Modified_Since case

Ari Luotonen and Kevin Altis
World-Wide Web Proxies
Proceedings of the 1st International WWW Conference, May 1994.

        
        http(i, mq, mp, reqData, repData)
        /\ represents(mp, i, cbody)
        /\ mp < mq2
        /\ http(i, mq2, mp2, reqData2, repData2)
        /\ method(reqData2) = GET
        /\ Last_Modified(repData) = If_Modified_Since(reqData2)
        /\ status(repData2) = NotModified
        => represents(mp2, i, cbody);

        % The Conditional GET Axiom, If_None_Match case
        http(i, mq, mp, reqData, repData)
        /\ represents(mp, i, cbody)
        /\ mp < mq2
        /\ http(i, mq2, mp2, reqData2, repData2)
        /\ method(reqData2) = GET
        /\ ETag(repData) \in If_None_Match(reqData2) % leave * unspecified for now
        /\ status(repData2) = NotModified
        /\ ETag(repData2) = ETag(repData)
        => represents(mp2, i, cbody); % implied metadata?