我经常在其他正式规范中使用集合的基数,我想知道是否可以在带有 WP frama-c 插件的 ACSL 中使用它。
例如,我觉得写
assumes card({*a, *b, *c}) == 3
比
写更清楚assumes *a != *b && *a != *c && *b != *c
好吧,我找到了一个解决方案(我警告你一个缓慢的解决方案,必须将超时从 10 秒更改为 30 秒,仅用于以下示例)。它在 Frama-C 版本的 Calcium 中也被破坏,声称它找不到 Qed 库(该错误似乎是在尝试调用logic boolean
类型 Frama-C 函数)。它在 Frama-C 版本的 Chlorine 中正常工作(没有测试其他版本)。
/* "set" appears to be a reserved word in frama-c */
/*@ predicate full_card{L}(unsigned int* the_set, integer set_size) =
\forall integer a, b; 0 <= a < set_size && 0 <= b < set_size && a != b ==> the_set[a] != the_set[b];
*/
/*@ logic boolean in_set_bool{L}(unsigned int* the_set, integer set_size, unsigned int element) =
set_size == 0 ? \false : element == the_set[0] || in_set_bool(the_set + 1, set_size - 1, element);
*/
/*@ logic integer card{L}(unsigned int* the_set, integer set_size) =
set_size == 0 ? 0 : (
in_set_bool(the_set + 1, set_size - 1, the_set[0])
? card(the_set + 1, set_size - 1)
: card(the_set + 1, set_size - 1) + 1);
*/
int main(int argc, char** argv) {
unsigned int set[] = { 1, 2, 3 };
unsigned int set_size = 3;
/*@ assert full_card(&set[0], set_size); */
/*@ assert card(&set[0], set_size) == 3; */
unsigned int set_two[] = { 3, 2, 1, 3 };
unsigned int set_two_size = 4;
/*@ assert card(&set_two[0], set_two_size) == 3; */
/*@ assert !full_card(&set_two[0], set_two_size); */
}