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

У меня есть карта типа 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;
    }

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


dafny
person Jofbr    schedule 11.05.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Современный 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 автоматически проверяет на соответствие спецификации.

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

method containsValue(m: map<int,char>, val: char) returns (b: bool)
    ensures b <==> exists i :: i in m && m[i] == val;
{
    var m' := m;
    while m'.Keys != {}
        invariant m'.Keys <= m.Keys
        invariant forall k | k in m' :: m'[k] == m[k]
        invariant (exists i :: i in m && m[i] == val) ==> (exists i :: i in m' && m'[i] == val)
        decreases m'.Keys
    {
        var k :| k in m';
        if m'[k] == val {
            return true;
        }
        m' := map k' | k' in m' && k' != k :: m'[k'];
    }
    return false;
}

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

person James Wilcox    schedule 11.05.2018
comment
Эй, спасибо за ваш ответ. Приятно знать, что .Keys и .Values можно использовать. Знаете ли вы, есть ли способ сделать обратный поиск на карте? Так что-то вроде map.getValue(key) ? - person Jofbr; 12.05.2018
comment
Или я могу инвертировать map<int,char> в map<char,int> каким-то образом, используя понимание карты или что-то еще? Это позволит мне искать ключ по значению на исходной карте. - person Jofbr; 12.05.2018
comment
Привет, было бы лучше задать отдельный вопрос о выполнении обратного поиска. - person James Wilcox; 12.05.2018
comment
Конечно stackoverflow.com/questions/50302154/dafny-reverse-lookup-map - person Jofbr; 12.05.2018