在谓词中使用方法：Dafny

Question

我想在谓词内使用方法。简要说明：

我定义了一个数据类型 RSState，如下元组所示。

datatype RSState = RSState(ceilingPrio: nat,
                            takenBy: nat,
                            cs: map<Process, TState>)

在有效性不变量中，我想使用

ceilingPrio

方法设置（检查，不是设置...它是谓词！）

Max

字段。

predicate validRS(r: RSState, T: set<Process>)
{
    r.cs.Keys == T &&
    r.ceilingPrio == Max(T)
}

Max(T)

是一种从集合中找到最大的方法：

datatype Process = Process(id: nat,
                    qPrio: nat)

function maximum(x: nat, y: nat): (m: nat)
    ensures m >= x
    ensures m >= y
{
    if x >= y then x else y
}

method Max(s: set<P>) returns (t: nat)
    requires s != {} && validTS(s)
    ensures forall p :: p in s ==> p.qPrio <= t
{
    var x :| x in s;
    if s == {x} {
        t := x.qPrio;
    } else {
        var s' := s - {x};
        var y := Max(s');
        t := maximum(x.qPrio, y);
    }
}

predicate validRS

失败说：“不允许表达式调用方法（Max）”。

我发现的解决方案使用了 Dafny 中的 Lambda 函数的概念。阅读文档后我很迷失。我已经在 Python 中使用了 Lambda 函数并从概念上理解了它，但我未能将它用于我的目的。

此外，如果我尝试将

Max

声明为

function method

，IDE 会抱怨

the phrase 'function method' is not allowed when using --function-syntax:4; to declare a compiled function, use just 'function'

Answer 1

在 Dafny 中，幽灵代码和非幽灵代码是有区别的。幽灵代码仅用于验证。非幽灵代码可以通过转译为其他语言（Rust、C# 等，如果是 Dafny）来运行。表达和陈述之间也有区别。

谓词体是表达式，而方法调用是语句。从 Dafny 的最新版本开始，谓词和函数可以在幽灵和非幽灵上下文中使用。两者都可以使用像 Ghost 谓词和 Ghost 函数这样的 Ghost 前缀，专门在 Ghost 上下文中使用。现在表达式不能使用像方法调用这样的语句。我认为这里不允许的原因是将幽灵和非幽灵上下文（函数）与非幽灵上下文（方法）分开。

如果您只关心验证，只需将所有内容转换为幽灵谓词和幽灵函数。

ghost function Max(s: set<Process>) : (t: nat)
  requires s != {} && validTS(s)
  ensures forall p :: p in s ==> p.qPrio <= t 
{
    var x :| x in s;
    if s == {x} then x.qPrio 
     else  
        var s' := s - {x};
        var y := Max(s');
        maximum(x.qPrio, y)
}

ghost predicate validRS(r: RSState, T: set<Process>)
    requires T != {} && validTS(T)
{
    r.cs.Keys == T && r.ceilingPrio == Max(T)
}