Specifying Web Architecture with Larch

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

Why Formal Systems?

They help me...

check consistency within and across specs
check consistency of code (hopefully)
form concise, compelling arguments
think clearly

Why Larch?

(relatively) low cost of entry:
- easy to install
- familiar notation
- interactive tools, FAQ
practical integration with running code
practical integration with a proof assistant

Some Results

in Specifying Web Architecture with Larch:

harmonized character set terminology between SGML and MIME
reviewed XML Infoset, RDF, XML Schema specs
found a bug in Wadler's XPath semantics
working through Makoto's hedge automata
found a satisfying model of HTTP optimizations

The Semantic Web needs a model of State in the Web

on page p1, we find P
on page p2, we find P->Q
can we conclude Q?
- is the data from p2 still fresh?
- are p1 and p2 credible sources? on the subject of P and Q?

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:

who's time? client's? servers'? are they syncrhonized?
is this Set[Literal] ever observeable?
... and other issues

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?