% $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.