Array Index Big EnoughCode template contract predicate to ensure an array indexing is big enough according to its lower boundEiffel Softwareabig_enoughEiffelcodecontractinvariantpreconditionpostcondition
${index}_big_enough: ${index} >= ${array}.lower${end}