--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on June 2009 ---
>As a minor remark about \valid_range, I would like to add that I find it always a bit odd >that I have to specify >\valid_range(a, 0, n-1) >to express an array of length n. I would prefer "\valid_range(a, 0, n)" or even shorter "\valid_range(a, n)". >In other words, I think that right open ranges fit better to C. The same is true for \valid, you have to specify \valid(a+(0..n-1)). However, I prefer it this way. I believe it makes the range of indices more explicit. Spec# has a range operator (0:a.Length) = {k | 0 <= k < a.Length}. I find it a bit confusing that the first element is included in the range, but not the last. If however \valid_range is not part of ACSL every user can define it in a way he preferes. Regards, Boris