//@ requires n >= 0 && \valid_range(t,0,n−1);