Это код для игры Bulls and Cows, просто у нас есть 2 массива a[] и b[] одинаковой длины, если a[i] == b[i], то Bulls += 1, если a[i ] в b && a[i] != b[i] тогда Cows += 1.
Я написал функцию Bulls and Cows, но метод BullCows имеет некоторые проблемы при ее вычислении, из-за чего мое утверждение не выполняется.
`
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..])
)
}
function cowspec(s:seq<nat>, u:seq<nat>): nat
requires |s| > 0
requires |u| > 0
requires |s| <= |u|
{
var extra:= |u|-|s|;
var index:=0;
if |s| == 1 then (
if s[0] in u
then 1 else 0
) else(
if s[index] in u && s[index]!=u[extra]
then (1+ cowspec(s[index+1..],u))
else cowspec(s[index+1..],u)
)
}
method BullsCows (s:seq<nat>, u:seq<nat>) returns (b:nat, c:nat)
requires |s|>0 && |u|>0 &&|s|==|u|
// No duplicates in array
requires forall i, j | 0 <= i < |s| && 0 <= j < |s| && i != j :: s[i] != s[j]
requires forall i, j | 0 <= i < |u| && 0 <= j < |u| && i != j :: u[i] != u[j]
ensures forall k :: 0 <= k < |s| && s[k] !in u ==> b == c == 0
ensures forall k :: 0 <= k < |s| && s[k] in u ==> (c + b) > 0
{
var index := 0;
b := 0;
c := 0;
while(index<|s|)
invariant index <= |s|
invariant forall k :: 0 <= k < index && s[k] in u ==> (b + c) > 0
{
if s[index] in u {
if s[index] == u[index]{
b:=b+1;
} else {
c:=c+1;
}
}
index:=index + 1;
}
}
method NotMain()
{
var sys:seq<nat> := [4,2,9,3,1];
var usr:seq<nat> := [1,2,3,4,5];
assert bullspec(sys, usr) == 1; //True
assert cowspec(sys, usr) == 3; //True
var b:nat, c:nat := BullsCows(sys, usr);
assert b == 1; //Not true
assert c == 3; //Not true
}
` Метод NotMain говорит, что assert b == 1; и утверждать c==3; неправда, это язык Дафни, пожалуйста, помогите мне с этой логикой, я ломаю голову.
Я пытаюсь поставить много гарантий в методе BullsCows, но ничего не происходит.
Проблема в том, что постусловие на BullsCows()
недостаточно сильное, чтобы доказать последние два утверждения. В частности, нет никакой связи между работой BullsCows()
и спецификациями bullspec()
и cowspec()
. Вам нужно соединить эти вещи вместе.
Для иллюстрации я собираюсь использовать более простой пример, которому легче следовать. Что касается вашего примера выше, последнее утверждение не выполняется в следующем:
function sumspec(xs: seq<nat>, i: nat) : nat
requires i <= |xs| {
if |xs| == 0 || i == 0 then 0
else sumspec(xs,i-1) + xs[i-1]
}
method sum(s:seq<nat>) returns (r:nat) {
r := 0;
for i := 0 to |s| {
r := r + s[i];
}
return r;
}
method main() {
assert sumspec([1,2,3],3) == 6;
var r := sum([1,2,3]);
assert r == 6;
}
Хотя sumspec()
является действительной спецификацией для sum()
, мы не связываем эти две вещи. Таким образом, Дафни предполагает, что sum()
может вернуть любое значение для r
!
Чтобы связать спецификацию (sumspec
) с ее реализацией (sum
), нужно более сильное постусловие:
method sum(s:seq<nat>) returns (r:nat)
ensures r == sumspec(s,|s|) {
r := 0;
for i := 0 to |s|
invariant r == sumspec(s,i) {
r := r + s[i];
}
return r;
}
Здесь r == sumspec(s,|s|)
связывает спецификацию с результатом нашей реализации. Мы также добавили цикл invariant
, чтобы помочь Дафни показать, что это постусловие выполняется.
Что ж, это было бы началом. Но я подозреваю, что вы не получите этот инвариант цикла для проверки. Вам, вероятно, придется переработать bullspec
и cowspec
, я думаю.
О, спасибо, я снова напишу код, спасибо за ваше предложение
Итак, в методе BullCows я добавлю гарантии b == bullspec(s,u), а затем в цикле я тоже добавлю инвариант b == bullspect(s,u), верно?