Array Index Small EnoughCode template contract predicate to ensure an array indexing is small enough according to its upper boundEiffel Softwareasmall_enoughEiffelcodecontractinvariantpreconditionpostcondition
${index}_small_enough: ${index} <= ${array}.upper${end}