0

我想创建一个具有以下先决条件的程序：不变：

y = x ∗ x ∧ z = y ∗ x ∧ x ≤ n

变体：

n − x

程序结构如下：

while<cond>
   <invariant specification>
   <body>

程序应该如何看起来像用 frama-c 或why3 编写的？

编辑： 我通过删除乘法并添加加法来修改您的程序。通过这样做，我使用了两个循环。我运行了我的程序，但我收到了警告。这是程序：

#include <limits.h>

/*@ requires n < INT_MAX; // avoids overflow in computing z
*/
void f(unsigned long n) {
    unsigned long x = 0, y = 0, z = 0, contor, aux_x, aux_y;
    /*@ loop assigns x, y, z, contor, aux_x, aux_y;
      @ loop invariant y == x * x && z == y * x && x <= n;
      @ loop variant n - x;
      @ */
    while (x < n) {
        x++;
        contor = 1;
        aux_x = 0;
        aux_y = 0;
        /* @ loop assings contor, aux_x, aux_y;
           @ loop invariant 1 <= contor <= x;
           @ loop variant x - contor, x, y;
           @*/
        while (contor <= x) {
            aux_x += x;
            aux_y += y;
            contor++;
        }
        y = aux_x;
        z = aux_y;
    }
}

这些是警告：

[kernel] Parsing loop.c (with preprocessing)
[rte] annotating function f
[wp] loop.c:20: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 6 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_f_loop_assigns_part2 : Timeout (Qed:6ms) (10s) (cached)
[wp] [Alt-Ergo 2.4.1] Goal typed_f_loop_variant_decrease : Timeout (Qed:16ms) (10s) (cached)
[wp] [Alt-Ergo 2.4.1] Goal typed_f_loop_invariant_established : Timeout (Qed:3ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_f_loop_invariant_preserved : Timeout (Qed:11ms) (10s)
[wp] [Cache] found:2, updated:2
[wp] Proved goals:    2 / 6
  Qed:               2  (7ms)
  Alt-Ergo 2.4.1:    0  (interrupted: 4) (cached: 2)
[wp:pedantic-assigns] loop.c:5: Warning: 
  No 'assigns' specification for function 'f'.
  Callers assumptions might be imprecise.

你能解释一下为什么即使我为内部循环指定了不变量和变体，我也会收到那些讨厌的警告吗？

4

1 回答 1

2

目前还不清楚您想要实现什么，但这里有一个可以证明frama-c -wp loop.c并具有适当不变量和变体的 C 程序：

/*@ requires n < 2097152; // avoids overflow in computing z
 */
void f(unsigned long n) {
  unsigned long x = 0, y = 0, z = 0;
  /*@ loop invariant y == x * x && z == y * x && x <= n;
      loop assigns x,y,z;
      loop variant n - x;
  */
  while (x < n) {
    x++;
    y = x * x;
    z = y * x;
  }
}

注意：requires不是为了避免计算时溢出而可以编写的最通用的方法，但它比取 的三次根z更容易计算。2^212^64-1

于 2022-01-14T07:46:24.353 回答