如何在Alloy中查看函数返回值并完成自定义函数的功能测试

你可以通过以下两种常用方案完成函数逻辑验证、结果查看：

方法1：用断言自动校验全量场景 #

这是Alloy最推荐的逻辑验证方式，无需手动构造输入，Alloy会自动遍历指定范围内的所有合法实例，校验函数是否符合预期行为，示例代码如下：

// 断言定义：getTime返回的时间一定大于等于输入集合内所有文件的时间
assert getTimeIsMax {
    all F: set File | all f: F | gte[getTime[F], f.time]
}
// 设定实例范围，执行断言校验
check getTimeIsMax for 3 File, 3 Time

运行上述check指令后，如果没有找到反例，说明在你设定的3个File、3个Time的范围内，函数逻辑完全符合预期；如果存在反例，Alloy会直接展示不符合逻辑的实例供你排查。

方法2：手动构造测试用例，直观查看函数输出 #

如果你需要自定义输入场景，直接查看函数的返回结果，可以编写测试谓词构造指定场景，配合评估器或者辅助变量查看输出：

步骤1：编写测试谓词 #

// 测试用例：存在2个时间不同的文件
pred customTestCase {
    #File = 2
    all disj f1, f2: File | f1.time != f2.time
}
// 运行测试用例
run customTestCase for 2 File, 2 Time

步骤2：查看函数输出 #

运行run指令得到合法实例后，有两种方式查看结果：

• 打开可视化界面顶部的「Evaluator」（评估器），输入getTime[File]回车，就能直接看到函数返回的Time值
• 如果你希望输出直接展示在可视化实例中，可以给谓词加输出绑定变量：

pred testCaseWithOutput[out: Time] {
    #File = 2
    all disj f1, f2: File | f1.time != f2.time
    out = getTime[File]
}
run {some out: Time | testCaseWithOutput[out]} for 2 File, 2 Time

运行后out变量会直接出现在实例可视化界面中，无需打开评估器即可查看结果。

额外优化提示 #

你当前编写的getTime逻辑可以借助util/ordering模块提供的max函数简化，简化后逻辑和原有逻辑完全等价：

fun getTime[F : set File] : Time {
    max[f.time | f in F]
}

内容的提问来源于stack exchange，提问作者chai_tea