让我从这个例子开始我的问题：
void A (void)
{
B();
C();
D();
E();
... // function calls go on.
return;
}
现在让我们在代码中添加 ACSL 注释：
/*@
ensures PostConditionOfB();
ensures PostConditionOfC();
ensures PostConditionOfD();
ensures PostConditionOfE();
... // ensuring the predicates of the remaining functions goes on.
*/
void A (void)
{
B();
C();
D();
E();
... // function calls go on.
return;
}
我让 Frama-C 通过执行“frama-c-gui -wp file.c”来检查代码。在函数 A 中调用函数 B、C 和 D 时，合约标记为有效。通过添加函数 E 和可能更多其他函数的调用，合约被标记为无效。我们提出了在每个函数调用之后立即添加“断言”的想法，以便为 Frama-C 提供假设满足哪些后置条件的线索。通过这种方法，合同被标记为有效。查看代码：
/*@
ensures PostConditionOfB();
ensures PostConditionOfC();
ensures PostConditionOfD();
ensures PostConditionOfE();
... // ensuring the predicates of the remaining functions goes on.
*/
void A (void)
{
B();
//@ assert PostConditionOfB();
C();
//@ assert PostConditionOfB();
//@ assert PostConditionOfC();
D();
//@ assert PostConditionOfB();
//@ assert PostConditionOfC();
//@ assert PostConditionOfD();
E();
//@ assert PostConditionOfB();
//@ assert PostConditionOfC();
//@ assert PostConditionOfD();
//@ assert PostConditionOfE();
... // function calls go on.
return;
}
问题来了：有没有更好的方法来检查包含多个函数调用的函数的合同，而不是在每个函数调用之后立即添加“断言”？
更新代码：
file.h 如下所示：
#define SIZE_FIRST 100
#define SIZE_SECOND 30
#define SIZE_THIRD 30
typedef struct
{
int Field_5;
int Field_6;
} Struct_C;
typedef struct
{
int Field_1;
int Field_2;
int Field_3;
int Field_4;
Struct_C At_1 [ SIZE_SECOND ];
Struct_C At_2 [ SIZE_THIRD ];
Struct_C At_3 [ SIZE_THIRD ];
} Struct_B;
typedef struct
{
Struct_B At [ SIZE_FIRST ];
int Count;
} Struct_A;
/*@ predicate
Reset_Basics (Struct_B * Stct_B) =
(Stct_B->Field_1 == 0) &&
(Stct_B->Field_2 == 0) &&
(Stct_B->Field_3 == 0) &&
(Stct_B->Field_4 == 0);
*/
/*@ predicate
Reset_At_1 (Struct_B * Stct_B, integer First, integer Last) =
\forall integer Index; First <= Index < Last ==>
(Stct_B->At_1 [ Index ].Field_5 == 0) &&
(Stct_B->At_1 [ Index ].Field_6 == 0);
*/
/*@ predicate
Reset_At_2 (Struct_B * Stct_B, integer First, integer Last) =
\forall integer Index; First <= Index < Last ==>
(Stct_B->At_2 [ Index ].Field_5 == 0) &&
(Stct_B->At_2 [ Index ].Field_6 == 0);
*/
/*@ predicate
Reset_At_3 (Struct_B * Stct_B, integer First, integer Last) =
\forall integer Index; First <= Index < Last ==>
(Stct_B->At_3 [ Index ].Field_5 == 0) &&
(Stct_B->At_3 [ Index ].Field_6 == 0);
*/
file.c 如下所示：
#include "file.h"
void Initialize (Struct_A * const Stct_A);
void Reset (Struct_B * const Stct_B);
void Reset_Basics (Struct_B * const Stct_B);
void Reset_At_1 (Struct_B * const Stct_B);
void Reset_At_2 (Struct_B * const Stct_B);
void Reset_At_3 (Struct_B * const Stct_B);
/*@
assigns Stct_A->At [ 0..(SIZE_FIRST - 1) ];
assigns Stct_A->Count;
*/
void Initialize (Struct_A * const Stct_A)
{
/*@
loop invariant 0 <= Index <= SIZE_FIRST;
loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index <
Index) ==> Reset_Basics(&(Stct_A->At [ Stct_B_Index ]));
loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index <
Index) ==> Reset_At_1(&(Stct_A->At [ Stct_B_Index ]), 0,
SIZE_SECOND);
loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index <
Index) ==> Reset_At_2(&(Stct_A->At [ Stct_B_Index ]), 0,
SIZE_THIRD);
loop invariant \forall integer Stct_B_Index; (0 <= Stct_B_Index <
Index) ==> Reset_At_3(&(Stct_A->At [ Stct_B_Index ]), 0,
SIZE_THIRD);
loop assigns Index, Stct_A->At [ 0..(SIZE_FIRST - 1) ];
loop variant SIZE_FIRST - Index;
*/
for (int Index = 0; Index < SIZE_FIRST; ++(Index))
{
Reset(&(Stct_A->At [ Index ]));
}
Stct_A->Count = 0;
return;
}
/*@
assigns * Stct_B;
ensures Reset_Basics(Stct_B);
*/
void Reset_Basics (Struct_B * const Stct_B)
{
Stct_B->Field_1 = 0;
Stct_B->Field_2 = 0;
Stct_B->Field_3 = 0;
Stct_B->Field_4 = 0;
return;
}
/*@
assigns Stct_B->At_1 [ 0..(SIZE_SECOND - 1) ];
ensures Reset_At_1(Stct_B, 0, SIZE_SECOND);
*/
void Reset_At_1 (Struct_B * const Stct_B)
{
/*@
loop invariant 0 <= Index <= SIZE_SECOND;
loop invariant Reset_At_1(Stct_B, 0, Index);
loop assigns Index, Stct_B->At_1 [ 0..(SIZE_SECOND - 1) ];
loop variant SIZE_SECOND - Index;
*/
for (int Index = 0; Index < SIZE_SECOND; ++(Index))
{
Stct_B->At_1 [ Index ].Field_5 = 0;
Stct_B->At_1 [ Index ].Field_6 = 0;
}
return;
}
/*@
assigns Stct_B->At_2 [0..(SIZE_THIRD - 1)];
ensures Reset_At_2(Stct_B, 0, SIZE_THIRD);
*/
void Reset_At_2 (Struct_B * Stct_B)
{
/*@
loop invariant 0 <= Index <= SIZE_THIRD;
loop invariant Reset_At_2(Stct_B, 0, Index);
loop assigns Index, Stct_B->At_2 [0..(SIZE_THIRD - 1)];
loop variant SIZE_THIRD - Index;
*/
for (int Index = 0; Index < SIZE_THIRD; ++(Index))
{
Stct_B->At_2 [ Index ].Field_5 = 0;
Stct_B->At_2 [ Index ].Field_6 = 0;
}
return;
}
/*@
assigns Stct_B->At_3 [0..(SIZE_THIRD - 1)];
ensures Reset_At_3(Stct_B, 0, SIZE_THIRD);
*/
void Reset_At_3 (Struct_B * Stct_B)
{
/*@
loop invariant 0 <= Index <= SIZE_THIRD;
loop invariant Reset_At_3(Stct_B, 0, Index);
loop assigns Index, Stct_B->At_3 [0..(SIZE_THIRD - 1)];
loop variant SIZE_THIRD - Index;
*/
for (int Index = 0; Index < SIZE_THIRD; ++(Index))
{
Stct_B->At_3 [ Index ].Field_5 = 0;
Stct_B->At_3 [ Index ].Field_6 = 0;
}
return;
}
/*@
assigns * Stct_B;
ensures Reset_Basics(Stct_B);
ensures Reset_At_1(Stct_B, 0, SIZE_SECOND);
ensures Reset_At_2(Stct_B, 0, SIZE_THIRD);
ensures Reset_At_3(Stct_B, 0, SIZE_THIRD);
*/
void Reset (Struct_B * const Stct_B)
{
Reset_Basics(Stct_B);
Reset_At_1(Stct_B);
Reset_At_2(Stct_B);
Reset_At_3(Stct_B);
return;
}