Как проверить, что этот элемент последовательности равен этому элементу последовательности в Dafny
У меня есть 2 последовательности a:seq и b:seq, интересно, если мы используем функцию, как мы можем определить, что элемент с этим индексом в seq a равен элементу с этим индексом в seq b
function test(s:seq<nat>, u:seq<nat>): nat
ensures |s|>0
ensures |u|>0
ensures |s| == |u|
{
// Code
}
method Testing()
{
var sys:seq<nat> := [4,2,9,3,1];
var usr:seq<nat> := [1,2,3,4,5];
assert test(sys, usr) == 1
// The element at the index 2 of sys and usr are equal, so it have 1 element that match in both 2 sequence
}
Из-за функции я не мог создать цикл while, поэтому я не могу выполнить базовую логику, поэтому мне интересно, есть ли что-то, что соответствует требованию.
Ответы 2
После исследования и работы с Python, чтобы найти рекурсию в Python, я, наконец, нашел ответ на этот вопрос:
function bullspec(s:seq<nat>, u:seq<nat>): nat
requires |s| > 0
requires |u| > 0
requires |s| == |u|
{
var index:=0;
if |s| == 1 then (
if s[0]==u[0]
then 1 else 0
) else (
if s[index] != u[index]
then bullspec(s[index+1..],u[index+1..])
else 1+bullspec(s[index+1..],u[index+1..])
)
}
Этот ответ неверен, к сожалению. быкСпец([2],[2]) возвращает 1
Я думал, что это соответствует функции, что s=[2] и u=[2], она точно вернет 1, потому что s[i] = u[i]
О, так ваша формулировка проблемы заключалась в том, что вы искали, есть ли у двух последовательностей общий элемент с одним и тем же индексом? Почему вы не возвращаете логическое значение, если это так?
Извините за нечеткие требования, мне нужно подсчитать, сколько элементов равно как значению, так и одному и тому же индексу... но эта рекурсия может заставить меня усердно работать с инвариантом большего размера, поэтому я изменю его, но спасибо за ваше предложения <3
О, хорошо, я совершенно неправильно понял. Сама функция является спецификацией.
Это замечательная проблема, которую можно решить с Дафни. Позвольте мне четко сформулировать проблему:
Даны две последовательности одинаковой длины, найти первый индекс, при котором эти последовательности равны. В противном случае вернуть длину последовательностей.
Эта формулировка позволяет не требовать, чтобы последовательности были непустыми. Таким образом, мы можем начать со следующего определения
function bullspec(s:seq<nat>, u:seq<nat>): (r: nat)
requires |s| == |u|
// Ensures r is either a sequence index or the sequence length
ensures r <= |s|
// All the elements before r are different
ensures forall i: nat | i < r :: s[i] != u[i]
// Either r is the sequence length or the elements at index r are equal
ensures r == |s| || s[r] == u[r]
{
Теперь, если вам удастся доказать эту функцию, вам придется доказать, что эта функция делает то, что вы хотите. Чтобы получить тело функции, обычно нужно проверить, пуста ли последовательность. В нашем случае мы можем вернуть 0 — длину последовательности.
if |s| == 0 then 0 else
Если последовательность не пуста, то мы можем сравнить первые элементы. Если они равны, то возвращаем индекс 0
if s[0] == u[0] then 0 else
В противном случае, что произойдет, если мы вернемся к bullspec(s[1..],u[1..])? Мы получим индекс со смещением на 1! Так что нам нужно только добавить 1 к нему.
1 + bullspec(s[1..],u[1..])
}
Таким образом, вы можете убедиться, что ваша функция делает именно то, что вы хотели.
Как вы видели, я экспериментировал с вашим решением и обнаружил сбой в VSCode. Большое спасибо за предложение!