Блог

Последовательности в Dafny являются неизменяемым типом, поэтому с точки зрения проверки не имеет значения, как они представлены во время выполнения. Но, как известно функциональным программистам, нормально представлять списки на функциональном языке (под капотом, таким образом, чтобы программист не мог манипулировать) в виде связанных списков, так что получение хвоста списка занимает постоянное время (и не требует выделения памяти), и поэтому объединение списков перераспределяет ячейки левого аргумента, но просто использует ссылку на правый аргумент.

Записано ли что-нибудь о том, как последовательности должны быть представлены в реализациях Dafny? Опять же, это проблема только в том случае, если кто-то действительно хочет запускать программы Dafny.

Во всех текущих бэкендах Dafny последовательности (и массивы, если на то пошло) представлены массивом или векторным типом.

В общем, вы можете проверить исходные файлы среды выполнения, чтобы увидеть, как Dafny реализует что-либо «под капотом»: https://github.com/dafny-lang/dafny/tree/master/Source/DafnyRuntime

Между тем, если вы хотите использовать связанный список, вы можете создать свой собственный тип данных связанного списка:

 datatype List<V> = Cons(v: V, tail: List<V>) | Nil