配列の境界検査
bounds check
https://en.wikipedia.org/wiki/Bounds_checking
Dependent Types in Pratical Programming
ref
TaPL.icon
p.5 の補足
ATS言語
や
Coq
はできるらしい