Проблема в том, что ваше определение s
и ваша конструкция o
идут в «разных направлениях». Рекурсивный случай s
определяет s(i)
в терминах i[0]
и того, что «ранее» определено в s(i[1..])
. Напротив, итерация цикла определяет новый o
в терминах i[n]
и предыдущего значения o
. Потребовалась бы индуктивно доказанная лемма, чтобы установить обязательные доказательства в вашей текущей программе, и Дафни не изобрел такие леммы сам по себе.
Для записи в этом ответе, вот что вы начали с:
function s(i: seq): seq {
if |i| == 0 then [] else
if i[0] == 42 then [i[0]] + s(i[1..])
else s(i[1..])
}
method q (i: seq) returns (o: seq)
ensures o == s(i)
{
var n := 0;
o := [];
while n < |i|
invariant n <= |i| && o == s(i[..n])
{
if i[n] == 42 {
o := o + [i[n]];
}
n := n + 1;
}
}
Есть четыре выхода.
Одним из выходов является определение другой версии s
, назовите ее s'
, которая рекурсивно повторяется с другого конца данной последовательности. Затем замените s
на s'
в спецификации вашего метода и инвариант цикла. Это хорошее решение, если только по какой-то причине вы не предпочитаете s
, а не s'
, в спецификации вашего метода.
Второй выход - определить такое s'
и доказать лемму о том, что s(i)
и s'(i)
возвращают одно и то же значение. Это позволит вам сохранить s
в спецификации вашего метода за счет наличия двух определений функций и необходимости написать (и доказать и использовать) лемму.
Третий выход состоит в том, чтобы изменить цикл на итерацию «вниз» вместо «вверх». То есть начните n
с |i|
и уменьшите n
в теле цикла. (Как обычно, увеличение в n
обычно лучше всего делать в конце тела цикла (постинкремент), тогда как уменьшение в n
обычно лучше всего делать в начале тела цикла (предварительное уменьшение)). .)
Четвертый выход - изменить способ записи инварианта цикла относительно o
. В настоящее время инвариант говорит о том, что вы уже вычислили, то есть o == s(i[..n])
. Вместо этого вы можете написать инвариант в терминах того, что еще предстоит вычислить, как в o + s(i[n..]) == s(i)
, который вы можете прочитать как «как только я добавлю s(i[n..])
в o
, у меня будет s(i)
». Вот эта версия q
:
method q(i: seq) returns (o: seq)
ensures o == s(i)
{
var n := 0;
o := [];
while n < |i|
invariant n <= |i| && o + s(i[n..]) == s(i)
{
if i[n] == 42 {
o := o + [i[n]];
}
n := n + 1;
}
}
Вам также может быть интересно посмотреть этот эпизод Угол проверки на эту тему.
Rustan
Не возможно сохранить шаблон отчета в XMLformat. XML поддерживается как формат экспорта "представленного" отчета только.
Поскольку, что цель, Вам нужен шаблон отчета в формате XML. Существует решение для создания отчетов Java под названием Совершенно ясный, который может читать, отчет Отчетов о Crytsal обрабатывают по шаблону и сохраняют его как шаблон отчета XML. Наоборот это не работает. После создания XML-файла, Вы не можете открыть отчет с Crystal Reports снова. Но можно работать с отчетом, использующим Совершенно ясный, который идет с разработчиком GUI также.
Я просто протестировал в Crystal Reports 10.
Откройте отчет, Вы хотите экспортировать, нажать на экспорт в меню файла, и по крайней мере в CR 10, XML в самой нижней части.
Затем экран появляется, прося каталог и основное имя файла сохранять к. Согласно Окну это использует "Кристаллический Язык разметки" Формат XML
По крайней мере, в версии 8.5 XML-файл является одним из поддерживаемых мест назначения экспорта точно так же, как PDF, Excel или Word. Кажется маловероятным, они удалили бы поддержку в более поздних версиях.