我试图将这段伪代码转换为 SMT-LIB 语言，但我卡住了。
List function my_fun(int x)
{
list = nil
for(i in 1 to x):
if(some_condition_on_i)
list.concat(i)
return list
}
到目前为止我所做的是：
(declare-const l1 (List Int))
(define-fun my_fun ((x Int)) (List Int)
(forall ((t Int))
(ite (and (some_condition_on_t) (< t x)) (insert t l1) l1 )
)
)
)
我知道这是错误的，而且不起作用。你能帮我理解我该怎么做吗？
SMT-LIB 建模逻辑，其中变量始终不可变；另一方面，您的代码似乎是命令式的，即诸如此类的变量list and i是可变的。这种关键的差异将是编码程序时面临的最大挑战，而推理命令式程序的挑战引发了诸如Dafny https://github.com/Microsoft/dafny, Boogie https://github.com/boogie-org/boogie, or Viper http://viper.ethz.ch/
以下是一些提示：
-
(insert t l1)代表一个新列表，通过插入得到t into l1。它会not modify l1（并且无法修改 l1，因为它是逻辑变量）
- 一个合乎逻辑的forall是一个布尔公式（它的计算结果是true or false），它不是您可以执行的语句（例如其副作用）
-
如果值x是静态已知的（即如果它是5），然后你可以展开循环（这里是伪代码）：
l0 := Nil
l1 := ite(condition(1), insert(1, l0), l0)
l2 := ite(condition(2), insert(2, l1), l1)
...
l4 := ite(condition(4), insert(4, l3), l3)
- 如果值
x不是静态已知的，那么您很可能需要一个循环不变式或与固定点为了考虑未知数量的循环迭代
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
