% $Id: TTL.lsl,v 1.4 1999/08/10 05:20:22 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]

[source]

HTML generated using lsl2html.