我不明白为什么frama-c不能证明这部分的shell排序算法。我将 Astraver 与 Alt-Ergo 2.4.3 和 CVC v1.8 一起使用，它们将最后一个循环中的条件标记为证明问题。怎么了？
#include <stdlib.h>
#include <string.h>
/*@ predicate ArraysEquality{L}(int *a, int *b, integer m, integer n) =
@ \forall integer k; m <= k < n ==> a[k] == b[k];
@
@ predicate Sorted{L}(int *a, integer n) =
@ \forall integer i, j; 0 <= i <= j < n ==> a[i] <= a[j];
@
@ predicate CopiedArray(int *dest, int *src, integer n) =
@ \forall integer i; 0 <= i < n ==> dest[i] == src[i];
@
@ predicate Swap{L1, L2}(int *a, integer n, integer i, integer j) =
@ 0 <= i < n && 0 <= j < n &&
@ \at(a[i], L1) == \at(a[j], L2) &&
@ \at(a[j], L1) == \at(a[i], L2) &&
@ \forall integer k; 0 <= k < n && k != i && k != j
@ ==> \at(a[k], L1) == \at(a[k], L2);
@
@ inductive Permutation{L1, L2}(int *a, integer n) {
@ case reflexive{L1}:
@ \forall int *a, integer n;
@ Permutation{L1, L1}(a, n);
@
@ case transitive{L1, L2, L3}:
@ \forall int *a, integer n;
@ Permutation{L1, L2}(a, n) && Permutation{L2, L3}(a, n)
@ ==> Permutation{L1, L3}(a, n);
@
@ case swapstep{L1, L2}:
@ \forall int *a, integer n, i, j;
@ Swap{L1, L2}(a, n, i, j)
@ ==> Permutation{L1, L2}(a, n);
@ }
@
@*/
/* lemma subarray_of_copy:
\forall int *a, *b, integer n, l, r;
0 <= l < r < n && CopiedArray(a, b, n) ==> ArraysEquality(a, b, l, r);
*/
/* lemma sorted_continuation:
\forall int *a, integer n, i;
1 <= i < n && Sorted(a, i) && a[i - 1] <= a[i]
==> Sorted(a, i);
*/
/*@ requires \valid(dest + (0..n-1));
@ requires \valid(src + (0..n-1));
@ requires n > 1;
@ assigns dest[0..n-1];
@ ensures CopiedArray(dest, src, n);
@*/
void copyArray(int* dest, const int* src, size_t n) {
memcpy(dest, src, n * sizeof(int));
}
/*@ requires \valid(arr + (0..n-1));
@ requires n > 1;
@ requires 0 < gap < n;
@ //ensures Swap{Pre, Post}(arr, n, i, i - gap);
@ //ensures Permutation{Pre, Post}(arr, n);
@*/
void fun(int *arr, int n, int gap, int i) {
int tmp, j;
//@ ghost int tmp_for_copy;
//@ ghost int *arr_copy = malloc(n * sizeof(int));
//@ ghost copyArray(arr_copy, arr, n);
//@ assert CopiedArray(arr_copy, arr, n);
//@ assert CopiedArray(arr_copy, arr, n) ==> ArraysEquality(arr, arr_copy, 0, n);
//@ ghost beforeEntry:
/*@ loop invariant gap <= i <= n;
@ //loop invariant gap == 1 ==> Sorted(arr, 0, i);
@ //loop invariant Permutation{Pre, Here}(arr, n);
@ //loop invariant ArraysEquality(arr, arr_copy, 0, i);
@ loop assigns i, j, tmp, arr[0..n-1];
@ loop variant n - i;
@*/
for (i = gap; i < n; ++i) {
tmp = arr[i];
// assert ArraysEquality(arr, arr_copy, 0, i);
//@ ghost int counter = 0;
/*@ loop invariant gap <= i < n;
@ loop invariant 0 <= j <= i;
@ loop invariant j != i ==> arr[j] > tmp && arr[j] == arr[j + gap];
@ loop invariant j == i ==> arr[j] == tmp;
@ loop invariant Permutation{LoopEntry, Here}(arr_copy, n);
@ loop invariant Permutation{LoopEntry, Here}(arr_copy, n) ==> Permutation{beforeEntry, Here}(arr_copy, n);
@ loop assigns j, arr[0..i], arr_copy[0..i], tmp_for_copy;
@ loop variant i - counter;
@*/
for (j = i; j >= gap && arr[j - gap] > tmp; j -= gap) {
//@ ghost counter = counter + 1;
//@ assert j >= gap && j - gap >= 0;
arr[j] = arr[j - gap];
//@ assert arr[j] > tmp;
// assert arr[j - gap] > tmp;
// assert arr[j] == arr[j - gap];
//@ ghost beforeSwap:
//@ ghost tmp_for_copy = arr_copy[j];
//@ ghost arr_copy[j] = arr_copy[j - gap];
//@ ghost arr_copy[j - gap] = tmp_for_copy;
//@ assert Swap{beforeSwap, Here}(arr_copy, n, j, j - gap);
//@ assert Swap{beforeSwap, Here}(arr_copy, n, j, j - gap) ==> Permutation{beforeSwap, Here}(arr_copy, n);
//@ assert Permutation{beforeSwap, Here}(arr_copy, n) ==> Permutation{LoopEntry, Here}(arr_copy, n);
// assert ArraysEquality(arr, arr_copy, j - gap + 1, i);
//@ assert j >= gap;
}
// assert ArraysEquality(arr, arr_copy, j + 1, i);
arr[j] = tmp;
//@ assert j >= 0;
// assert ArraysEquality(arr, arr_copy, j, i);
//@ assert Permutation{beforeEntry, Here}(arr_copy, n);
}
}
arr
数组的副本，以便通过它检查
arr的排列，Frama-c 会用绿色勾号标记循环不变持久性检查。但如果你看一下报告，即使它被标记为已证实，但嵌套循环中带有条件的部分仍然被标记为红色。
希望以下内容对您有所帮助。它是使用 Spark 而不是 Frama-C 编写的，但可能会给您一些关于断言和循环不变量需要什么的想法。
我在Spark包中创建了shell排序功能，它将排序过程与排序过程的实现分离。
包规范包含排序过程的API，包括要排序的数组类型的规范和排序过程的后置条件。
package shell_sort with
SPARK_Mode
is
type idx_t is range 0 .. 9;
type arr_t is array (Idx_t) of Natural;
procedure sort (arr : in out arr_t) with
SPARK_Mode,
Post =>
(for all I in arr'First .. arr'Last - 1 => arr (I) <= arr (I + 1)) and then
(for some I in arr'Old'Range =>
(for some J in arr'Range => arr'Old (I) = arr (J)));
end shell_sort;
后置条件指出，对于数组中从第一个元素到最后一个元素的前一个元素的所有元素，每个元素都小于或等于其下一个元素，并且排序数组中的每个元素也在未排序数组中.
包体包含排序过程的实现。
package body shell_sort with
SPARK_Mode
is
procedure sort (arr : in out arr_t) with
SPARK_Mode
is
procedure swap (left, right : in out Natural) with
Post => left'Old = right and right'Old = left
is
temp : Natural := left;
begin
left := right;
right := temp;
end swap;
original : arr_t := arr;
function found(value : natural) return boolean with
Post =>
( if (for some I in original'range => original(I) = value) then
found'result = True
else
found'result = False) is
result : boolean := false;
begin
if (for some I in original'range => original(I) = value) then
result := true;
end if;
return result;
end found;
begin
loop
pragma Loop_Invariant
(for all I in arr'range => found(arr(I)));
for I in arr'First .. arr'Last - 1 loop
if arr (I) > arr (I + 1) then
swap (arr (I), arr (I + 1));
pragma Assert (arr (I) < arr (I + 1));
end if;
pragma Assert (arr (I) <= arr (I + 1));
end loop;
if (for all I in arr'First .. arr'Last - 1 => arr (I) <= arr (I + 1))
then
exit;
end if;
end loop;
end sort;
end shell_sort;
Spark 允许在其他函数和过程的范围内定义函数和过程。此示例实现了交换过程和查找函数，以简化排序过程中的逻辑并简化第一个循环不变式。
名为 GnatProve 的 Spark 证明器的输出为：
Summary of SPARK analysis
=========================
-------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow CodePeer Provers Justified Unproved
-------------------------------------------------------------------------------------------------------------
Data Dependencies . . . . . .
Flow Dependencies . . . . . .
Initialization . . . . . .
Non-Aliasing 1 1 . . . .
Run-time Checks . . . . . .
Assertions 4 . . 4 (CVC4 95%, Z3 5%) . .
Functional Contracts 3 . . 3 (CVC4 88%, Trivial 13%) . .
LSP Verification . . . . . .
Termination . . . . . .
Concurrency . . . . . .
-------------------------------------------------------------------------------------------------------------
Total 8 1 (13%) . 7 (88%) . .
max steps used for successful proof: 9816
Analyzed 2 units
in unit main, 0 subprograms and packages out of 1 analyzed
Main at main.adb:5 skipped
in unit shell_sort, 4 subprograms and packages out of 4 analyzed
shell_sort at shell_sort.ads:1 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (0 checks)
shell_sort.sort at shell_sort.ads:6 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (5 checks)
shell_sort.sort.found at shell_sort.adb:17 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (1 checks)
shell_sort.sort.swap at shell_sort.adb:7 flow analyzed (0 errors, 0 checks and 0 warnings) and proved (1 checks)