求助：Dafny递归遍历链表时reads子句引发的错误如何解决

问题根源 #

你遇到的insufficient reads clause错误，是因为list_corresponds的reads子句仅声明了读取当前l节点和它的tk字段，但递归调用list_corresponds(s[1..], l.next)时，需要访问l.next节点及其tk字段，这些对象不在当前声明的读取集合中，Dafny的堆检查机制因此报错。

解决方案 #

修改list_corresponds的reads子句，使其覆盖从l出发通过next链可达的所有TokenList节点，以及每个节点的tk字段。利用Dafny的传递闭包语法l.*.next可以简洁地表示所有后续节点，再加上当前节点和所有节点的tk字段，就能满足递归遍历的读取需求。

修改后的完整代码 #

datatype TokenType =
    TokenNumber |
    TokenPlus   |
    TokenMinus  |
    TokenTimes  |
    TokenDivide |
    TokenLbrac  |
    TokenRbrac  |
    TokenError

class Token
{
    var c: char;
    var typ: TokenType;
    constructor (cc: char, t: TokenType)
        ensures c == cc && t == typ
    { 
        c := cc; typ := t; 
    }
}

predicate corresponds(c: char, token: Token)
    reads token
{
    c == token.c && (
        (token.typ == TokenNumber && '0' <= c && c <= '9') ||
        (token.typ == TokenPlus   && c == '+') ||
        (token.typ == TokenMinus  && c == '-') ||
        (token.typ == TokenTimes  && c == '*') ||
        (token.typ == TokenDivide && c == '/') ||
        (token.typ == TokenLbrac  && c == '(') ||
        (token.typ == TokenRbrac  && c == ')')
    )
}

class TokenList
{
    var tk: Token;
    var next: TokenList;
    var eol: bool;
    constructor (token: Token, l: TokenList, end: bool)
        ensures tk == token && next == l && eol == end
    {
        tk := token; next := l; eol := end;
    }
}

predicate list_corresponds(s: string, l: TokenList)
    // 修改此处的reads子句，覆盖整个链表的节点和对应的tk字段
    reads l, l.*.next, l.*.tk
    decreases s
{
    if |s| == 0 then
        l.eol
    else
        assert |s| > 0;
        if s[0] == ' ' then
            false
        else
            corresponds(s[0], l.tk) && list_corresponds(s[1..], l.next)
}

补充说明 #

• l.*.next是Dafny的传递闭包语法，表示从l出发，通过next字段能到达的所有TokenList实例（包括l.next、l.next.next等）。
• 加上l是为了覆盖当前节点本身，l.*.tk则覆盖所有可达节点的tk字段，确保递归调用时每一层的读取操作都被合法声明。
• 改为可空类型无法解决问题，因为核心矛盾是读取的堆对象未被声明，和是否可空无关。

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