Почему возникает эта проблема с набором текста?

Пытаюсь написать программу на Дафни, вот часть программы:

method GenerateAllIndexSubsets<T>(q: seq<T>) returns (res: set<set<nat>>)
    ensures res == AllIndexSubsets(q)
{
    if |q| == 0
        { 
        assert |q| == 0;// if's guard
        // ==>
        assert {} == AllIndexSubsets<nat>([]);
        assert q == [];
        assert {} == AllIndexSubsets(q);
        res := {};
        assert res == AllIndexSubsets(q); // postcondition
        }
    else
        { 
            assert |q| != 0; // !(if's guard)
            var res0 : set<set<nat>> := GenerateAllIndexSubsets<T>(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            res := res0;    
            assert res ==  AllIndexSubsets(q[1..]); //GenerateAllIndexSubsets postcondition with q[1..]
            var index : nat := q[0];
            var res1: set<set<nat>> := (set x | x in res0 :: x + {index});
            assert res1 == AllIndexSubsets(q) - AllIndexSubsets(q[1..]);
            assert res0 == AllIndexSubsets(q[1..]);
            assert res1 == AllIndexSubsets(q) - res0;
            // ==>
            assert res0 + res1 == AllIndexSubsets(q);
            res := res + res1;
            assert res == AllIndexSubsets(q); // postcondition
        }
    assert res == AllIndexSubsets(q); // postcondition
}

в строке var index : nat := q[0] я получаю следующую проблему:

тип не согласуется с типом элемента seq (получил int)

Почему я получаю это и как я могу исправить это сейчас и не получить это снова в будущем?


types dafny
person Snirka    schedule 25.02.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

q — это последовательность элементов типа T, поэтому q[0] имеет тип T. Но вы пытаетесь присвоить его переменной типа nat, что неверно.

(Причина, по которой в сообщении об ошибке Dafny упоминается int вместо nat, заключается в том, что nat определяется как подмножество int, поэтому, чтобы проверить, является ли что-то nat, Dafny сначала проверяет, является ли это int, что здесь не работает.)

person James Wilcox    schedule 26.02.2018
comment
Спасибо за комментарий, могу ли я присвоить переменной любого типа значение типа T? потому что, если я хочу работать с элементами в q, как я могу это сделать? - person Snirka; 26.02.2018
comment
Я не уверен, что понимаю, что вы имеете в виду, но вы могли бы сказать, например, var x : T := q[0]. Это делает то, что вы хотите? - person James Wilcox; 26.02.2018
comment
Да, я знаю, что могу это сделать, но если, например, я хочу умножить этот элемент, могу ли я это сделать? потому что я не знаю, что это тип (будь это «nat» или «int»), все, что я знаю, это тип T, так что какие действия я могу сделать с ним? - person Snirka; 26.02.2018
comment
Вы ничего не можете с этим сделать, но в этом и есть смысл. Что бы значило умножить его на что-то, если бы T был, например, каким-то произвольным определяемым пользователем классом? - person James Wilcox; 26.02.2018
comment
Так какова его основная цель? итерация (в данном случае, потому что у нас есть последовательность типа ‹T›)? - person Snirka; 26.02.2018
comment
T — это переменная типа, обозначающая произвольный тип. Переменные типа предназначены для поддержки повторного использования кода, а не для повторной реализации функции для каждого типа, в котором вы хотите ее использовать. Кроме того, на мой взгляд, вы хотели написать var index := 0, инициализируя index нулем. Ноль — это индекс, но q[0] — это не индекс, это элемент. - person James Wilcox; 26.02.2018
comment
Я только что понял, что вы, возможно, запутались в обозначении seq<T>. Это тип последовательностей Ts. Итак, это список, в котором каждый элемент имеет тип T. Вы можете получить доступ к различным элементам, используя нотацию индексации q[i] (если q является последовательностью). Здесь i — это индекс в списке. Индексы всегда имеют тип int. Чтобы подчеркнуть, T — это тип элементов, а не индексов. - person James Wilcox; 26.02.2018