Initial Commit

1 files changed, 50 insertions, 0 deletions

diff --git a/src/sequence/sequence.c b/src/sequence/sequence.c
new file mode 100644
index 0000000..c9c30f1
--- /dev/null
+++ b/src/sequence/sequence.c
@@ -0,0 +1,50 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "../core/index.h"
+
+#include "sequence.h"
+
+/* 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 JH_sequence_cmp
+(
+   const JH_index sequence_a [const restrict static 1],
+   const JH_index sequence_b [const restrict static 1],
+   const JH_index length
+)
+{
+   JH_index i, a, b;
+
+   for (i = 0; i < length; ++i)
+   {
+      a = sequence_a[i];
+      b = sequence_b[i];
+
+      if (a < b)
+      {
+         return -1;
+      }
+      else if (a > b)
+      {
+         return 1;
+      }
+   }
+
+   return 0;
+}
+