Trying out ACSL, continuing implementation.

43 files changed, 1286 insertions, 1009 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 147f2d0..07d8f30 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -3,6 +3,7 @@ add_subdirectory(core)
 add_subdirectory(knowledge)
 add_subdirectory(pipe)
 add_subdirectory(server)
+add_subdirectory(sequence)
 add_subdirectory(storage)
 
 set(
diff --git a/src/core/CMakeLists.txt b/src/core/CMakeLists.txt
index bc722d7..b864aff 100644
--- a/src/core/CMakeLists.txt
+++ b/src/core/CMakeLists.txt
@@ -2,10 +2,6 @@ set(
    SRC_FILES ${SRC_FILES}
    ${CMAKE_CURRENT_SOURCE_DIR}/char.c
    ${CMAKE_CURRENT_SOURCE_DIR}/index.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_creation.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_from_string.c
-   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_to_string.c
 )
 
 set(SRC_FILES ${SRC_FILES} PARENT_SCOPE)
diff --git a/src/core/char.c b/src/core/char.c
index 9297643..819cd57 100644
--- a/src/core/char.c
+++ b/src/core/char.c
@@ -14,44 +14,6 @@ ZoO_char ZoO_char_to_lowercase (const ZoO_char c)
 }
 
 /* See: "char.c" */
