You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
228 lines
5.5 KiB
228 lines
5.5 KiB
<HTML>
|
|
<HEAD>
|
|
<!-- Created with AOLpress/2.0 -->
|
|
<TITLE>Specifying Web Architecture with Larch (WWW9 Presentation)</TITLE>
|
|
</HEAD>
|
|
<BODY>
|
|
<H1>
|
|
Specifying Web Architecture with Larch
|
|
</H1>
|
|
<ADDRESS>
|
|
<A HREF="http://www.w3.org/People/Connolly/">Dan Connolly</A><BR>
|
|
<A HREF="http://www9.org/">9th International World Wide Web
|
|
Conference</A><BR>
|
|
Amsterdam<BR>
|
|
May 2000
|
|
</ADDRESS>
|
|
<H1>
|
|
Why Formal Systems?
|
|
</H1>
|
|
<P>
|
|
They help me...
|
|
<UL>
|
|
<LI>
|
|
check consistency within and across specs
|
|
<LI>
|
|
check consistency of code (hopefully)
|
|
<LI>
|
|
form concise, compelling arguments
|
|
<LI>
|
|
think clearly
|
|
</UL>
|
|
<H1>
|
|
Why Larch?
|
|
</H1>
|
|
<UL>
|
|
<LI>
|
|
(relatively) low cost of entry:
|
|
<UL>
|
|
<LI>
|
|
easy to install
|
|
<LI>
|
|
familiar notation
|
|
<LI>
|
|
interactive tools, FAQ
|
|
</UL>
|
|
<LI>
|
|
practical integration with running code
|
|
<LI>
|
|
practical integration with a proof assistant
|
|
</UL>
|
|
<H1>
|
|
Some Results
|
|
</H1>
|
|
<P>
|
|
in <A HREF="http://www.w3.org/XML/9711theory/Overview.html">Specifying Web
|
|
Architecture with Larch</A>:
|
|
<UL>
|
|
<LI>
|
|
harmonized character set terminology between SGML and MIME
|
|
<LI>
|
|
reviewed XML Infoset, RDF, XML Schema specs
|
|
<LI>
|
|
found a bug in Wadler's XPath semantics
|
|
<LI>
|
|
working through Makoto's hedge automata
|
|
<LI>
|
|
found a satisfying model of HTTP optimizations
|
|
</UL>
|
|
<H1>
|
|
The Semantic Web needs a model of State in the Web
|
|
</H1>
|
|
<UL>
|
|
<LI>
|
|
on page p1, we find P
|
|
<LI>
|
|
on page p2, we find P->Q
|
|
<LI>
|
|
can we conclude Q?
|
|
<UL>
|
|
<LI>
|
|
is the data from p2 still fresh?
|
|
<LI>
|
|
are p1 and p2 credible sources? on the subject of P and Q?
|
|
</UL>
|
|
</UL>
|
|
<H1>
|
|
A Simple Model of State in the Web
|
|
</H1>
|
|
<P>
|
|
cf discussion with Paul Burchard, circa 1995:
|
|
<PRE>GET : URI -> Literal
|
|
</PRE>
|
|
<P>
|
|
e.g.
|
|
<PRE>GET("http://example.com") =
|
|
"<html><head><title>Example</title> ...</html>"
|
|
</PRE>
|
|
<H1>
|
|
Multiple Formats
|
|
</H1>
|
|
<PRE>GET("http://example.com/logo") = ...GIF data...
|
|
</PRE>
|
|
<P>
|
|
but... hmm... later, I find
|
|
<PRE>GET("http://example.com/logo") = ...PNG data...
|
|
</PRE>
|
|
<P>
|
|
so I've got
|
|
<PRE>GET("http://example.com/logo") != GET("http://example.com/logo")
|
|
</PRE>
|
|
<P>
|
|
so how about
|
|
<PRE>GET : URI -> Set[Literal]
|
|
</PRE>
|
|
<P>
|
|
e.g.
|
|
<PRE>GET("http://example.com/logo") =
|
|
{...GIF data..., ...PNG data...}
|
|
</PRE>
|
|
<H1>
|
|
The Web Varies over Time
|
|
</H1>
|
|
<P>
|
|
one day I find:
|
|
<PRE>GET("http://example.com", t1) =
|
|
{"<html><head><title>Example</title> ...</html>", ...}
|
|
</PRE>
|
|
<P>
|
|
and the next:
|
|
<PRE>GET("http://example.com", t2) =
|
|
{"<html><head><title>Example Company</title> ...</html>", ... }
|
|
</PRE>
|
|
<P>
|
|
so how about
|
|
<P>
|
|
GET : URI, Time -> Set[Literal]
|
|
<P>
|
|
but:
|
|
<UL>
|
|
<LI>
|
|
who's time? client's? servers'? are they syncrhonized?
|
|
<LI>
|
|
is this <TT>Set[Literal]</TT> ever observeable?
|
|
<LI>
|
|
... and other issues
|
|
</UL>
|
|
<H1>
|
|
The HTTP Trait
|
|
</H1>
|
|
<P>
|
|
<A HREF="../../../XML/9711theory/HTTP">HTTP trait</A>
|
|
<PRE>...
|
|
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.
|
|
</PRE>
|
|
<H1>
|
|
The 200 OK Axiom
|
|
</H1>
|
|
<PRE> http(i, mq, mp, reqData, repData)
|
|
/\ method(reqData) = GET
|
|
/\ status(repData) = OK
|
|
=> represents(mp, i, content(repData));
|
|
</PRE>
|
|
<H1>
|
|
The Origin Server Axiom, TCP/IP/DNS case
|
|
</H1>
|
|
<PRE> %
|
|
% 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)]);
|
|
|
|
|
|
</PRE>
|
|
<H1>
|
|
The Conditional GET Axiom, If_Modified_Since case
|
|
</H1>
|
|
<P>
|
|
Ari Luotonen and Kevin Altis<BR>
|
|
<CITE><A href='http://www1.cern.ch/PapersWWW94/luotonen.ps'>World-Wide Web
|
|
Proxies</A></CITE><BR>
|
|
Proceedings of the 1st International WWW Conference, May 1994.
|
|
<PRE>
|
|
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?
|
|
|
|
|
|
</PRE>
|
|
</BODY></HTML>
|