% $Id: Seq.lsl,v 1.2 2000/01/17 21:33:40 connolly Exp $
%
% For some strange reason, the Sequence trait in the LSL handbook
% includes order on E. This is the same trait less that
% constraint on E.
Seq (E, C): trait
% Comparison, subsequences
includes
String(E, C for String[E])
introduces
isPrefix, isSubstring, isSubsequence: C, C ® Bool
find: C, C ® Int
asserts " e, e1, e2: E, s, s1, s2: C
isPrefix(s1, s2) = (s1 = prefix(s2, len(s1)));
isSubstring(s1, s2) =
isPrefix(s1, s2) Ú isSubstring(s1, tail(s2));
isSubsequence(empty, s);
ØisSubsequence(e -| s, empty);
isSubsequence(e1 -| s1, e2 -| s2) =
(e1 = e2 Ù isSubsequence(s1, s2))
Ú isSubsequence(e1 -| s1, s2);
find(empty, empty) = 0;
find(s1, e -| s2) =
(if isPrefix(s1, e -| s2) then 0
else find(s1, s2) + 1)
implies
IsPO (isPrefix, C),
IsPO (isSubstring, C),
IsPO (isSubsequence, C)
" s, s1, s2: C, i, n: Int
isPrefix(prefix(s, n), s);
isSubstring(substring(s, i, n), s);
isSubstring(s1, s2) Þ isSubsequence(s1, s2)
converts
isPrefix, isSubstring, isSubsequence, find
exempting " s: C, e: E find(e -| s, empty)
[Index]
[source]
HTML generated using lsl2html.