-int ZoO_char_is_banned (const ZoO_char c)
-{
-   switch (c)
-   {
-      case '(':
-      case ')':
-      case '[':
-      case ']':
-      case '{':
-      case '}':
-      case '<':
-      case '>':
-         return 1;
-
-      default:
-         return 0;
-   }
-}
-
-/* See: "char.c" */
-int ZoO_char_is_punctuation (const ZoO_char c)
-{
-   switch (c)
-   {
-      case '!':
-      case ',':
-      case '.':
-      case ':':
-      case ';':
-      case '?':
-         return 1;
-
-      default:
-         return 0;
-   }
-}
-
-/* See: "char.c" */
 int ZoO_word_cmp
 (
    const ZoO_char word_a [const static 1],
diff --git a/src/core/char.h b/src/core/char.h
index 2b4a355..7039563 100644
--- a/src/core/char.h
+++ b/src/core/char.h
@@ -22,23 +22,5 @@ int ZoO_word_cmp
  */
 ZoO_char ZoO_char_to_lowercase (const ZoO_char c);
 
-/*
- * Returns '1' iff {c} should be considered as an punctuation character, '0'
- * otherwise.
- */
-/*@
- @ ensures ((\result == 1) || (\result == 0));
- @*/
-int ZoO_char_is_punctuation (const ZoO_char c);
-
-/*
- * Returns '1' iff containing {c} means the word should not be learned. '0'
- * otherwise.
- */
-/*@
- @ ensures ((\result == 1) || (\result == 0));
- @*/
-int ZoO_word_char_is_banned (const ZoO_char c);
-
 #endif
 
diff --git a/src/core/char_types.h b/src/core/char_types.h
index a2a736c..de0fad2 100644
--- a/src/core/char_types.h
+++ b/src/core/char_types.h
@@ -1,16 +1,5 @@
 #ifndef _ZoO_CORE_CHAR_TYPES_H_
 #define _ZoO_CORE_CHAR_TYPES_H_
-/*
- * FIXME: Does not belong here.
- */
-/*
-enum ZoO_word_property
-{
-   ZoO_WORD_NO_PROPERTY,
-   ZoO_WORD_HAS_NO_LEFT_SEPARATOR,
-   ZoO_WORD_HAS_NO_RIGHT_SEPARATOR
-};
-*/
 
 /* ZoO_char = UTF-8 char */
 typedef char ZoO_char;
diff --git a/src/core/index.c b/src/core/index.c
index 375e0ad..dc52d03 100644
--- a/src/core/index.c
+++ b/src/core/index.c
@@ -35,8 +35,13 @@ ZoO_index ZoO_index_random (void)
    ZoO_index result;
    unsigned char * result_bytes;
 
+   /*@ ghost return 4; @*/ /* Chosen by fair dice roll. */
+                           /* Guaranteed to be random. */
+   /* More seriously, I am not explaining the hack below to Frama-C */
+
    result_bytes = (unsigned char *) &result;
 
+
    for (i = 0; i < sizeof(ZoO_index); ++i)
    {
       result_bytes[i] = random_uchar();
diff --git a/src/core/index.h b/src/core/index.h
index 1417662..eb3c471 100644
--- a/src/core/index.h
+++ b/src/core/index.h
@@ -6,14 +6,19 @@
 /*
  * Returns a random ZoO_index.
  */
+/*@
+   ensures (\result <= ZoO_INDEX_MAX);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random (void);
 
 /*
  * Returns a random ZoO_index, included in [0, limit]
  */
 /*@
- @ ensures (\result <= limit);
- @*/
+   ensures (\result <= limit);
+   assigns \result;
+@*/
 ZoO_index ZoO_index_random_up_to (const ZoO_index limit);
 
 #endif
diff --git a/src/core/index_types.h b/src/core/index_types.h
index a71121c..84a1e20 100644
--- a/src/core/index_types.h
+++ b/src/core/index_types.h
@@ -1,6 +1,12 @@
 #ifndef _ZoO_CORE_INDEX_TYPES_H_
 #define _ZoO_CORE_INDEX_TYPES_H_
 
+/*
+ * ZoO_index is a replacement for size_t. As many indices are stored for every
+ * word learned, having control over which type of variable is used to represent
+ * those indices lets us scale the RAM usage.
+ */
+
 #include <limits.h>
 
 /* Must be unsigned. */
@@ -9,4 +15,9 @@ typedef unsigned int ZoO_index;
 /* Must be > 0. */
 #define ZoO_INDEX_MAX UINT_MAX
 
+
+#if (ZoO_INDEX_MAX > SIZE_MAX)
+   #error "ZoO_index should not be able to go higher than a size_t variable."
+#endif
+
 #endif
diff --git a/src/core/sequence.c b/src/core/sequence.c
deleted file mode 100644
index d7ff9d0..0000000
--- a/src/core/sequence.c
+++ /dev/null
@@ -1,103 +0,0 @@
-#include <stdlib.h>
-#include <string.h>
-
-#include "../core/index.h"
-
-#include "sequence.h"
-
-/*
- * Bypass rendundant ZoO_START_OF_SEQUENCE_ID at the start of a sequence.
- */
-/* ensures (*sequence_offset <= sequence_length) */
-static void bypass_redundant_sos
-(
-   const ZoO_index sequence [const restrict],
-   const ZoO_index sequence_length,
-   ZoO_index sequence_offset [const restrict static 1]
-)
-{
-   ZoO_index i;
-
-   *sequence_offset = 0;
-
-   for (i = 0; i < sequence_length; ++i)
-   {
-      if (sequence[i] != ZoO_START_OF_SEQUENCE_ID)
-      {
-         return;
-      }
-      else if (sequence[i] == ZoO_START_OF_SEQUENCE_ID)
-      {
-         *sequence_offset = i;
-      }
-   }
-}
-
-
-/* See "sequence.h" */
-int ZoO_sequence_cmp
-(
-   const ZoO_index sequence_a [const],
-   ZoO_index sequence_a_length,
-   const ZoO_index sequence_b [const],
-   ZoO_index sequence_b_length
-)
-{
-   ZoO_index min_length, a, b;
-   ZoO_index a_offset, b_offset;
-   ZoO_index i;
-
-   bypass_redundant_sos(sequence_a, sequence_a_length, &a_offset);
-   bypass_redundant_sos(sequence_b, sequence_b_length, &b_offset);
-
-   /*@ requires (*a_offset <= sequence_a_length) @*/
-   sequence_a_length -= a_offset;
-   /*@ requires (*b_offset <= sequence_b_length) @*/
-   sequence_b_length -= b_offset;
-
-   if (sequence_a_length < sequence_b_length)
-   {
-      min_length = sequence_a_length;
-   }
-   else
-   {
-      min_length = sequence_b_length;
-   }
-
-   /*@ ensures (min_length <= sequence_a_length) @*/
-   /*@ ensures (min_length <= sequence_b_length) @*/
-
-   for (i = 0; i < min_length; ++i)
-   {
-      /*@ requires ((i + a_offset) < sequence_a_length) @*/
-      a = sequence_a[i + a_offset];
-      /*@ requires ((i + b_offset) < sequence_b_length) @*/
-      b = sequence_b[i + b_offset];
-
-      if (a < b)
-      {
-         return -1;
-      }
-      else if (b > a)
-      {
-         return 1;
-      }
-      else if ((a == ZoO_END_OF_SEQUENCE_ID) && (b == ZoO_END_OF_SEQUENCE_ID))
-      {
-         return 0;
-      }
-   }
-
-   if (sequence_a_length > sequence_b_length)
-   {
-      return 1;
-   }
-   else if (sequence_a_length < sequence_b_length)
-   {
-      return -1;
-   }
-   else
-   {
-      return 0;
-   }
-}
diff --git a/src/core/sequence.h b/src/core/sequence.h
deleted file mode 100644
index 1e286ab..0000000
--- a/src/core/sequence.h
+++ /dev/null
@@ -1,80 +0,0 @@
-#ifndef _ZoO_CORE_SEQUENCE_H_
-#define _ZoO_CORE_SEQUENCE_H_
-
-#include "../core/char_types.h"
-#include "../core/index_types.h"
-
-#include "../pipe/pipe.h"
-
-#include "../knowledge/knowledge_types.h"
-
-#include "sequence_types.h"
-
-int ZoO_sequence_from_undercase_string
-(
-   const ZoO_char string [const restrict],
-   const ZoO_index string_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-);
-
-/*
- * Creates a sequence containing {initial_word}. The remaining elements of
- * sequence are added according to what is known to {k} as being possible.
- * The resulting sequence starts by ZoO_START_OF_SEQUENCE_ID, and ends by
- * ZoO_END_OF_SEQUENCE_ID. The sequence is allocated by the function. If an
- * error occur, it is unallocated and set to NULL ({sequence_size} is set
- * accordingly).
- * Return:
- *    0 on success.
- *    -1 iff the allocating failed.
- *    -2 iff the sequence initialization failed.
- *    -3 iff an error occured when trying to add elements to the right of the
- *       sequence.
- *    -4 iff an error occured when trying to add elements to the left of the
- *       sequence.
- *    -5 iff the resulting sequence would have been empty.
- * Pre:
- *    (> {markov_order} 0)
- *    (knows {k} {initial_word})
- *    (initialized {k})
- */
-int ZoO_sequence_create_from
-(
-   const ZoO_index initial_word,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const ZoO_index markov_order,
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-);
-
-/*
- * Compares two sequences.
- * ZoO_END_OF_SEQUENCE marks the ending of a sequence, regardless of indicated
- * sequence length, meaning that [10][ZoO_END_OF_SEQUENCE][9] and
- * [10][ZoO_END_OF_SEQUENCE][8] are considered equal. Sequences do not have to
- * contain ZoO_END_OF_SEQUENCE. [10][ZoO_END_OF_SEQUENCE] and [10] are
- * considered different, [10][ZoO_END_OF_SEQUENCE]
- * and [10][ZoO_END_OF_SEQUENCE][ZoO_END_OF_SEQUENCE] are considered equal.
- * Same logic is applyied for ZoO_START_OF_SEQUENCE:
- * [START_OF_SEQUENCE][10] is not [10], but
- * [START_OF_SEQUENCE][START_OF_SEQUENCE][10] and [START_OF_SEQUENCE][10] are
- * the same.
- * Return:
- *    1 iff {sequence_a} should be considered being more than {sequence_b}
- *    0 iff {sequence_a} should be considered being equal to {sequence_b}
- *    -1 iff {sequence_a} should be considered being less than {sequence_b}
- */
-int ZoO_sequence_cmp
-(
-   const ZoO_index sequence_a [const],
-   const ZoO_index sequence_a_length,
-   const ZoO_index sequence_b [const],
-   const ZoO_index sequence_b_length
-);
-
-#endif
diff --git a/src/core/sequence_from_string.c b/src/core/sequence_from_string.c
deleted file mode 100644
index deaec86..0000000
--- a/src/core/sequence_from_string.c
+++ /dev/null
@@ -1,351 +0,0 @@
-#define _POSIX_C_SOURCE 200809L
-#include <stdlib.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../core/char.h"
-#include "../core/index.h"
-
-#include "../pipe/pipe.h"
-
-#include "../knowledge/knowledge.h"
-
-#include "sequence.h"
-
-static int add_word_id_to_sequence
-(
-   const ZoO_index word_id,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   *sequence_length += 1;
-
-   new_sequence =
-      (ZoO_index *) realloc
-      (
-         (void *) *sequence,
-         (((size_t) sequence_length) * sizeof(ZoO_index))
-      );
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR(io, "Unable to reallocate a sequence to add word ids to it.");
-
-      return -1;
-   }
-
-   return 0;
-}
-
-/******************************************************************************/
-/** HANDLING PUNCTUATION ******************************************************/
-/******************************************************************************/
-
-/*
- * Semaphore:
- *    Takes then releases access for {k}.
- */
-static int add_punctuation_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_char punctuation,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_id;
-   ZoO_char as_word[2];
-
-   as_word[0] = punctuation;
-   as_word[1] = '\0';
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if (ZoO_knowledge_find_word_id(k, as_word, 2, &word_id, io) < 0)
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      ZoO_PROG_ERROR
-      (
-         io,
-         "'%s' was defined as a punctuation, was found in a string, yet is not"
-         " defined in the knowledge database.",
-         as_word
-      );
-
-      return -1;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   if (add_word_id_to_sequence(word_id, sequence, sequence_length, io) < 0)
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int word_is_punctuation_terminated
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length
-)
-{
-   return ZoO_char_is_punctuation(string[word_length]);
-}
-
-/******************************************************************************/
-/** HANDLING WORDS ************************************************************/
-/******************************************************************************/
-
-/*
- * Semaphore:
- *    Takes then releases access for {k}.
- */
-static int add_word_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_id;
-   ZoO_char * stored_word;
-
-   if (word_length == 0)
-   {
-      return 0;
-   }
-
-   (void) ZoO_knowledge_lock_access(k, io);
-
-   if
-   (
-      ZoO_knowledge_learn_word
-      (
-         k,
-         (string + word_start),
-         word_length,
-         &word_id,
-         io
-      ) < 0
-   )
-   {
-      (void) ZoO_knowledge_unlock_access(k, io);
-
-      return -1;
-   }
-
-   (void) ZoO_knowledge_unlock_access(k, io);
-
-   if (add_word_id_to_sequence(word_id, sequence, sequence_length, io) < 0)
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int add_finding_to_sequence
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index word_start,
-   const ZoO_index word_length,
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   struct ZoO_knowledge k [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index punctuation;
-
-   if (word_is_punctuation_terminated(string, word_start, word_length))
-   {
-      punctuation = 1;
-   }
-   else
-   {
-      punctuation = 0;
-   }
-
-   if
-   (
-      add_word_to_sequence
-      (
-         string,
-         word_start,
-         (word_length - punctuation),
-         sequence,
-         sequence_length,
-         k,
-         io
-      ) < 0
-   )
-   {
-      return -1;
-   }
-
-   if
-   (
-      (punctuation == 1)
-      &&
-      (
-         add_punctuation_to_sequence
-         (
-            string,
-            string[word_start + word_length - 1],
-            sequence,
-            sequence_length,
-            k,
-            io
-         ) < 0
-      )
-   )
-   {
-      return -1;
-   }
-
-   return 0;
-}
-
-static int find_word
-(
-   const ZoO_char string [const restrict static 1],
-   const ZoO_index string_length,
-   const ZoO_index offset,
-   ZoO_index word_start [const restrict static 1],
-   ZoO_index word_length [const restrict static 1]
-)
-{
-   ZoO_index i;
-
-   i = offset;
-
-   while ((string[i] == ' ') && (i < string_length))
-   {
-      i += 1;
-   }
-
-   if (i >= string_length)
-   {
-      return -1;
-   }
-
-   *word_start = i;
-
-   while ((string[i] != ' ') && (i < string_length))
-   {
-      i += 1;
-   }
-
-   if (i >= string_length)
-   {
-      return -1;
-   }
-
-   *word_length = (i - *word_start);
-
-   return 0;
-}
-
-/******************************************************************************/
-/** EXPORTED ******************************************************************/
-/******************************************************************************/a
-
-/* See: "sequence.h" */
-int ZoO_sequence_from_undercase_string
-(
-   const ZoO_char string [const restrict],
-   const ZoO_index string_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_index * sequence [const restrict static 1],
-   ZoO_index sequence_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index word_start, word_length;
-   ZoO_index i;
-
-   i = 0;
-
-   *sequence = (ZoO_index *) NULL;
-   *sequence_length = 0;
-
-   if
-   (
-      add_word_id_to_sequence
-      (
-         ZoO_START_OF_SEQUENCE_ID,
-         sequence,
-         sequence_length,
-         io
-      ) < 0
-   )
-   {
-      return -1;
-   }
-
-   while (i < string_length)
-   {
-      if (find_word(string, i, string_length, &word_start, &word_length) < 0)
-      {
-         break;
-      }
-
-      if
-      (
-         add_finding_to_sequence
-         (
-            string,
-            word_start,
-            word_length,
-            sequence,
-            sequence_length,
-            k,
-            io
-         ) < 0
-      )
-      {
-         free((void *) *sequence);
-         *sequence = (ZoO_index *) NULL;
-         *sequence_length = 0;
-
-         return -1;
-      }
-
-      i = (word_start + word_length);
-   }
-
-   if
-   (
-      add_word_id_to_sequence
-      (
-         ZoO_END_OF_SEQUENCE_ID,
-         sequence,
-         sequence_length,
-         io
-      ) < 0
-   )
-   {
-      free((void *) *sequence);
-
-      *sequence = (ZoO_index *) NULL;
-      *sequence_length = 0;
-
-      return -1;
-   }
-
-   return 0;
-}
diff --git a/src/core/sequence_to_string.c b/src/core/sequence_to_string.c
deleted file mode 100644
index 16fc859..0000000
--- a/src/core/sequence_to_string.c
+++ /dev/null
@@ -1,97 +0,0 @@
-#define _POSIX_C_SOURCE 200809L
-#include <stdlib.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../core/char.h"
-#include "../core/index.h"
-
-#include "../cli/cli.h"
-
-#include "../knowledge/knowledge.h"
-
-#include "sequence.h"
-
-/* TODO */
-static int add_word
-(
-   const ZoO_index word_id,
-   const size_t destination_size,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_char destination [const restrict static max_destination_length],
-   size_t destination_used_size [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-	const ZoO_char * word;
-	size_t word_size;
-
-	(void) ZoO_knowledge_lock_access(k, io);
-	ZoO_knowledge_get_word(k, word_id, &word, &word_size, io);
-	(void) ZoO_knowledge_unlock_access(k, io);
-
-	if ((destination_used_size + word_size) > max_destination_length)
-	{
-	}
-
-	if
-	(
-		(word_size == 2)
-		&& ZoO_char_is_punctuation(word[0])
-	)
-	{
-		snprintf
-		(
-			(destination + *destination_used_size),
-			word_size,
-			ZoO_CHAR_STRING_SYMBOL,
-			current_sentence
-		);
-	}
-	else
-	{
-	}
-
-   return 0;
-}
-/******************************************************************************/
-/** EXPORTED ******************************************************************/
-/******************************************************************************/
-
-int ZoO_sequence_to_undercase_string
-(
-   const ZoO_index sequence [const restrict static 1],
-   const ZoO_index sequence_length,
-   const ZoO_index max_destination_length,
-   struct ZoO_knowledge k [const restrict static 1],
-   ZoO_char destination [const restrict static max_destination_length],
-   ZoO_index destination_length [const restrict static 1],
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index i;
-   const ZoO_index actual_length = (sequence_length - 1);
-
-   for (i = 0; i < actual_length; ++i)
-   {
-      if
-      (
-         add_word
-         (
-            sequence[i],
-            max_destination_length,
-            k,
-            destination,
-            destination_length,
-            io
-         ) < 0
-      )
-      {
-         *destination_length = 0;
-
-         return -1;
-      }
-   }
-
-   return 0;
-}
diff --git a/src/knowledge/knowledge.c b/src/knowledge/knowledge.c
index 95683b9..463d40b 100644
--- a/src/knowledge/knowledge.c
+++ b/src/knowledge/knowledge.c
@@ -26,6 +26,7 @@ int ZoO_knowledge_lock_access
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
+   /* TODO */
    return 0;
 }
 
