Trying out ACSL, continuing implementation.

1 files changed, 208 insertions, 0 deletions

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