frama- c / ACSL / WP: Мощность множества - PullRequest
Новая
       28

frama- c / ACSL / WP: Мощность множества

2 голосов
/ 20 марта 2020

Я часто использую количество множеств в других формальных спецификациях, и мне интересно, можно ли было использовать его в ACSL с плагином WP frama- c.

Например, мне кажется, что более понятным было бы написать assumes card({*a, *b, *c}) == 3 вместо assumes *a != *b && *a != *c && *b != *c

1 Ответ

1 голос
/ 04 мая 2020

Хорошо, я нашел решение (медленное, предупреждаю вас, пришлось изменить время ожидания с 10 до 30 секунд только для следующего примера). Также он не работает в Frama- C версии Calcium, утверждая, что не может найти библиотеку Qed (похоже, ошибка при попытке вызвать функцию Frama- C типа logic boolean). В 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); */
}
...