사전 조건으로 배열을 반복하는 방법은 무엇입니까?

Question

전제 조건에서 배열을 반복하고 싶습니다. 하지만 전제 조건에서는 "보낸 사람"및 "건너 뛰기"구문을 사용할 수 없습니다.

전제 조건에서 배열을 반복 할 방법이 있습니까?

insert_last (s: STRING) 
require 
    new_is_longer_than_prevs: 
-- here I want to iterate through array "arr" and if length of s is longer than all other previously stored string values in array 
do 
    arr.force (s, arr.upper + 1) 
end 

Answer 1

버전이 다른 응답에 제시된 대부분의 경우 (이 일을 배열의 낮은 인덱스를 가정입니다)에서 작동합니다. 그러나, 전역 루프는 배열보다는 인덱스 범위에서 직접 사용할 수 있습니다

new_is_longer_than_prevs: 
    across arr as c all s.count > c.item.count end 

이 버전은 모든 낮은 인덱스 작동 및 실행시 약간 더 효율적입니다.

Answer 2

당신은 또는 '등의 ... 일부 ... 말 ...에서'전제 조건과 사후에 '등 ... 모든 ... 말 ... 통해'사용할 수 있습니다. '모든'버전은 모든 반복에 대해 조건이 참이면 유효하고 하나 이상의 반복에 대해 조건이 참이면 '일부'버전이 유효하게 사용됩니다. 당신은 당신의 코드에서이 같은 몇 가지 일을 사용할 수 있습니다

insert_last (s: STRING) 
    require 
     new_is_longer_than_prevs: 
      across arr.lower |..| arr.upper as la_index all s.count > arr[la_index.item].count end 
    do 
     arr.force (s, arr.upper + 1) 
    end