% $Id: HTTP.html,v 1.1 2003/10/01 07:22:16 connolly Exp $

c.f.
Hypertext Transfer Protocol -- HTTP/1.1
RFC 2616 Fielding, et al. June 1999

HTTP: trait

   includes
       TTL,
       DNS,
       WebState, WebSemantics,
       ReliableTransport,
       List(Literal),
       String(HTTPFormat)
% @@LARCHBUG: I mean a sequence of HTTPFormats indexed by
% non-negative integers,
% but the larch Sequence trait assumes a strict partial order
% on E and defines things like lexicographic order. Sounds like
% a string to me, but the larch folks call it a Sequence. Go figure.

   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.

      HTTPURISchemeID: → URISchemeID
      host: absoluteURI → DomainName
% e.g. host(http://www.w3.org) = www.w3.org
      port: absoluteURI → PortNum
% e.g. port(http://www.w3.org:8080) = 8080
% port(http://www.w3.org) = 80
      account: absoluteURI → AccountName
      nil: → AccountName
% e.g. path(http://foo@www.w3.org/index.html) = foo

% type system of sorts...
% hmm... @@idea for rdf-comments: does the data: URI scheme
% map all literals to URIs? I think so.
% hmm... connection to XML datatypes
      hostAddr: Literal → HostAddr
% e.g. 207.37.25.124

      host: Channel→HostAddr
      port: Channel → PortNum
% if chan is a TCP endpoint, then host(chan) is
% the IP address of the channel and port(chan) is its port


      http: Message, Message, HTTPFormat, HTTPFormat → Bool
% for http(r, q, fr, fq) read: r and q are the
% request and reply messages of a conforming HTTP transaction and
% fr is the parsed data from r and fq is the parsed data from q.

      httpParseReqs: ByteSequence, String[HTTPFormat] → Bool
      httpParseReps: ByteSequence,  String[HTTPFormat] → Bool
% for httpParseReqs(bytes, msgdatalist) read: bytes parses
% per the HTTP grammar as a list of HTTPFormats msgdatalist.

      path: HTTPFormat → PathName
      host: HTTPFormat → DomainName % Host: xyx
      content: HTTPFormat → Literal

      method: HTTPFormat → Method
      GET: → Method

      status: HTTPFormat → StatusCode
      OK: → StatusCode % 200
      NotModified: → StatusCode % 304

      ETag: HTTPFormat → Literal
      Last_Modified: HTTPFormat → Literal
      If_Modified_Since: HTTPFormat → Literal
      If_None_Match: HTTPFormat → List[Literal]



   asserts ∀ i:absoluteURI,
                   mq, mp, ma, mq2, mp2:Message,
                   reqData, repData, reqData2, repData2: HTTPFormat,
                   cmsgs, smsgs: String[HTTPFormat],
                   lit1, cbody: Literal,
                   ip1: HostAddr

% The GET/200 OK Axiom
% Note that it's independent of scheme(i); i.e.
% the HTTP protocol can be used to get information about
% ftp: URIs, or mid: URIs, etc.
        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
% c.f.
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) ∈ If_None_Match(reqData2) % leave * unspecified for now
        ∧ status(repData2) = NotModified
        ∧ ETag(repData2) = ETag(repData)
        ⇒ represents(mp2, i, cbody); % implied metadata?


[Index]

HTML generated using lsl2html.