Действительно ясно, что ввод представляет собой массив, но почему, когда он переходит к флагу [1..], он говорит, что флаг — это последовательность? Вот ссылка: http://rise4fun.com/Dafny/fUgu
Дафни: Почему я ввожу массив Дафни говорит, что это последовательность
Ответы (1)
Для массива A и целых чисел lo и hi выражение A[lo..hi] возвращает последовательность (не массив) из hi-lo элементов из A, начиная с индекса lo. Для вашей программы я бы рекомендовал либо заставить все ваши функции работать с последовательностями, либо (вероятно, лучше для вашей программы) добавить параметры lo и hi ко всем функциям, чтобы очертить интересующую вас часть массива.
person
Rustan Leino
schedule
22.05.2017
@Lilac Liu, привет, я тоже борюсь с последовательностями и массивами в Dafny. Вы случайно не нашли способ преобразовать seq в массив?
- person Amir-Mousavi; 22.05.2018
метод SeqToArray‹T›(s: seq‹T›) возвращает (a: массив‹T›) гарантирует свежесть(a) && a[..] == s { a := new T[|s|](i требует 0 ‹= i ‹ |s| =› s[i]); }
- person Rustan Leino; 24.05.2018