@@ -35,4 +36,5 @@ void ZoO_knowledge_unlock_access
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
+   /* TODO */
 }
diff --git a/src/knowledge/knowledge.h b/src/knowledge/knowledge.h
index 872bb94..c65ee2c 100644
--- a/src/knowledge/knowledge.h
+++ b/src/knowledge/knowledge.h
@@ -41,7 +41,7 @@ int ZoO_knowledge_learn_word
 (
    struct ZoO_knowledge k [const static 1],
    const ZoO_char word [const restrict static 1],
-   const ZoO_index word_length,
+   const size_t word_length,
    ZoO_index result [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 );
@@ -50,7 +50,7 @@ int ZoO_knowledge_learn_sequence
 (
    struct ZoO_knowledge k [const restrict static 1],
    const ZoO_index sequence [const restrict static 1],
-   const ZoO_index sequence_length,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const struct ZoO_pipe io [const restrict static 1]
 );
@@ -88,7 +88,7 @@ int ZoO_knowledge_get_word
    const struct ZoO_knowledge k [const static 1],
    const ZoO_index word_ref,
    const ZoO_char * word [const restrict static 1],
-   size_t word_size [const restrict static 1],
+   ZoO_index word_size [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 );
 
@@ -125,7 +125,7 @@ int ZoO_knowledge_find_following_words
 (
    const struct ZoO_knowledge k [const static 1],
    const ZoO_index sequence [const restrict],
-   const ZoO_index sequence_length,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const ZoO_index * restrict following_words [const restrict static 1],
    const ZoO_index * restrict following_words_weights [const restrict static 1],
diff --git a/src/knowledge/knowledge_finalize.c b/src/knowledge/knowledge_finalize.c
index 36a7406..9628672 100644
--- a/src/knowledge/knowledge_finalize.c
+++ b/src/knowledge/knowledge_finalize.c
@@ -1,8 +1,4 @@
 #include <stdlib.h>
-#include <string.h>
-#include <stdint.h> /* defines SIZE_MAX */
-
-#include "../cli/cli.h"
 
 #include "knowledge.h"
 
@@ -59,7 +55,7 @@ static void knowledge_word_finalize
    struct ZoO_knowledge_word w [const restrict static 1]
 )
 {
-   w->word_size = 0;
+   w->word_length = 0;
    w->occurrences = 0;
 
    if (w->word != (ZoO_char *) NULL)
diff --git a/src/knowledge/knowledge_learn_markov_sequence.c b/src/knowledge/knowledge_learn_markov_sequence.c
index ec71254..2bd0103 100644
--- a/src/knowledge/knowledge_learn_markov_sequence.c
+++ b/src/knowledge/knowledge_learn_markov_sequence.c
@@ -2,7 +2,7 @@
 #include <string.h>
 #include <stdint.h> /* defines SIZE_MAX */
 
-#include "../core/sequence.h"
+#include "../sequence/sequence.h"
 
 #include "../pipe/pipe.h"
 
@@ -18,15 +18,16 @@ static void set_nth_sequence
    const ZoO_index sequence_id
 )
 {
-   /* Safe: (> k->sequences_length 1) */
    if (sorted_sequence_id < (k->sequences_length - 1))
    {
       memmove
       (
-         /* Safe: (=< (+ sorted_sequence_id 1) k->sequences_length) */
          (void *) (k->sequences_sorted + (sorted_sequence_id + 1)),
          (const void *) (k->sequences_sorted + sorted_sequence_id),
-         ((k->sequences_length - 1) - sorted_sequence_id)
+         (
+            ((size_t) ((k->sequences_length - 1) - sorted_sequence_id))
+            * sizeof(ZoO_index)
+         )
       );
    }
 
diff --git a/src/knowledge/knowledge_learn_sequence.c b/src/knowledge/knowledge_learn_sequence.c
index 7696fbc..35b6d15 100644
--- a/src/knowledge/knowledge_learn_sequence.c
+++ b/src/knowledge/knowledge_learn_sequence.c
@@ -2,7 +2,7 @@
 #include <string.h>
 #include <stdint.h> /* defines SIZE_MAX */
 
-#include "../core/sequence.h"
+#include "../sequence/sequence.h"
 
 #include "../pipe/pipe.h"
 
@@ -15,11 +15,15 @@ static int add_following_sequence
 (
    struct ZoO_knowledge k [const restrict static 1],
    const ZoO_index sequence [const restrict static 1],
-   const ZoO_index index,
-   const ZoO_index sequence_length,
+   const size_t index,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const struct ZoO_pipe io [const restrict static 1]
-);
+)
+{
+   /* TODO */
+   return -1;
+}
 
 /******************************************************************************/
 /** LEARN PRECEDING SEQUENCE **************************************************/
@@ -28,33 +32,32 @@ static int add_preceding_sequence
 (
    struct ZoO_knowledge k [const restrict static 1],
    const ZoO_index sequence [const restrict static 1],
-   const ZoO_index index,
-   const ZoO_index sequence_length,
+   const size_t index,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
+   /* TODO */
+   return -1;
 }
 
 /******************************************************************************/
 /** EXPORTED ******************************************************************/
 /******************************************************************************/
-
 int ZoO_knowledge_learn_sequence
 (
    struct ZoO_knowledge k [const restrict static 1],
    const ZoO_index sequence [const restrict static 1],
-   const ZoO_index sequence_length,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
    ZoO_index * buffer;
-   ZoO_index i;
+   size_t i;
    const ZoO_index buffer_length = (markov_order - 1);
 
-   /* TODO */
-
    for (i = 0; i < sequence_length; ++i)
    {
       k->words[sequence[i]].occurrences += 1;
diff --git a/src/knowledge/knowledge_learn_word.c b/src/knowledge/knowledge_learn_word.c
index e6979dc..33a2bf1 100644
--- a/src/knowledge/knowledge_learn_word.c
+++ b/src/knowledge/knowledge_learn_word.c
@@ -30,7 +30,7 @@ static void initialize_word
 )
 {
    w->word = (const ZoO_char *) NULL;
-   w->word_size = 0;
+   w->word_length = 0;
    w->occurrences = 0;
 
    initialize_sequence_collection(&(w->followed));
@@ -53,7 +53,7 @@ static ZoO_char * copy_word
       (ZoO_char *)
       calloc
       (
-         (size_t) (original_length + 1),
+         original_length,
          sizeof(ZoO_char)
       );
 
@@ -71,8 +71,6 @@ static ZoO_char * copy_word
       (((size_t) original_length) * sizeof(ZoO_char))
    );
 
-   result[original_length] = '\0';
-
    return 0;
 }
 
@@ -86,7 +84,8 @@ static int reallocate_words_list
 
    if
    (
-      (SIZE_MAX / sizeof(struct ZoO_knowledge_word)) > (size_t) k->words_length
+      (SIZE_MAX / sizeof(struct ZoO_knowledge_word))
+      > (size_t) k->words_length
    )
    {
       ZoO_S_ERROR
@@ -135,7 +134,7 @@ static int reallocate_words_sorted_list
     * whose size is bigger than a ZoO_index.
     * */
    /*
-   if ((SIZE_MAX / sizeof(ZoO_index)) > (size_t) k->words_length)
+   if ((SIZE_MAX / sizeof(ZoO_index)) > k->words_length)
    {
       ZoO_S_ERROR
       (
@@ -185,7 +184,10 @@ static void set_nth_word
          /* Safe: (=< (+ sorted_word_id 1) k->words_length) */
          (void *) (k->words_sorted + (sorted_word_id + 1)),
          (const void *) (k->words_sorted + sorted_word_id),
-         ((k->words_length - 1) - sorted_word_id)
+         (
+            ((size_t) ((k->words_length - 1) - sorted_word_id))
+            * sizeof(ZoO_index)
+         )
       );
    }
 
@@ -235,7 +237,7 @@ static int add_word
    initialize_word(k->words + word_id);
 
    k->words[word_id].word = stored_word;
