Поддержка отладки в Boogie

Question

Я работаю над проектом, использующим Boogie для проверки распределенных приложений. В моей работе мне нужна лучшая поддержка отладки, когда проверка не удалась.

Я просмотрел параметры командной строки и нашел следующие параметры полезными в моем контексте:

1. \mv
2. \z3multipleErrors
3. \break

Я попробовал их, и у меня есть некоторые вопросы / вопросы.

Я попытаюсь объяснить мою проблему с помощью тривиального примера. Ниже приведена спецификация Boogie для увеличения счетчика.

counter.bpl:::

var counter: int;
procedure increment(value: int)
modifies counter;
ensures (counter >= 0);
{
  assume(counter >= 0);
  counter := counter + value;
}

Я выполняю командную строку следующим образом: Boogie.exe /z3multipleErrors /mv:counter.model counter.bpl

Результат:

Boogie program verifier version 2.3.0.61016, Copyright (c) 2003-2014, Microsoft.
counter.bpl(10,1): Error BP5003: A postcondition might not hold on this return path.
counter.bpl(5,1): Related location: This is the postcondition that might not hold.
Execution trace:
    counter.bpl(7,3): anon0

Boogie program verifier finished with 0 verified, 1 error

и модель это:

counter.model:::

*** MODEL
%lbl%@82 -> false
%lbl%+37 -> true
%lbl%+45 -> true
counter -> 0
counter@0 -> (- 1)
value -> (- 1)
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
*** END_MODEL

В этом случае встречным примером является случай, когда value увеличивается на -1, когда counter равно 0. Но я хотел бы иметь больше контрпримеров. Итак, у меня есть два вопроса здесь:

1. Я ожидал /z3multipleErrors возможность дать мне несколько встречных примеров, в данном случае что-то вроде [counter = 0 & value = -1, -2, -3,..], [counter = 1 & value = -2, -3, ...] и т.д. Затем я планирую использовать набор значений, чтобы получить представление об ошибке, в данном случае value отрицательно. Я что-то здесь упускаю?
2. Является ли встречный пример "минимальным счетчиком"? Я знаю, что этот случай является тривиальным примером, но я хотел бы знать, всегда ли я получаю минимальный контрпример.

Предположим, у меня есть связанный список, который я проверяю, является ли он линейным. В качестве встречного примера я могу получить следующие результаты:1 -> 1 или же 1 -> 2 -> 3 -> 4 ..... -> 1Оба являются идеальными контрпримерами, но первый - минимальный контрпример.

Теперь переходим к следующему этапу моего выпуска.

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

matrix.bpl:::

var matrix: [int][int]int;
procedure modify(row:int, column:int, value: int)
modifies matrix;
ensures (forall r, c:int :: matrix[r][c] >= 0);
{

matrix.model:::

*** MODEL
%lbl%@193 -> false
%lbl%+104 -> true
%lbl%+79 -> true
c@@0!0!0 -> 2
column -> 2
matrix -> |T@[Int][Int]Int!val!0|
matrix@0 -> |T@[Int][Int]Int!val!1|
r@@0!0!1 -> 1
row -> 1
value -> (- 563)
Store_[$int]$int -> {
  |T@[Int]Int!val!1| 2 (- 563) -> |T@[Int]Int!val!0|
  else -> |T@[Int]Int!val!0|
}
Select_[$int]$int -> {
  |T@[Int]Int!val!0| 2 -> (- 563)
  |T@[Int]Int!val!1| 2 -> 0
  else -> (- 563)
}
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
Select_[$int][$int]$int -> {
  |T@[Int][Int]Int!val!1| 1 -> |T@[Int]Int!val!0|
  |T@[Int][Int]Int!val!0| 1 -> |T@[Int]Int!val!1|
  else -> |T@[Int]Int!val!0|
}
Store_[$int][$int]$int -> {
  |T@[Int][Int]Int!val!0| 1 |T@[Int]Int!val!0| -> |T@[Int][Int]Int!val!1|
  else -> |T@[Int][Int]Int!val!1|
}
*** END_MODEL

В идеале вывод здесь должен быть таким же, как и неотрицательный счетчик выше, т. Е. Значение должно быть неотрицательным. Но понимание этой информации из этого контрпримера требует больших усилий.

У меня есть два вопроса в этом контексте:

1. Прилагаются ли какие-то усилия, чтобы сделать контрпример понятным для неопытных пользователей? Я видел интерфейс BVD, но я почувствовал, что это небольшое украшение модели простого текста.
2. Описание \break Флаг выглядит многообещающе, но я вижу, что он еще не реализован. Было бы полезно узнать статус этого. Есть ли работа в процессе?

Спасибо, что нашли время, чтобы прочитать этот длинный отчет. Буду признателен за любую помощь, даже если она решит лишь небольшую часть вопроса.