I've always appreciated Ada's approach to arrays. You can create array types and specify both the type of the values and of the index. If zero based makes sense for your use, use that, if something else makes sense use that.
e.g.
type Index is range 1 .. 5;
type My_Int_Array is
array (Index) of My_Int;
It made life pretty nice when working in SPARK if you defined suitable range types for indexes. The proof steps were generally much easier and frequently automatically handled.
e.g.
It made life pretty nice when working in SPARK if you defined suitable range types for indexes. The proof steps were generally much easier and frequently automatically handled.