-   k->words[word_id].word_size = ((word_length + 1) * sizeof(ZoO_char));
+   k->words[word_id].word_length = word_length;
 
    if (reallocate_words_sorted_list(k, io) < 0)
    {
@@ -257,22 +259,28 @@ int ZoO_knowledge_learn_word
 (
    struct ZoO_knowledge k [const restrict static 1],
    const ZoO_char word [const restrict static 1],
-   const ZoO_index word_length,
+   const size_t word_length,
    ZoO_index word_id [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
    ZoO_index sorted_id;
 
+   if (word_length >= (size_t) ZoO_INDEX_MAX)
+   {
+      ZoO_S_ERROR(io, "Word is too long to be learned.");
+
+      return -1;
+   }
+
    if
    (
       ZoO_knowledge_find_word_id
       (
          k,
          word,
-         (word_length * sizeof(ZoO_char)),
-         word_id,
-         io
+         (((size_t) word_length) * sizeof(ZoO_char)),
+         word_id
       ) == 0
    )
    {
@@ -282,5 +290,5 @@ int ZoO_knowledge_learn_word
    sorted_id = *word_id;
    *word_id = k->words_length;
 
-   return add_word(k, word, word_length, *word_id, sorted_id, io);
+   return add_word(k, word, (ZoO_index) word_length, *word_id, sorted_id, io);
 }
diff --git a/src/knowledge/knowledge_search.c b/src/knowledge/knowledge_search.c
index 23aab71..4ea4572 100644
--- a/src/knowledge/knowledge_search.c
+++ b/src/knowledge/knowledge_search.c
@@ -2,7 +2,7 @@
 
 #include "../core/char.h"
 #include "../core/index.h"
-#include "../core/sequence.h"
+#include "../sequence/sequence.h"
 
 #include "../pipe/pipe.h"
 
@@ -13,7 +13,7 @@ int ZoO_knowledge_find_word_id
 (
    const struct ZoO_knowledge k [const restrict static 1],
    const ZoO_char word [const restrict static 1],
-   const size_t word_size,
+   const size_t word_length,
    ZoO_index result [const restrict static 1]
 )
 {
@@ -40,7 +40,7 @@ int ZoO_knowledge_find_word_id
    {
       i = (current_min + ((current_max - current_min) / 2));
 
-      cmp = ZoO_word_cmp(word, word_size, k->words[k->words_sorted[i]].word);
+      cmp = ZoO_word_cmp(word, word_length, k->words[k->words_sorted[i]].word);
 
       if (cmp > 0)
       {
@@ -211,7 +211,7 @@ int ZoO_knowledge_find_following_words
 (
    const struct ZoO_knowledge k [const static 1],
    const ZoO_index sequence [const restrict],
-   const ZoO_index sequence_length,
+   const size_t sequence_length,
    const ZoO_index markov_order,
    const ZoO_index * restrict following_words [const restrict static 1],
    const ZoO_index * restrict following_words_weights [const restrict static 1],
@@ -224,14 +224,15 @@ int ZoO_knowledge_find_following_words
    ZoO_index i, current_min, current_max, local_sequence;
    const ZoO_index * restrict candidate;
    const ZoO_index markov_sequence_length = (markov_order - 1);
-   const ZoO_index sequence_offset =
-      ((sequence_length - markov_sequence_length) - 1);
+   const size_t sequence_offset =
+      ((sequence_length - ((size_t) markov_sequence_length)) - 1);
    const ZoO_index word = sequence[sequence_offset];
 
    if (word >= k->words_length)
    {
       ZoO_S_ERROR
       (
+         io,
          "Attempting to find the following words of an unknown word."
       );
 
diff --git a/src/knowledge/knowledge_types.h b/src/knowledge/knowledge_types.h
index 7eafc8b..4962991 100644
--- a/src/knowledge/knowledge_types.h
+++ b/src/knowledge/knowledge_types.h
@@ -18,7 +18,7 @@ struct ZoO_knowledge_sequence_collection
 struct ZoO_knowledge_word
 {
    const ZoO_char * word;
-   size_t word_size;
+   ZoO_index word_length;
    ZoO_index occurrences;
    struct ZoO_knowledge_sequence_collection followed;
    struct ZoO_knowledge_sequence_collection preceded;
@@ -32,7 +32,6 @@ struct ZoO_knowledge
    ZoO_index ** sequences;
    ZoO_index sequences_length;
    ZoO_index * sequences_sorted;
-   ZoO_index sequences_length;
 };
 
 #endif
diff --git a/src/cli/CMakeLists.txt b/src/parameters/CMakeLists.txt
index 94e6337..94e6337 100644
--- a/src/cli/CMakeLists.txt
+++ b/src/parameters/CMakeLists.txt
diff --git a/src/cli/parameters.c b/src/parameters/parameters.c
index 82ac9d1..82ac9d1 100644
--- a/src/cli/parameters.c
+++ b/src/parameters/parameters.c
diff --git a/src/cli/parameters.h b/src/parameters/parameters.h
index 7927ef7..7927ef7 100644
--- a/src/cli/parameters.h
+++ b/src/parameters/parameters.h
diff --git a/src/cli/parameters_types.h b/src/parameters/parameters_types.h
index f9ca88b..f9ca88b 100644
--- a/src/cli/parameters_types.h
+++ b/src/parameters/parameters_types.h
diff --git a/src/pipe/pipe.c b/src/pipe/pipe.c
index e69de29..8f414f5 100644
--- a/src/pipe/pipe.c
+++ b/src/pipe/pipe.c
@@ -0,0 +1 @@
+/* TODO */
diff --git a/src/pipe/pipe.h b/src/pipe/pipe.h
index ea31b55..3c5fd44 100644
--- a/src/pipe/pipe.h
+++ b/src/pipe/pipe.h
@@ -143,4 +143,5 @@
       }\
    )
 
+/* TODO: add missing pipe functions */
 #endif
diff --git a/src/pipe/pipe_types.h b/src/pipe/pipe_types.h
index 15b4a54..cfeb514 100644
--- a/src/pipe/pipe_types.h
+++ b/src/pipe/pipe_types.h
@@ -1,5 +1,5 @@
 #ifndef _ZoO_PIPE_PIPE_TYPES_H_
-#define _ZoO_PIPE_PIPE_TYPESH_
+#define _ZoO_PIPE_PIPE_TYPES_H_
 
 #include <stdio.h>
 
@@ -8,6 +8,12 @@ struct ZoO_pipe
    FILE * out;
    FILE * in;
 };
-   const struct ZoO_pipe io [const restrict static 1]
+
+struct ZoO_pipe_names
+{
+   char request_pipe[255];
+   char reply_pipe[255];
+};
+//   const struct ZoO_pipe io [const restrict static 1]
 
 #endif
diff --git a/src/sequence/CMakeLists.txt b/src/sequence/CMakeLists.txt
new file mode 100644
index 0000000..1186557
--- /dev/null
+++ b/src/sequence/CMakeLists.txt
@@ -0,0 +1,11 @@
+set(
+   SRC_FILES ${SRC_FILES}
+   ${CMAKE_CURRENT_SOURCE_DIR}/sequence.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_append.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_creation.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_from_string.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/sequence_to_string.c
+)
+
+set(SRC_FILES ${SRC_FILES} PARENT_SCOPE)
+
diff --git a/src/sequence/sequence.c b/src/sequence/sequence.c
new file mode 100644
index 0000000..852b05c
--- /dev/null
+++ b/src/sequence/sequence.c
@@ -0,0 +1,170 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "../core/index.h"
+
+#include "sequence.h"
+
+/*
+ * Bypass rendundant ZoO_START_OF_SEQUENCE_ID at the start of a sequence.
+ */
+/*@
+   requires
+   (
+      \valid(sequence+ (0 .. sequence_length))
+      || (sequence_length == 0)
+   );
+   requires \separated(sequence, sequence_offset);
+
+   assigns (*sequence_offset);
+
+   ensures (*sequence_offset < sequence_length);
+
+   ensures
+   (
+      (*sequence_offset == 0)
+      || (sequence[0 .. *sequence_offset] == ZoO_START_OF_SEQUENCE_ID)
+   );
+
+   ensures
+   (
+      (*sequence_offset == sequence_length)
+      || (sequence[*sequence_offset + 1] != ZoO_START_OF_SEQUENCE_ID)
+   );
+
+@*/
+static void bypass_redundant_sos
+(
+   const ZoO_index sequence [const restrict],
+   const size_t sequence_length,
+   size_t sequence_offset [const restrict static 1]
+)
+{
+   ZoO_index i;
+
+   *sequence_offset = 0;
+
+   /*@
+      loop invariant 0 <= i <= sequence_length;
+      loop invariant (*sequence_offset <= i);
+      loop invariant
+      (
+         (*sequence_offset == 0)
+         || (sequence[*sequence_offset] == ZoO_START_OF_SEQUENCE_ID)
+      );
+      loop invariant
+         (
+            (i == 0) || (sequence[0 .. (i - 1)] == ZoO_START_OF_SEQUENCE_ID)
+         );
+      loop assigns i, *sequence_offset;
+      loop variant (sequence_length - i);
+   @*/
+   for (i = 0; i < sequence_length; ++i)
+   {
+      if (sequence[i] != ZoO_START_OF_SEQUENCE_ID)
+      {
+         return;
+      }
+      else if (sequence[i] == ZoO_START_OF_SEQUENCE_ID)
+      {
+         *sequence_offset = i;
+      }
+   }
+}
+
+
+/* See "sequence.h" */
+/*@
+   \requires
+   (
+      \valid(sequence_a+ (0 .. sequence_a_length))
+      || (sequence_a_length == 0)
+   );
+
+   \requires
+   (
+      \valid(sequence_b+ (0 .. sequence_b_length))
+      || (sequence_b_length == 0)
+   );
+
+   assigns \result;
+@*/
+int ZoO_sequence_cmp
+(
+   const ZoO_index sequence_a [const],
+   size_t sequence_a_length,
+   const ZoO_index sequence_b [const],
+   size_t sequence_b_length
+)
+{
+   size_t min_length, a, b;
+   size_t a_offset, b_offset;
+   size_t i;
+   /*@ ghost size_t actual_a_length, actual_b_length; @*/
+
+   bypass_redundant_sos(sequence_a, sequence_a_length, &a_offset);
+   bypass_redundant_sos(sequence_b, sequence_b_length, &b_offset);
+
+   /*@ ghost actual_a_length = sequence_a_length; @*/
+   /*@ ghost actual_b_length = sequence_b_length; @*/
+
+   /*@ assert (a_offset <= sequence_a_length); @*/
+   sequence_a_length -= a_offset;
+   /*@ assert (b_offset <= sequence_b_length); @*/
+   sequence_b_length -= b_offset;
+
+   if (sequence_a_length < sequence_b_length)
+   {
+      min_length = sequence_a_length;
+   }
+   else
+   {
+      min_length = sequence_b_length;
+   }
+
+   /*@ assert (min_length <= sequence_a_length); @*/
+   /*@ assert (min_length <= sequence_b_length); @*/
+
+   /*@ assert (min_length + a_offset <= actual_a_length); @*/
+   /*@ assert (min_length + b_offset <= actual_b_length); @*/
+
+   /*@
+      loop invariant 0 <= i <= min_length;
+      loop assigns i;
+      loop variant (min_length - i);
+   @*/
+   for (i = 0; i < min_length; ++i)
+   {
+      /*@ assert ((i + a_offset) < actual_a_length); @*/
+      a = sequence_a[i + a_offset];
+      /*@ assert ((i + b_offset) < actual_b_length); @*/
+      b = sequence_b[i + b_offset];
+
+      if (a < b)
+      {
+         return -1;
+      }
+      else if (b > a)
+      {
+         return 1;
+      }
+      else if ((a == ZoO_END_OF_SEQUENCE_ID) && (b == ZoO_END_OF_SEQUENCE_ID))
+      {
+         return 0;
+      }
+   }
+
+   if (sequence_a_length > sequence_b_length)
+   {
+      return 1;
+   }
+   else if (sequence_a_length < sequence_b_length)
+   {
+      return -1;
+   }
+   else
+   {
+      return 0;
+   }
+}
+
diff --git a/src/sequence/sequence.h b/src/sequence/sequence.h
new file mode 100644
index 0000000..d1ac16f
--- /dev/null
+++ b/src/sequence/sequence.h
@@ -0,0 +1,208 @@
+#ifndef _ZoO_CORE_SEQUENCE_H_
+#define _ZoO_CORE_SEQUENCE_H_
+
+/* Defines SIZE_MAX */
+#include <stdint.h>
+
+#include "../core/char_types.h"
+#include "../core/index_types.h"
+
+#include "../pipe/pipe.h"
+
+#include "../knowledge/knowledge_types.h"
+
+#include "sequence_types.h"
+
+/*@
+   requires \valid(sequence);
+   requires \valid(*sequence);
+   requires \valid(sequence_capacity);
+   requires \valid(io);
+   requires ((sequence_required_capacity * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires (*sequence_capacity >= 0);
+   requires (*sequence_capacity <= SIZE_MAX);
+   requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires \separated(sequence, sequence_capacity, io);
+
+   ensures
+   (
+      (
+         (\result >= 0)
+         && (*sequence_capacity >= sequence_required_capacity)
+         && ((*sequence_capacity * sizeof(ZoO_index)) <= SIZE_MAX)
+      )
+      || (\result < 0)
+   );
+
+   behavior successful_reallocation:
+      assigns (*sequence);
+      assigns (*sequence_capacity);
+
+      ensures (\result > 0);
+      ensures ((*sequence_capacity) == sequence_required_capacity);
+      ensures \valid(sequence);
+
+   behavior already_done:
+      assigns \nothing;
+
+      ensures (\result == 0);
+      ensures ((*sequence_capacity) >= sequence_required_capacity);
+
+   behavior failure:
+      assigns \nothing;
+
+      ensures (\result < 0);
+
+   complete behaviors;
+   disjoint behaviors;
+@*/
+int ZoO_sequence_ensure_capacity
+(
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   const size_t sequence_required_capacity,
+   const struct ZoO_pipe io [const restrict static 1]
+);
+
+int ZoO_sequence_from_undercase_string
+(
+   const ZoO_char string [const restrict],
+   const size_t string_length,
+   struct ZoO_knowledge k [const restrict static 1],
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+);
+
+/*
+ * Creates a sequence containing {initial_word}. The remaining elements of
+ * sequence are added according to what is known to {k} as being possible.
+ * The resulting sequence starts by ZoO_START_OF_SEQUENCE_ID, and ends by
+ * ZoO_END_OF_SEQUENCE_ID. The sequence is allocated by the function. If an
+ * error occur, it is unallocated and set to NULL ({sequence_size} is set
+ * accordingly).
+ * Return:
+ *    0 on success.
+ *    -1 iff the allocating failed.
+ *    -2 iff the sequence initialization failed.
+ *    -3 iff an error occured when trying to add elements to the right of the
+ *       sequence.
+ *    -4 iff an error occured when trying to add elements to the left of the
+ *       sequence.
+ *    -5 iff the resulting sequence would have been empty.
+ * Pre:
+ *    (> {markov_order} 0)
+ *    (knows {k} {initial_word})
+ *    (initialized {k})
+ */
+int ZoO_sequence_create_from
+(
+   const ZoO_index initial_word,
+   size_t credits [const restrict],
+   struct ZoO_knowledge k [const restrict static 1],
+   const ZoO_index markov_order,
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+);
+
+/*@
+   requires \valid(sequence_length);
+   requires \valid(io);
+   requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires \separated(sequence, sequence_capacity, sequence_length, io);
+
+   behavior success:
+      assigns (*sequence_length);
+      assigns (*sequence[0]);
+      assigns (*sequence_capacity);
+
+      ensures (\result >= 0);
+      ensures ((*sequence_length > \old(*sequence_length)));
+
+   behavior could_not_increase_length:
+      ensures (\result == -1);
+
+      assigns (*sequence_length);
+
+   behavior could_not_reallocate:
+      ensures (\result < -1);
+
+   complete behaviors;
+   disjoint behaviors;
+@*/
+int ZoO_sequence_append_left
+(
+   const ZoO_index word_id,
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+);
+
+/*@
+   requires \valid(*sequence);
+   requires \valid(sequence_capacity);
+   requires \valid(sequence_length);
+   requires \valid(io);
+   requires (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires (((*sequence_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+   requires \separated(sequence, sequence_capacity, sequence_length, io);
+
+   behavior success:
+      assigns (*sequence_length);
+      assigns (*sequence);
+      assigns (*sequence_capacity);
+
+      ensures (\result >= 0);
+      ensures ((*sequence_length > \old(*sequence_length)));
+
+   behavior could_not_increase_length:
+      ensures (\result == -1);
+
+      assigns (*sequence_length);
+
+   behavior could_not_reallocate:
+      ensures (\result < -1);
+
+   complete behaviors;
+   disjoint behaviors;
+@*/
+int ZoO_sequence_append_right
+(
+   ZoO_index * sequence [const restrict static 1],
+   const ZoO_index word_id,
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+);
+
+/*
+ * Compares two sequences.
+ * ZoO_END_OF_SEQUENCE marks the ending of a sequence, regardless of indicated
+ * sequence length, meaning that [10][ZoO_END_OF_SEQUENCE][9] and
+ * [10][ZoO_END_OF_SEQUENCE][8] are considered equal. Sequences do not have to
+ * contain ZoO_END_OF_SEQUENCE. [10][ZoO_END_OF_SEQUENCE] and [10] are
+ * considered different, [10][ZoO_END_OF_SEQUENCE]
+ * and [10][ZoO_END_OF_SEQUENCE][ZoO_END_OF_SEQUENCE] are considered equal.
+ * Same logic is applyied for ZoO_START_OF_SEQUENCE:
+ * [START_OF_SEQUENCE][10] is not [10], but
+ * [START_OF_SEQUENCE][START_OF_SEQUENCE][10] and [START_OF_SEQUENCE][10] are
+ * the same.
+ * Return:
+ *    1 iff {sequence_a} should be considered being more than {sequence_b}
+ *    0 iff {sequence_a} should be considered being equal to {sequence_b}
+ *    -1 iff {sequence_a} should be considered being less than {sequence_b}
+ */
+int ZoO_sequence_cmp
+(
+   const ZoO_index sequence_a [const],
+   size_t sequence_a_length,
+   const ZoO_index sequence_b [const],
+   size_t sequence_b_length
+);
+
+#endif
diff --git a/src/sequence/sequence_append.c b/src/sequence/sequence_append.c
new file mode 100644
index 0000000..a119d8b
--- /dev/null
+++ b/src/sequence/sequence_append.c
@@ -0,0 +1,212 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <stdint.h> /* defines SIZE_MAX */
+
+#include "../core/index.h"
+
+#include "../pipe/pipe.h"
+
+#include "sequence.h"
+
+/******************************************************************************/
+/** MEMORY (RE)ALLOCATION *****************************************************/
+/******************************************************************************/
+
+/*@
+   requires \valid(required_capacity);
+   requires \valid(io);
+   requires (*required_capacity >= 0);
+   requires (*required_capacity <= SIZE_MAX);
+   requires \separated(required_capacity, io);
+
+   assigns \result;
+
+   ensures (*required_capacity >= 0);
+
+   behavior success:
+      assigns (*required_capacity);
+
+      ensures (\result >= 0);
+      ensures ((*required_capacity) == (\old(*required_capacity) + 1));
+      ensures (((*required_capacity) * sizeof(ZoO_index)) <= SIZE_MAX);
+
+   behavior failure:
+      assigns \nothing;
+
+      ensures (\result < 0);
+
+   complete behaviors;
+   disjoint behaviors;
+@*/
+static int increment_required_capacity
+(
+   size_t required_capacity [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   if
+   (
+      (*required_capacity == SIZE_MAX)
+      || ((SIZE_MAX / sizeof(ZoO_index)) <= (*required_capacity + 1))
+   )
+   {
+      /*@ assert \valid(io); @*/
+      /*@ ghost return -1; @*/
+      ZoO_S_ERROR
+      (
+         io,
+         "Sequence capacity increment aborted, as the new size would not fit"
+         " in a size_t variable."
+      );
+
+      return -1;
+   }
+
+   /*@ assert ((*required_capacity) < SIZE_MAX); @*/
+   /*@ assert \valid(required_capacity); @*/
+   *required_capacity = (*required_capacity + 1);
+
+   /* assert (((*required_capacity) * sizeof(ZoO_index)) <= SIZE_MAX); @*/
+
+   return 0;
+}
+
+/******************************************************************************/
+/** EXPORTED ******************************************************************/
+/******************************************************************************/
+
+int ZoO_sequence_ensure_capacity
+(
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   const size_t sequence_required_capacity,
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   ZoO_index * new_sequence;
+
+   if (sequence_required_capacity <= *sequence_capacity)
+   {
+      return 0;
+   }
+
+   /*@
+      assert
+      (
+         sequence_required_capacity
+         <= (SIZE_MAX / sizeof(ZoO_index))
+      );
+   @*/
+   /*@ assert \valid(sequence); @*/
+   /*@ assert \valid(*sequence); @*/
+
+   new_sequence =
+      (ZoO_index *) realloc
+      (
+         (void *) *sequence,
+         (sequence_required_capacity * sizeof(ZoO_index))
+      );
+
+   if (new_sequence == (ZoO_index *) NULL)
+   {
+      /*@ assert \valid(io); @*/
+      /*@ ghost return -1; @*/
+
+      ZoO_S_ERROR
+      (
+         io,
+         "Unable to reallocate memory to match sequence's required size."
+      );
+
+      return -1;
+   }
+
+   *sequence_capacity = sequence_required_capacity;
+   *sequence = new_sequence;
+
+   return 1;
+}
+
+int ZoO_sequence_append_left
+(
+   const ZoO_index word_id,
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   if (increment_required_capacity(sequence_length, io) < 0)
+   {
+      return -1;
+   }
+
+   /*@ assert (((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX); @*/
+   if
+   (
+      /* Appears to make Frama-C forget everything about *sequence_length. */
+      ZoO_sequence_ensure_capacity
+      (
+         sequence,
+         sequence_capacity,
+         *sequence_length,
+         io
+      ) < 0
+   )
+   {
+      return -2;
+   }
+   /*@ assert *sequence_length >= 0; @*/
+
+   if (*sequence_length > 1)
+   {
+      /*@ assert(((*sequence_length) * sizeof(ZoO_index)) <= SIZE_MAX); @*/
+
+      memmove
+      (
+         (void *) (*sequence + 1),
+         (const void *) sequence,
+         (((*sequence_length) - 1) * sizeof(ZoO_index))
+      );
+   }
+
+   (*sequence)[0] = word_id;
+
+   return 0;
+}
+
+int ZoO_sequence_append_right
+(
+   ZoO_index * sequence [const restrict static 1],
+   const ZoO_index word_id,
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   if (increment_required_capacity(sequence_length, io) < 0)
+   {
+      return -1;
+   }
+
+   /*@ assert ((*sequence_length * sizeof(ZoO_index)) < SIZE_MAX); @*/
+   if
+   (
+      ZoO_sequence_ensure_capacity
+      (
+         sequence,
+         sequence_capacity,
+         *sequence_length,
+         io
+      ) < 0
+   )
+   {
+      return -1;
+   }
+
+   /* assert (*sequence_length >= 1) */
+   (*sequence)[*sequence_length - 1] = word_id;
+
+   return 0;
+}
diff --git a/src/core/sequence_creation.c b/src/sequence/sequence_creation.c
index c5ca6af..e8ae2a1 100644
--- a/src/core/sequence_creation.c
+++ b/src/sequence/sequence_creation.c
@@ -52,72 +52,6 @@ static ZoO_index weighted_random_pick
 /******************************************************************************/
 
 /*
- * Adds an id to the left of the sequence.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {*sequence} remains untouched.
- * Returns:
- *    0 on success.
- *    -1 iff adding the word would cause an overflow.
- *    -2 iff memory allocation was unsuccessful.
- * Post:
- *    (initialized {sequence})
- *    (initialized {*sequence})
- */
-static int left_append
-(
-   const ZoO_index word_id,
-   ZoO_index * sequence [const restrict],
-   const size_t sequence_size,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   if ((SIZE_MAX - sizeof(ZoO_index)) > sequence_size)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Left side append aborted, as the new sequence's size would overflow."
-      );
-
-      return -1;
-   }
-
-   new_sequence = (ZoO_index *) malloc(sizeof(ZoO_index) + sequence_size);
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Left side append aborted, as memory for the new sequence could not be"
-         " allocated."
-      );
-
-      return -2;
-   }
-
-   if (sequence_size > 0)
-   {
-      memcpy
-      (
-         (void *) (new_sequence + 1),
-         (const void *) sequence,
-         sequence_size
-      );
-
-      free((void *) sequence);
-   }
-
-   new_sequence[0] = word_id;
-
-   *sequence = new_sequence;
-
-   return 0;
-}
-
-/*
  * Adds an id to the left of the sequence, according to what is known as likely
  * to fit there.
  * This requires the reallocation of {sequence}. The freeing of the previous
@@ -137,9 +71,10 @@ static int left_append
 static int extend_left
 (
    ZoO_index * sequence [const restrict static 1],
-   const size_t sequence_size,
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
    const ZoO_index markov_order,
-   const struct ZoO_knowledge k [const restrict static 1],
+   struct ZoO_knowledge k [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
@@ -172,7 +107,7 @@ static int extend_left
 
    if
    (
-      left_append
+      ZoO_sequence_append_left
       (
          weighted_random_pick
          (
@@ -180,7 +115,8 @@ static int extend_left
             preceding_words_weights_sum
          ),
          sequence,
-         sequence_size,
+         sequence_capacity,
+         sequence_length,
          io
       ) < 0
    )
@@ -220,18 +156,30 @@ static int extend_left
 static int complete_left_part_of_sequence
 (
    ZoO_index * sequence [restrict static 1],
-   size_t sequence_size [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
    const ZoO_index markov_order,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
+   size_t credits [const restrict],
+   struct ZoO_knowledge k [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
    for (;;)
    {
-      if ((credits == (ZoO_index *) NULL) || (*credits > 0))
+      if ((credits == (size_t *) NULL) || (*credits > 0))
       {
-         if (extend_left(sequence, *sequence_size, markov_order, k, io) < 0)
+         if
+         (
+            extend_left
+            (
+               sequence,
+               sequence_capacity,
+               sequence_length,
+               markov_order,
+               k,
+               io
+            ) < 0
+         )
          {
             /* We are sure *sequence[0] is defined. */
             if (*sequence[0] == ZoO_START_OF_SEQUENCE_ID)
@@ -256,13 +204,7 @@ static int complete_left_part_of_sequence
          return 0;
       }
 
-      /*
-       * Safe: if it was going to overflow, extend_left would have returned a
-       * negative value, making this statement unreachable.
-       */
-      *sequence_size = (*sequence_size + sizeof(ZoO_index));
-
-      if (credits != (ZoO_index *) NULL)
+      if (credits != (size_t *) NULL)
       {
          *credits -= 1;
       }
@@ -293,65 +235,6 @@ static int complete_left_part_of_sequence
 /** ADDING ELEMENTS TO THE RIGHT **********************************************/
 /******************************************************************************/
 
-/*
- * Adds an id to the right of the sequence.
- * This requires the reallocation of {sequence}. The freeing of the previous
- * memory space is handled. If an error happened, {sequence} remain untouched.
- * Returns:
- *    0 on success.
- *    -1 iff adding the word would cause an overflow.
- *    -2 iff memory allocation was unsuccessful.
- * Post:
- *    (initialized {sequence})
- *    (initialized {*sequence})
- */
-static int right_append
-(
-   ZoO_index * sequence [const restrict],
-   const ZoO_index word_id,
-   const size_t sequence_size,
-   const ZoO_index sequence_length,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   ZoO_index * new_sequence;
-
-   if ((SIZE_MAX - sizeof(ZoO_index)) > sequence_size)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Right side append aborted, as the new sequence's size would overflow."
-      );
-
-      return -1;
-   }
-
-   new_sequence =
-      (ZoO_index *) realloc
-      (
-         sequence,
-         (sequence_size + sizeof(ZoO_index))
-      );
-
-   if (new_sequence == (ZoO_index *) NULL)
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Right side append aborted, as memory for the new sequence could not "
-         "be allocated."
-      );
-
-      return -2;
-   }
-
-   new_sequence[sequence_length] = word_id;
-
-   *sequence = new_sequence;
-
-   return 0;
-}
 
 /*
  * Adds an id to the right of the sequence, according to what is known as likely
@@ -373,10 +256,10 @@ static int right_append
 static int extend_right
 (
    ZoO_index * sequence [const restrict static 1],
-   const size_t sequence_size,
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
    const ZoO_index markov_order,
-   const ZoO_index sequence_length,
-   const struct ZoO_knowledge k [const restrict static 1],
+   struct ZoO_knowledge k [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
@@ -393,11 +276,12 @@ static int extend_right
       (
          k,
          *sequence,
-         sequence_length,
+         *sequence_length,
          markov_order,
          &following_words,
          &following_words_weights,
-         &following_words_weights_sum
+         &following_words_weights_sum,
+         io
       ) < 0
    )
    {
@@ -410,7 +294,7 @@ static int extend_right
 
    if
    (
-      right_append
+      ZoO_sequence_append_right
       (
          sequence,
          weighted_random_pick
@@ -418,7 +302,7 @@ static int extend_right
             following_words_weights,
             following_words_weights_sum
          ),
-         sequence_size,
+         sequence_capacity,
          sequence_length,
          io
       ) < 0
@@ -459,36 +343,33 @@ static int extend_right
 static int complete_right_part_of_sequence
 (
    ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
    const ZoO_index markov_order,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
+   size_t credits [const restrict],
+   struct ZoO_knowledge k [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
-   ZoO_index sequence_length;
-
-   sequence_length = (*sequence_size / sizeof(ZoO_index));
-
    for (;;)
    {
-      if ((credits == (ZoO_index *) NULL) || (*credits > 0))
+      if ((credits == (size_t *) NULL) || (*credits > 0))
       {
          if
          (
             extend_right
             (
                sequence,
-               *sequence_size,
-               markov_order,
+               sequence_capacity,
                sequence_length,
+               markov_order,
                k,
                io
             ) < 0
          )
          {
             /* Safe: (> sequence_length 1) */
