Дафни чек карта содержит значение

Question

У меня есть карта типа map<int,char> в dafny, и я хочу посмотреть, содержит ли она какое-либо значение.

Предполагая, что в dafny для этого еще нет синтаксиса, я начал создавать метод для него, но застрял. Мой код ниже:

method containsValue(m: map<int,char>, val: char) returns (b: bool) 
    ensures b <==> exists i :: i in m && m[i] == val;
  {
    var i := 0;
    while (i < m.Length) {
        if (m[i] == val) 
          { return true; }      
      }
        return false;
    }

Это не работает, потому что я не знаю, как найти размер карты, и могут быть и другие проблемы. пожалуйста помогите

Answer 1

Modern Dafny имеет встроенный синтаксис для этого, используя специальное поле .Values карт, которое возвращает набор значений на карте.Карты также имеют .Keys для возврата набора ключей.(К сожалению, .Keys и .Values на данный момент не документированы. Мы работаем над этим.)

Вы можете выразить свой метод в одной строке следующим образом

method containsValue(m: map<int,char>, val: char) returns (b: bool) 
    ensures b <==> exists i :: i in m && m[i] == val;
{
    return val in m.Values;
}

который Dafny автоматически проверяет, удовлетворяет ли его спецификация.

---

Вы также можете вручную выполнять итерации по элементам карты следующим образоми, следовательно, плохой стиль.(Особенно для этого метода, где однострочная версия намного понятнее.) Однако иногда она полезна в других контекстах, поэтому полезно знать технику.