all.htm 5.47 KB

Raw Blame History Permalink

<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-&gt;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 -&gt; Literal
</PRE>
<P>
e.g.
<PRE>GET("http://example.com") =
	"&lt;html&gt;&lt;head&gt;&lt;title&gt;Example&lt;/title&gt; ...&lt;/html&gt;"
</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 -&gt; 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) =
	{"&lt;html&gt;&lt;head&gt;&lt;title&gt;Example&lt;/title&gt; ...&lt;/html&gt;", ...}
</PRE>
<P>
and the next:
<PRE>GET("http://example.com", t2) =
	{"&lt;html&gt;&lt;head&gt;&lt;title&gt;Example Company&lt;/title&gt; ...&lt;/html&gt;", ... }
</PRE>
<P>
so how about
<P>
GET : URI, Time -&gt; 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 -&gt; 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
        =&gt; 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

        =&gt; 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 &lt; mq2
        /\ http(i, mq2, mp2, reqData2, repData2)
        /\ method(reqData2) = GET
        /\ Last_Modified(repData) = If_Modified_Since(reqData2)
        /\ status(repData2) = NotModified
        =&gt; represents(mp2, i, cbody);

        % The Conditional GET Axiom, If_None_Match case
        http(i, mq, mp, reqData, repData)
        /\ represents(mp, i, cbody)
        /\ mp &lt; 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)
        =&gt; represents(mp2, i, cbody); % implied metadata?


</PRE>
</BODY></HTML>