tokenize1 (s, token, l(1)) :=
let
nextString := ++(s[2 ... size(s)]) when size (s) > 1;
in
l ++ [token] when size(s) = 0 else
tokenize1 (nextString, token ++ s[1], l) when s[1] /= " " else
tokenize1 (nextString, "", l ++ [token]) when s[1] = " ";
/* Pre-condition: s is a string (possibly empty).
* Post-condition: returns a list with the strings between the spaces as elements.
* - join the list with " ", and you get the original string.
*
* pre: String (s) -- would this already be given through the type definition,
* assuming we had types in the langauge?
* - also note: eiffel uses "require". I think I used that in my quasi-paper
* on the subject.
* - String (s) is a generator for strings.
*
* post: list (return) [also given by typing?], join (l, " ") = s
*
* Is this pattern reversible? I don't think so - the reverse *is* the join method.
* - Can we get the inverse of a pattern from the postcondition?
*/
tokenize (s) := tokenize1 (s, "", []);