使用 Frama-C 验证线性搜索
Verification of a linear search with Frama-C
我再次对一个简单的验证练习感到困惑,这次是在 Frama-C (Sodium) 中使用 WP 插件,因为我无法让 Jessie 在 uni 工作站上工作(正在安装过程中)管理员 staff/team。)我一直在阅读 'ACSL by example' 和手册。尽管我认为这个示例足够简单,可以很快得到正确的结果。在使用 Dafny 和 Whiley 验证相同的算法后,也许我的算法有点被污染了。
#include <stdio.h>
// A linear search over a sorted array looking for a given element.
/*@ requires len > 0;
@ requires \valid( ls+ ( 0..(len - 1) ) );
@ requires \forall size_t k; 0 <= k < (len - 1) ==> ls[k] <= ls[k + 1];
@ assigns \nothing;
@ behavior found:
@ assumes \exists size_t k; 0 <= k < len && ls[k] == item;
@ ensures \result >= 0;
@ behavior nfound:
@ assumes \forall size_t k; 0 <= k < len ==> ls[k] != item;
@ ensures \result == -1;
@ complete behaviors found, nfound;
@ disjoint behaviors found, nfound;
*/
int search( int ls[], const size_t len, int item )
{
size_t i = 0;
/*@ loop invariant 0 <= i <= len;
@ loop invariant \forall size_t k; 0 <= k < i ==> ls[k] != item;
@ loop assigns i;
@ loop variant len - i;
*/
while ( i < len )
{
if ( ls[i] == item )
return i;
++i;
}
return -1;
}
int main()
{
int src[] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 };
if ( search( src, 10, 5 ) >= 0 ) printf( "found item" );
else printf( "no item found" );
}
我在尝试验证时得到的输出是:
$ frama-c -pp-annot -wp -wp-rte -wp-timeout 100 search.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing search.c (with preprocessing)
/tmp/ppannot97a491.c:1:0: warning: "__STDC_VERSION__" redefined
#define __STDC_VERSION__ 201112L
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:2:0: warning: "__STDC_UTF_16__" redefined
#define __STDC_UTF_16__ 1
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:3:0: warning: "__STDC_UTF_32__" redefined
#define __STDC_UTF_32__ 1
^
<built-in>: note: this is the location of the previous definition
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[rte] annotating function search
[wp] 20 goals scheduled
[wp] [Qed] Goal typed_main_call_search_pre : Valid
[wp] [Qed] Goal typed_main_call_search_pre_2 : Valid
[wp] [Alt-Ergo] Goal typed_search_complete_found_nfound : Valid (10ms) (19)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_preserved : Valid (17ms) (21)
[wp] [Alt-Ergo] Goal typed_search_disjoint_found_nfound : Valid (13ms) (19)
[wp] [Qed] Goal typed_search_loop_inv_established : Valid
[wp] [Qed] Goal typed_search_loop_inv_2_established : Valid
[wp] [Alt-Ergo] Goal typed_main_call_search_pre_3 : Valid (383ms) (93)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_2_preserved : Valid (17ms) (33)
[wp] [Qed] Goal typed_search_loop_assign : Valid
[wp] [Alt-Ergo] Goal typed_search_assert_rte_mem_access : Valid (50ms) (89)
[wp] [Alt-Ergo] Goal typed_search_assert_rte_unsigned_overflow : Valid (13ms) (30)
[wp] [Qed] Goal typed_search_assign_part1 : Valid
[wp] [Qed] Goal typed_search_assign_part2 : Valid
[wp] [Qed] Goal typed_search_assign_part3 : Valid
[wp] [Qed] Goal typed_search_assign_part4 : Valid
[wp] [Qed] Goal typed_search_loop_term_decrease : Valid (3ms)
[wp] [Qed] Goal typed_search_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_search_nfound_post : Valid (17ms) (33)
[wp] [Alt-Ergo] Goal typed_search_found_post : Unknown (54.3s)
[wp] Proved goals: 19 / 20
Qed: 11 (3ms-3ms)
Alt-Ergo: 8 (10ms-383ms) (93) (unknown: 1)
这让我困惑了一段时间,但在尝试 Coq 证明之后,我发现你无法证明 found
行为的原因很简单......它是 不 正确。即,对于 len > INT_MAX
和在数组的 INT_MAX
第一个单元格中未找到但出现在稍后某处的 item
,结果,如 int
所示,将是消极的。
好吧,从技术上讲,这是实现定义的,如 C99,6.3.1.3§3 中所述:
Otherwise, the new type is signed and the value cannot be represented in
it; either the result is implementation-defined or an
implementation-defined signal is raised.
如果您将选项 -warn-signed-downcast
添加到您的命令行,您将看到一个新的 RTE-generated 未被证明的断言:
/*@ assert rte: signed_downcast: i ≤ 2147483647; */
然后 found
行为的 post-condition 在上述断言成立的假设下得到证明。
我再次对一个简单的验证练习感到困惑,这次是在 Frama-C (Sodium) 中使用 WP 插件,因为我无法让 Jessie 在 uni 工作站上工作(正在安装过程中)管理员 staff/team。)我一直在阅读 'ACSL by example' 和手册。尽管我认为这个示例足够简单,可以很快得到正确的结果。在使用 Dafny 和 Whiley 验证相同的算法后,也许我的算法有点被污染了。
#include <stdio.h>
// A linear search over a sorted array looking for a given element.
/*@ requires len > 0;
@ requires \valid( ls+ ( 0..(len - 1) ) );
@ requires \forall size_t k; 0 <= k < (len - 1) ==> ls[k] <= ls[k + 1];
@ assigns \nothing;
@ behavior found:
@ assumes \exists size_t k; 0 <= k < len && ls[k] == item;
@ ensures \result >= 0;
@ behavior nfound:
@ assumes \forall size_t k; 0 <= k < len ==> ls[k] != item;
@ ensures \result == -1;
@ complete behaviors found, nfound;
@ disjoint behaviors found, nfound;
*/
int search( int ls[], const size_t len, int item )
{
size_t i = 0;
/*@ loop invariant 0 <= i <= len;
@ loop invariant \forall size_t k; 0 <= k < i ==> ls[k] != item;
@ loop assigns i;
@ loop variant len - i;
*/
while ( i < len )
{
if ( ls[i] == item )
return i;
++i;
}
return -1;
}
int main()
{
int src[] = { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 };
if ( search( src, 10, 5 ) >= 0 ) printf( "found item" );
else printf( "no item found" );
}
我在尝试验证时得到的输出是:
$ frama-c -pp-annot -wp -wp-rte -wp-timeout 100 search.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing search.c (with preprocessing)
/tmp/ppannot97a491.c:1:0: warning: "__STDC_VERSION__" redefined
#define __STDC_VERSION__ 201112L
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:2:0: warning: "__STDC_UTF_16__" redefined
#define __STDC_UTF_16__ 1
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannot97a491.c:3:0: warning: "__STDC_UTF_32__" redefined
#define __STDC_UTF_32__ 1
^
<built-in>: note: this is the location of the previous definition
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[rte] annotating function search
[wp] 20 goals scheduled
[wp] [Qed] Goal typed_main_call_search_pre : Valid
[wp] [Qed] Goal typed_main_call_search_pre_2 : Valid
[wp] [Alt-Ergo] Goal typed_search_complete_found_nfound : Valid (10ms) (19)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_preserved : Valid (17ms) (21)
[wp] [Alt-Ergo] Goal typed_search_disjoint_found_nfound : Valid (13ms) (19)
[wp] [Qed] Goal typed_search_loop_inv_established : Valid
[wp] [Qed] Goal typed_search_loop_inv_2_established : Valid
[wp] [Alt-Ergo] Goal typed_main_call_search_pre_3 : Valid (383ms) (93)
[wp] [Alt-Ergo] Goal typed_search_loop_inv_2_preserved : Valid (17ms) (33)
[wp] [Qed] Goal typed_search_loop_assign : Valid
[wp] [Alt-Ergo] Goal typed_search_assert_rte_mem_access : Valid (50ms) (89)
[wp] [Alt-Ergo] Goal typed_search_assert_rte_unsigned_overflow : Valid (13ms) (30)
[wp] [Qed] Goal typed_search_assign_part1 : Valid
[wp] [Qed] Goal typed_search_assign_part2 : Valid
[wp] [Qed] Goal typed_search_assign_part3 : Valid
[wp] [Qed] Goal typed_search_assign_part4 : Valid
[wp] [Qed] Goal typed_search_loop_term_decrease : Valid (3ms)
[wp] [Qed] Goal typed_search_loop_term_positive : Valid
[wp] [Alt-Ergo] Goal typed_search_nfound_post : Valid (17ms) (33)
[wp] [Alt-Ergo] Goal typed_search_found_post : Unknown (54.3s)
[wp] Proved goals: 19 / 20
Qed: 11 (3ms-3ms)
Alt-Ergo: 8 (10ms-383ms) (93) (unknown: 1)
这让我困惑了一段时间,但在尝试 Coq 证明之后,我发现你无法证明 found
行为的原因很简单......它是 不 正确。即,对于 len > INT_MAX
和在数组的 INT_MAX
第一个单元格中未找到但出现在稍后某处的 item
,结果,如 int
所示,将是消极的。
好吧,从技术上讲,这是实现定义的,如 C99,6.3.1.3§3 中所述:
Otherwise, the new type is signed and the value cannot be represented in it; either the result is implementation-defined or an implementation-defined signal is raised.
如果您将选项 -warn-signed-downcast
添加到您的命令行,您将看到一个新的 RTE-generated 未被证明的断言:
/*@ assert rte: signed_downcast: i ≤ 2147483647; */
然后 found
行为的 post-condition 在上述断言成立的假设下得到证明。