文章/答案/技术大牛

发布

社区首页 >问答首页 >合成一个保持循环不变和变体的循环程序。

问合成一个保持循环不变和变体的循环程序。
EN

Stack Overflow用户

提问于 2022-01-13 23:53:31

回答 1查看 60关注 0票数 0

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

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

变式：

n − x

程序结构如下：

while<cond>
   <invariant specification>
   <body>

程序应该是如何用frama或why3编写的？

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

#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;
    }
}

thoose的警告是：

[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.

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

frama-c

why3

回答 1

Stack Overflow用户

回答已采纳

发布于 2022-01-14 07:46:24

目前还不清楚您想要实现什么，但是这里有一个C程序，可以用frama-c -wp loop.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^21比使用2^64-1的立方根更容易。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/70704521

复制

相似问题

问合成一个保持循环不变和变体的循环程序。
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问合成一个保持循环不变和变体的循环程序。EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问合成一个保持循环不变和变体的循环程序。
EN