1
입력이 배열 인 것이 분명하지만, 플래그 [1 ..]이 진행될 때 플래그가 시퀀스라고 말하는 이유는 무엇입니까? http://rise4fun.com/Dafny/fUguDafny : 배열을 입력하는 이유 Dafny가 시퀀스라고 말합니다.
A
답변
1
배열 A과 정수 lo 및 hi 인덱스 lo 시작 A에서 hi-lo 요소의 시퀀스 (되지 배열)을 반환 A[lo..hi] 표현식 : 여기에 링크이다. 귀하의 프로그램에 대해서는 모든 기능을 시퀀스 나 (아마도 귀하의 프로그램에 대해) 더 잘 작동하도록하는 것이 좋습니다. lo 및 hi 매개 변수를 모든 기능에 추가하여 원하는 배열 부분을 윤곽으로 나타낼 수 있습니다.