-            if (*sequence[(sequence_length - 1)] == ZoO_END_OF_SEQUENCE_ID)
+            if (*sequence[(*sequence_length - 1)] == ZoO_END_OF_SEQUENCE_ID)
             {
                /*
                 * We failed to add a word, but it was because none should have
@@ -505,25 +386,18 @@ static int complete_right_part_of_sequence
       else
       {
          /* No more credits available, we end the sequence. */
-         *sequence[(sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
+         *sequence[(*sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
 
          return 0;
       }
 
-      /*
-       * Safe: if it was going to overflow, extend_left would have returned a
-       * negative value, making this statement unreachable.
-       */
-      *sequence_size = (*sequence_size + sizeof(ZoO_index));
-      sequence_length += 1;
-
-      if (credits != (ZoO_index *) NULL)
+      if (credits != (size_t *) NULL)
       {
          *credits -= 1;
       }
 
       /* Safe: (> sequence_length 1) */
-      switch (*sequence[(sequence_length - 1)])
+      switch (*sequence[(*sequence_length - 1)])
       {
          case ZoO_START_OF_SEQUENCE_ID:
             ZoO_S_WARNING
@@ -532,7 +406,7 @@ static int complete_right_part_of_sequence
                "END OF LINE was added at the right part of an sequence."
             );
 
-            *sequence[(sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
+            *sequence[(*sequence_length - 1)] = ZoO_END_OF_SEQUENCE_ID;
             return 0;
 
          case ZoO_END_OF_SEQUENCE_ID:
@@ -549,58 +423,6 @@ static int complete_right_part_of_sequence
 /******************************************************************************/
 
 /*
- * Allocates the memory required to store the initial sequence.
- * Returns:
- *    0 on success.
- *    -1 if this would require more memory than can indicate a size_t variable.
- *    -2 if the allocation failed.
- * Post:
- *    (initialized {*sequence})
- *    (initialized {*sequence_size})
- */
-static int allocate_initial_sequence
-(
-   ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
-   const ZoO_index markov_order,
-   const struct ZoO_pipe io [const restrict static 1]
-)
-{
-   if ((SIZE_MAX / sizeof(ZoO_index)) > ((size_t) markov_order))
-   {
-      ZoO_S_ERROR
-      (
-         io,
-         "Unable to store size of the initial sequence in a size_t variable."
-         "Either reduce the size of a ZoO_index or the markovian order."
-      );
-
-      *sequence = (ZoO_index *) NULL;
-      *sequence_size = 0;
-
-      return -1;
-   }
-
-   *sequence_size = (((size_t) markov_order) * sizeof(ZoO_index));
-   *sequence = (ZoO_index *) malloc(*sequence_size);
-
-   if (*sequence == (void *) NULL)
-   {
-      *sequence_size = 0;
-
-      ZoO_S_ERROR
-      (
-         io,
-         "Unable to allocate the memory required for an new sequence."
-      );
-
-      return -2;
-   }
-
-   return 0;
-}
-
-/*
  * Initializes an pre-allocated sequence by filling it with {initial_word}
  * followed by a sequence of ({markov_order} - 1) words that is known to have
  * followed {initial_word} at least once. This sequence is chosen depending on
@@ -621,7 +443,7 @@ static int initialize_sequence
    ZoO_index sequence [const restrict static 1],
    const ZoO_index initial_word,
    const ZoO_index markov_order,
-   const struct ZoO_knowledge k [const static 1],
+   struct ZoO_knowledge k [const static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
@@ -637,7 +459,6 @@ static int initialize_sequence
       return 0;
    }
 
-   /* TODO */
    (void) ZoO_knowledge_lock_access(k, io);
 
    if
@@ -701,33 +522,57 @@ static int initialize_sequence
 int ZoO_sequence_create_from
 (
    const ZoO_index initial_word,
-   ZoO_index credits [const restrict],
-   const struct ZoO_knowledge k [const restrict static 1],
+   size_t credits [const restrict],
+   struct ZoO_knowledge k [const restrict static 1],
    const ZoO_index markov_order,
    ZoO_index * sequence [const restrict static 1],
-   size_t sequence_size [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
    const struct ZoO_pipe io [const restrict static 1]
 )
 {
-   if (allocate_initial_sequence(sequence, sequence_size, markov_order, io) < 0)
+   if
+   (
+      ZoO_sequence_ensure_capacity
+      (
+         sequence,
+         sequence_capacity,
+         markov_order,
+         io
+      ) < 0
+   )
    {
+      *sequence_length = 0;
+
       return -1;
    }
 
-   if (initialize_sequence(*sequence, initial_word, markov_order, k, io) < 0)
+   if
+   (
+      initialize_sequence
+      (
+         *sequence,
+         initial_word,
+         markov_order,
+         k,
+         io
+      ) < 0
+   )
    {
-      free((void *) *sequence);
-      *sequence_size = 0;
+      *sequence_length = 0;
 
       return -2;
    }
 
+   *sequence_length = markov_order;
+
    if
    (
       complete_right_part_of_sequence
       (
          sequence,
-         sequence_size,
+         sequence_capacity,
+         sequence_length,
          markov_order,
          credits,
          k,
@@ -735,8 +580,7 @@ int ZoO_sequence_create_from
       ) < 0
    )
    {
-      free((void *) *sequence);
-      *sequence_size = 0;
+      *sequence_length = 0;
 
       return -3;
    }
@@ -746,7 +590,8 @@ int ZoO_sequence_create_from
       complete_left_part_of_sequence
       (
          sequence,
-         sequence_size,
+         sequence_capacity,
+         sequence_length,
          markov_order,
          credits,
          k,
@@ -754,19 +599,17 @@ int ZoO_sequence_create_from
       ) < 0
    )
    {
-      free((void *) *sequence);
-      *sequence_size = 0;
+      *sequence_length = 0;
 
       return -4;
    }
 
-   if ((*sequence_size / sizeof(ZoO_index)) < 3)
+   if (*sequence_length < 3)
    {
       /* 2 elements, for start and stop. */
       ZoO_S_ERROR(io, "Created sequence was empty.");
 
-      free((void *) *sequence);
-      *sequence_size = 0;
+      *sequence_length = 0;
 
       return -5;
    }
diff --git a/src/sequence/sequence_from_string.c b/src/sequence/sequence_from_string.c
new file mode 100644
index 0000000..cd04d70
--- /dev/null
+++ b/src/sequence/sequence_from_string.c
@@ -0,0 +1,214 @@
+#define _POSIX_C_SOURCE 200809L
+#include <stdlib.h>
+#include <string.h>
+#include <stdint.h> /* defines SIZE_MAX */
+
+#include "../core/char.h"
+#include "../core/index.h"
+
+#include "../pipe/pipe.h"
+
+#include "../knowledge/knowledge.h"
+
+#include "sequence.h"
+
+/******************************************************************************/
+/** HANDLING WORDS ************************************************************/
+/******************************************************************************/
+
+/*
+ * Semaphore:
+ *    Takes then releases access for {k}.
+ */
+static int add_word_to_sequence
+(
+   const ZoO_char string [const restrict static 1],
+   const size_t word_start,
+   const size_t word_length,
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   struct ZoO_knowledge k [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   ZoO_index word_id;
+   ZoO_char * stored_word;
+
+   if (word_length == 0)
+   {
+      return 0;
+   }
+
+   (void) ZoO_knowledge_lock_access(k, io);
+
+   if
+   (
+      ZoO_knowledge_learn_word
+      (
+         k,
+         (string + word_start),
+         word_length,
+         &word_id,
+         io
+      ) < 0
+   )
+   {
+      (void) ZoO_knowledge_unlock_access(k, io);
+
+      return -1;
+   }
+
+   (void) ZoO_knowledge_unlock_access(k, io);
+
+   if
+   (
+      ZoO_sequence_append_right
+      (
+         sequence,
+         word_id,
+         sequence_capacity,
+         sequence_length,
+         io
+      ) < 0
+   )
+   {
+      return -1;
+   }
+
+   return 0;
+}
+
+static int find_word
+(
+   const ZoO_char string [const restrict static 1],
+   const size_t string_length,
+   const size_t offset,
+   size_t word_start [const restrict static 1],
+   size_t word_length [const restrict static 1]
+)
+{
+   size_t i;
+
+   i = offset;
+
+   while ((string[i] == ' ') && (i < string_length))
+   {
+      i += 1;
+   }
+
+   if (i >= string_length)
+   {
+      return -1;
+   }
+
+   *word_start = i;
+
+   while ((string[i] != ' ') && (i < string_length))
+   {
+      i += 1;
+   }
+
+   if (i >= string_length)
+   {
+      return -1;
+   }
+
+   *word_length = (i - *word_start);
+
+   return 0;
+}
+
+/******************************************************************************/
+/** EXPORTED ******************************************************************/
+/******************************************************************************/
+
+/* See: "sequence.h" */
+int ZoO_sequence_from_undercase_string
+(
+   const ZoO_char string [const restrict],
+   const size_t string_length,
+   struct ZoO_knowledge k [const restrict static 1],
+   ZoO_index * sequence [const restrict static 1],
+   size_t sequence_capacity [const restrict static 1],
+   size_t sequence_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   size_t word_start, word_length;
+   size_t i;
+
+   i = 0;
+
+   *sequence = (ZoO_index *) NULL;
+   *sequence_length = 0;
+
+   if
+   (
+      ZoO_sequence_append_right
+      (
+         sequence,
+         ZoO_START_OF_SEQUENCE_ID,
+         sequence_capacity,
+         sequence_length,
+         io
+      ) < 0
+   )
+   {
+      return -1;
+   }
+
+   while (i < string_length)
+   {
+      if (find_word(string, i, string_length, &word_start, &word_length) < 0)
+      {
+         break;
+      }
+
+      if
+      (
+         add_word_to_sequence
+         (
+            string,
+            word_start,
+            word_length,
+            sequence,
+            sequence_capacity,
+            sequence_length,
+            k,
+            io
+         ) < 0
+      )
+      {
+         free((void *) *sequence);
+         *sequence = (ZoO_index *) NULL;
+         *sequence_length = 0;
+
+         return -1;
+      }
+
+      i = (word_start + word_length);
+   }
+
+   if
+   (
+      ZoO_sequence_append_right
+      (
+         sequence,
+         ZoO_END_OF_SEQUENCE_ID,
+         sequence_capacity,
+         sequence_length,
+         io
+      ) < 0
+   )
+   {
+      free((void *) *sequence);
+
+      *sequence = (ZoO_index *) NULL;
+      *sequence_length = 0;
+
+      return -1;
+   }
+
+   return 0;
+}
diff --git a/src/sequence/sequence_to_string.c b/src/sequence/sequence_to_string.c
new file mode 100644
index 0000000..cec3af8
--- /dev/null
+++ b/src/sequence/sequence_to_string.c
@@ -0,0 +1,189 @@
+#define _POSIX_C_SOURCE 200809L
+#include <stdlib.h>
+#include <string.h>
+#include <stdint.h> /* defines SIZE_MAX */
+
+#include "../core/char.h"
+#include "../core/index.h"
+
+#include "../pipe/pipe.h"
+
+#include "../knowledge/knowledge.h"
+
+#include "sequence.h"
+
+/******************************************************************************/
+/** MEMORY ALLOCATION *********************************************************/
+/******************************************************************************/
+static int ensure_string_capacity
+(
+   ZoO_char * string [const restrict static 1],
+   size_t string_capacity [const restrict static 1],
+   const size_t string_required_capacity,
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   ZoO_char * new_string;
+
+   if (string_required_capacity <= *string_capacity)
+   {
+      return 0;
+   }
+
+   new_string =
+      (ZoO_char *) realloc
+      (
+         (void *) *string,
+         ((size_t) string_required_capacity) * sizeof(ZoO_char)
+      );
+
+   if (new_string== (ZoO_char *) NULL)
+   {
+      ZoO_S_ERROR
+      (
+         io,
+         "Unable to reallocate memory to match string's required size."
+      );
+
+      return -1;
+   }
+
+   *string_capacity = string_required_capacity;
+   *string = new_string;
+
+   return 1;
+}
+
+/******************************************************************************/
+/** ADD WORD ******************************************************************/
+/******************************************************************************/
+static int increment_required_capacity
+(
+   size_t current_capacity [const restrict static 1],
+   const size_t increase_factor,
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   if ((ZoO_INDEX_MAX - increase_factor) > *current_capacity)
+   {
+      ZoO_S_ERROR
+      (
+         io,
+         "String capacity increment aborted, as the new capacity would not"
+         " fit in a ZoO_index variable."
+      );
+
+      return -1;
+   }
+
+   *current_capacity += increase_factor;
+
+   if ((SIZE_MAX / sizeof(ZoO_char)) > *current_capacity)
+   {
+      *current_capacity -= increase_factor;
+
+      ZoO_S_ERROR
+      (
+         io,
+         "String capacity increment aborted, as the new size would not fit"
+         " in a size_t variable."
+      );
+
+      return -2;
+   }
+
+   return 0;
+}
+
+static int add_word
+(
+   const ZoO_index word_id,
+   struct ZoO_knowledge k [const restrict static 1],
+   ZoO_char * destination [const restrict static 1],
+   size_t destination_capacity [const restrict static 1],
+   size_t destination_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+	const ZoO_char * word;
+	ZoO_index word_size;
+   size_t insertion_point;
+
+	(void) ZoO_knowledge_lock_access(k, io);
+	ZoO_knowledge_get_word(k, word_id, &word, &word_size, io);
+	(void) ZoO_knowledge_unlock_access(k, io);
+
+   insertion_point = *destination_length;
+
+   /* word_size includes '\n', which will be replaced by a space. */
+   /* (word_size == ZoO_INDEX_MAX) ==> could not have learned word. */
+   if (increment_required_capacity(destination_length, (word_size + 1), io) < 0)
+   {
+      return -1;
+   }
+
+   if
+   (
+      ensure_string_capacity
+      (
+         destination,
+         destination_capacity,
+         *destination_length,
+         io
+      ) < 0
+   )
+   {
+      return -2;
+   }
+
+   memcpy
+   (
+      (*destination + insertion_point),
+      (const void *) word,
+      word_size
+   );
+
+   (*destination)[*destination_length - 1] = ' ';
+
+   return 0;
+}
+
+/******************************************************************************/
+/** EXPORTED ******************************************************************/
+/******************************************************************************/
+int ZoO_sequence_to_undercase_string
+(
+   const ZoO_index sequence [const restrict static 1],
+   const size_t sequence_length,
+   ZoO_char * destination [const restrict static 1],
+   struct ZoO_knowledge k [const restrict static 1],
+   size_t destination_capacity [const restrict static 1],
+   size_t destination_length [const restrict static 1],
+   const struct ZoO_pipe io [const restrict static 1]
+)
+{
+   size_t i;
+
+   for (i = 0; i < sequence_length; ++i)
+   {
+      if
+      (
+         add_word
+         (
+            sequence[i],
+            k,
+            destination,
+            destination_capacity,
+            destination_length,
+            io
+         ) < 0
+      )
+      {
+         *destination_length = 0;
+
+         return -1;
+      }
+   }
+
+   return 0;
+}
diff --git a/src/core/sequence_types.h b/src/sequence/sequence_types.h
index c260a8a..717d418 100644
--- a/src/core/sequence_types.h
+++ b/src/sequence/sequence_types.h
@@ -3,8 +3,7 @@
 
 #define ZoO_START_OF_SEQUENCE_ID 0
 #define ZoO_END_OF_SEQUENCE_ID   1
-#define ZoO_ACTION_SEQUENCE_ID   2
 
-#define ZoO_RESERVED_IDS_COUNT   3
+#define ZoO_RESERVED_IDS_COUNT   2
 
 #endif
diff --git a/src/server/CMakeLists.txt b/src/server/CMakeLists.txt
new file mode 100644
index 0000000..2d1beaa
--- /dev/null
+++ b/src/server/CMakeLists.txt
@@ -0,0 +1,8 @@
+set(
+   SRC_FILES ${SRC_FILES}
+   ${CMAKE_CURRENT_SOURCE_DIR}/server.c
+   ${CMAKE_CURRENT_SOURCE_DIR}/server_worker.c
+)
+
+set(SRC_FILES ${SRC_FILES} PARENT_SCOPE)
+
diff --git a/src/server/server.c b/src/server/server.c
index 3ded7cc..8a75615 100644
--- a/src/server/server.c
+++ b/src/server/server.c
@@ -1,6 +1,7 @@
 #include <signal.h>
+#include <stdio.h>
 
-#include "../cli/parameters.h"
+#include "../parameters/parameters.h"
 
 #include "server.h"
 
@@ -18,6 +19,7 @@ int ZoO_server_main (const struct ZoO_parameters params)
 {
    struct ZoO_server server;
    struct ZoO_server_message msg_buffer;
+   struct ZoO_server_worker_parameters worker_params;
 
    if
    (
@@ -31,6 +33,14 @@ int ZoO_server_main (const struct ZoO_parameters params)
       return -1;
    }
 
+   ZoO_server_worker_initialize_parameters
+   (
+      &worker_params,
+      &server,
+      &msg_buffer,
+      &params
+   );
+
    while ((ZoO_SERVER_IS_RUNNING == (char) 1) || (server.running_threads > 0))
    {
       if (ZoO_server_receive_message(&server, &msg_buffer) < 0)
@@ -42,13 +52,21 @@ int ZoO_server_main (const struct ZoO_parameters params)
 
       switch (msg_buffer.type)
       {
-         case 'C':
-            ZoO_server_new_client(&server, &msg_buffer);
+         case 'C': /* Client request */
+            ZoO_server_add_worker(&server, &worker_params);
+            break;
 
-         case 'J':
-            ZoO_server_join_thread(&server, &msg_buffer);
+         case 'J': /* Join request */
+            ZoO_server_finalize_worker(&server, &msg_buffer);
+            break;
 
          default:
+            fprintf
+            (
+               stderr,
+               "[W] Received message with unknown type '%c'.\n",
+               msg_buffer.type
+            );
             break;
       }
    }
diff --git a/src/server/server.h b/src/server/server.h
index a75c6e7..f6aa0de 100644
--- a/src/server/server.h
+++ b/src/server/server.h
@@ -1,7 +1,7 @@
 #ifndef _ZoO_SERVER_SERVER_H_
 #define _ZoO_SERVER_SERVER_H_
 
-#include "../cli/parameters_types.h"
+#include "../parameters/parameters_types.h"
 
 #include "server_types.h"
 
@@ -24,13 +24,14 @@ int ZoO_server_receive_message
    struct ZoO_server_message msg_buffer [const restrict static 1]
 );
 
-int ZoO_server_new_client
+int ZoO_server_add_worker
 (
-   struct ZoO_server [const restrict static 1],
-   struct ZoO_server_message msg_buffer [const restrict static 1]
+   struct ZoO_server s [const restrict static 1],
+   struct ZoO_server_message msg_buffer [const restrict static 1],
+   struct ZoO_worker_parameters worker_params [const restrict static 1]
 );
 
-int ZoO_server_join_thread
+int ZoO_server_finalize_worker
 (
    struct ZoO_server [const restrict static 1],
    struct ZoO_server_message msg_buffer [const restrict static 1]
diff --git a/src/server/server_add_server_worker.c b/src/server/server_add_server_worker.c
new file mode 100644
index 0000000..cae10fd
--- /dev/null
+++ b/src/server/server_add_server_worker.c
@@ -0,0 +1,13 @@
+#include <pthread.h>
+
+#include "server.h"
+
+int ZoO_server_add_worker
+(
+   struct ZoO_server s [const restrict static 1],
+   struct ZoO_server_message msg_buffer [const restrict static 1]
+)
+{
+   /* TODO */
+   return -1;
+}
diff --git a/src/server/server_types.h b/src/server/server_types.h
index 75016d4..aeb0ec8 100644
--- a/src/server/server_types.h
+++ b/src/server/server_types.h
@@ -5,24 +5,21 @@
 
 #include "../core/index.h"
 
-struct ZoO_server_pipes_data
-{
-   char request_pipe[255];
-   char reply_pipe[255];
-};
+#include "../pipe/pipe_types.h"
 
 struct ZoO_server_message
 {
    char type;
    union
    {
-      struct ZoO_server_pipes_data pipes_name;
+      struct ZoO_pipe_names pipe_names;
       ZoO_index pthread_id;
    } data;
 };
 
 struct ZoO_server
 {
+   /* TODO: insert 2 thread barrier. */
    mqd_t mailbox;
    ZoO_index running_threads;
 };
diff --git a/src/server/server_worker.c b/src/server/server_worker.c
new file mode 100644
index 0000000..04f71ca
--- /dev/null
+++ b/src/server/server_worker.c
@@ -0,0 +1,21 @@
+#include "worker.h"
+
+void ZoO_worker_initialize_parameters
+(
+   struct ZoO_worker_parameters worker_params;
+   const struct ZoO_server_message msg_buffer [const restrict static 1],
+   const struct ZoO_parameters params [const restrict static 1]
+)
+{
+   worker_params->thread_id = 0;
+   pthread_barrier_t * barrier;
+   mqd_t * server_mailbox;
+   const struct ZoO_pipe_names * pipe_names;
+
+   /* Program data */
+   ZoO_index markov_order;
+   struct ZoO_knowledge * k;
+   const char * storage_filename;
+
+   /* TODO */
+}
diff --git a/src/server/server_worker.h b/src/server/server_worker.h
new file mode 100644
index 0000000..825cc11
--- /dev/null
+++ b/src/server/server_worker.h
@@ -0,0 +1,8 @@
+#ifndef _ZoO_WORKER_WORKER_H_
+#define _ZoO_WORKER_WORKER_H_
+
+#include "../parameters/parameters_types.h"
+
+#include "worker_types.h"
+
+#endif
diff --git a/src/server/server_worker_types.h b/src/server/server_worker_types.h
new file mode 100644
index 0000000..07757bd
--- /dev/null
+++ b/src/server/server_worker_types.h
@@ -0,0 +1,27 @@
+#ifndef _ZoO_WORKER_WORKER_TYPES_H_
+#define _ZoO_WORKER_WORKER_TYPES_H_
+
+#include <mqueue.h>
+
+#include "../core/index_types.h"
+
+#include "../pipes/pipes_types.h"
+
+#include "../knowledge/knowledge_types.h"
+
+
+struct ZoO_worker_parameters
+{
+   /* Communication data */
+   ZoO_index thread_id;
+   pthread_barrier_t * barrier;
+   mqd_t * server_mailbox;
+   const struct ZoO_pipe_names * pipe_names;
+
+   /* Program data */
+   ZoO_index markov_order;
+   struct ZoO_knowledge * k;
+   const char * storage_filename;
+};
+
+#endif