0

我遇到的问题是两个不同类中的两种不同方法不合作，设置如下：

class A{
    method b()
    ensures statement
    {
        // Do something
    }
}

class C{
    method d()
    requires statement
    {
        // Do something
    }
}

一个主要的称它们如下：

method Main(){
    var a: new A;
    var c: new C;

    a.b();
    c.d(); // Error: possible violation of function precondition
}

为什么方法d不承认方法b确保了它的前提条件？如果这是对 Dafny 证明者的限制，我将如何解决这个问题？

编辑： 当我创建这个例子时弄乱了语法，所以测试程序可以工作。然而，真正的仍然有问题。我正在努力解决的具体课程如下所述：

class TokenController{
        var database : map<int, Token>; 

        // Create a new token if one of the following is true:
        // * Token is null
        // * Invalid token
        //
        // Returns true if it was created, false otherwise.
        method createToken(key:int, securityLevel:int) returns (res: bool)
        modifies this`database;
        requires Defines.LOW() <= securityLevel <= Defines.HIGH();
        ensures key in database;
        ensures database[key] != null;
        ensures database[key].isValid;
        ensures old(key!in database) || old(database[key] == null) || old(!database[key].isValid) <==> res;
        {
            if(key !in database || database[key] == null || !database[key].isValid){
                var token := new Token.Token;
                token.init(key, securityLevel);
                // Add it to the map
                database := database[key:=token];
                res := true;
            }
            else{
                res := false;
            }
        }

        // Returns true if keyt matches the one in the database and the token is valid. Otherwise false.
        predicate method validToken(key:int)
        requires keyin database;
        requires database[key] != null;
        reads this`database;
        reads this.database[key];
        {
            database[key].fingerprint == key && database[key].isValid
        }
}

主要它被称为如下：

var tokenRes : bool;
tokenRes := tokenController.createToken(0, 0);
tokenRes := tokenController.validToken(0); //  Error: possible violation of function precondition
4

0 回答 0