Initial Commit

1 files changed, 26 insertions, 0 deletions

diff --git a/src/core/index.h b/src/core/index.h
new file mode 100644
index 0000000..66b2540
--- /dev/null
+++ b/src/core/index.h
@@ -0,0 +1,26 @@
+#ifndef _JH_CORE_INDEX_H_
+#define _JH_CORE_INDEX_H_
+
+#include "index_types.h"
+
+/*
+ * Returns a random JH_index.
+ */
+/*@
+   ensures (\result <= JH_INDEX_MAX);
+   assigns \result;
+@*/
+JH_index JH_index_random (void);
+
+/*
+ * Returns a random JH_index, included in [0, limit]
+ */
+/*@
+   ensures (\result <= limit);
+   assigns \result;
+@*/
+JH_index JH_index_random_up_to (const JH_index limit);
+
+int JH_index_cmp (const JH_index a, const JH_index b);
+
+#endif