% $Id: TTL.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
% [RFC 1035] Mockapetris, P., "Domain names - implementation and
% specification", STD 13, RFC 1035, November 1987.
% for m1 < m2 read: m1 happened before m2
% The Scalar sort is usually the integers, representing seconds;
% but as long as there's a strict partial order, we don't care
% whether you use floating points or reals or whatever.
% Hm... not even sure I need +.
AbelianGroup(+ for \circ, Scalar for T)
TTL: Message → Scalar % DNS time to live, HTTP max-age
fresh: Message, Message, Scalar → Bool
% for fresh(m1, m2, s) read:
% m2 was sent within s of when m1 was received
asserts ∀ m1, m2, m3: Message, s, t: Scalar
fresh(m1, m2, s) ⇒ m1 < m2;
s < t ∧ fresh(m1, m2, s) ⇒ fresh(m1, m2, t);
fresh(m1, m3, s) ∧ m1 < m2 ∧ m2 < m3 ⇒
fresh(m1, m2, s);
HTML generated using lsl2html.