1 files changed, 11 insertions, 0 deletions
diff --git a/src/core/index.h b/src/core/index.h
index 76e3507..1417662 100644
--- a/src/core/index.h
+++ b/src/core/index.h
@@ -3,6 +3,17 @@
 
 #include "index_types.h"
 
+/*
+ * Returns a random ZoO_index.
+ */
+ZoO_index ZoO_index_random (void);
+
+/*
+ * Returns a random ZoO_index, included in [0, limit]
+ */
+/*@
+ @ ensures (\result <= limit);
+ @*/
 ZoO_index ZoO_index_random_up_to (const ZoO_index limit);
 
 #endif