Дафни - пропагандистская оговорка?

Question

У меня проблема в том, что два разных метода в двух разных классах не взаимодействуют, установка выглядит следующим образом:

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 обеспечивает его предварительное условие? Если это ограничение для проверяющего Дафни, как бы я решил эту проблему?

Изменить: перепутал синтаксис, когда я создавал этот пример, поэтому тестовая программа работает. Настоящий, однако, все еще имеет проблемы. Конкретный класс, с которым я борюсь, упомянут ниже:

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