% $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.
% http://www.faqs.org/rfcs/rfc1035.html

TTL: trait
  includes
    StrictPartialOrder(<, Message),
% 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 +.
    StrictPartialOrder(<, Scalar),
    AbelianGroup(+ for \circ, Scalar for T)

  introduces
    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);

[Index]

HTML generated using lsl2html.