Дафни копирует мультимножество данных в массив - PullRequest
Новая
       16

Дафни копирует мультимножество данных в массив

0 голосов
/ 05 января 2020

Я новичок в Дафни. Я пишу программу для FindMax. Пройдя этот урок , я могу написать проверенную программу для массивов. 

method FindMax(a: array<int>) returns (i: int)

  requires 0<a.Length
  ensures 0<= i < a.Length
  ensures  forall k :: 0 <= k < a.Length ==> a[k] <= a[i]
   // Annotate this method with pre- and postconditions
   // that ensure it behaves as described.
{
   // Fill in the body that calculates the INDEX of the maximum.

  i:=0;
   var index := 0;
   while index < a.Length
      invariant 0 <= index <= a.Length
      invariant 0 <= i < a.Length
      invariant forall k :: 0 <= k < index ==> a[k] <= a[i]

      {
      if a[index] > a[i] {
      i := index;
      }
      index := index + 1;
   }
}

Теперь я хочу написать аналогичную программу, когда данные находятся в форме Multiset. Так как функция .length не разрешена в мультимножестве, она выдает ошибку. Другой подход, который я подумал, - преобразовать мультимножественные данные в массивы -> применить операцию и выполнить обратное преобразование. Теперь я застрял в функции записи для преобразования данных множества в массивы. Я прочитал этот учебник , но все еще сталкиваюсь с трудностями из-за ограниченной документации и новизны в Дафни. Любая помощь или ссылка на ресурс будут высоко оценены.

1 Ответ

0 голосов
/ 05 января 2020

Для всех тех, кто может посетить этот ответ позже - все, что вам нужно сделать, это использовать | a | в месте a.length и тот же метод будет правильно работать для мультимножества

...