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, "", []);