gpt4 book ai didi

recursion - 在合金中编程递归函数

转载 作者:行者123 更新时间:2023-12-05 01:48:06 28 4
gpt4 key购买 nike

我正在尝试在 Alloy 中构造一个递归函数。根据 Daniel Jackson 书中显示的语法,这是可能的。我的功能是:

fun auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method]: Method{
(m.b.id = idTarget) => {
m
} else (m.b.id != idTarget) => {
(m.b = LiteralValue) => {
m
} else {
some mRet:Method, c:Class | mRet in c.methods && m.b.id = mRet.id => auxiliaryToAvoidCyclicRecursion[idTarget, mRet]
}
}
}

但是求解器声称调用 auxiliaryToAvoidCyclicRecursion[idTarget, mRet] 说:

"This must be a formula expression.
Instead, it has the following possible type(s):
{this/Method}"

最佳答案

问题正是错误消息所说的:auxiliaryToAvoidCyclicRecursion 函数的返回类型是 Method,您正试图在 bool 蕴涵中使用它,其中公式是预期的(即 bool 类型的东西)。在任何其他静态类型语言中,您都会遇到同样类型的错误。

您可以将函数重写为谓词来解决此问题:

pred auxiliaryToAvoidCyclicRecursion[idTarget:MethodId, m:Method, ans: Method] {
(m.b.id = idTarget) => {
ans = m
} else (m.b.id != idTarget) => {
(m.b = LiteralValue) => {
ans = m
} else {
some mRet:Method, c:Class {
(mRet in c.methods && m.b.id = mRet.id) =>
auxiliaryToAvoidCyclicRecursion[idTarget, mRet, ans]
}
}
}
}

这应该不会给您带来编译错误,但要运行它请确保启用递归(选项 -> 递归深度)。正如您将看到的,最大递归深度为 3,这意味着无论您的分析范围如何,Alloy Analyzer 最多可以展开您的递归调用 3 次。如果这还不够,您仍然可以选择重写您的模型,以便将有问题的递归谓词建模为关系。这是一个简单的例子来说明这一点。

具有用于计算列表长度的递归定义函数的链表:

sig Node {
next: lone Node
} {
this !in this.^@next
}

fun len[n: Node]: Int {
(no n.next) => 1 else plus[1, len[n.next]]
}

// instance found when recursion depth is set to 3
run { some n: Node | len[n] > 3 } for 5 but 4 Int

// can't find an instance because of too few recursion unrollings (3),
// despite the scope being big enough
run { some n: Node | len[n] > 4 } for 5 but 4 Int

现在相同的列表,其中 len 被建模为一个关系(即 Node 中的一个字段)

sig Node {
next: lone Node,
len: one Int
} {
this !in this.^@next
(no this.@next) => this.@len = 1 else this.@len = plus[next.@len, 1]
}

// instance found
run { some n: Node | n.len > 4 } for 5 but 4 Int

请注意,后一种方法不使用递归(因此不依赖于“递归深度”配置选项的值),可能(而且通常)比前者慢得多。

关于recursion - 在合金中编程递归函数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/18921400/

28 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com