Что проверяет код вне класса Dafny, но не в инкапсулированном виде?

Question

Некоторый код, который проверяет вне класса Dafny, не может быть проверен при инкапсуляции. Мне интересно (1) почему и (2) как получить лучшее из обоих миров: инкапсуляция / абстракция и проверка. Код моделирует "отношение" как пару: набор доменов и набор пар над набором доменов. Две версии представлены ниже. Первое подтверждает, второе нет.

Код определяет условие достоверности, которое требует, чтобы пары в наборе пар действительно находились над доменом. Он определяет предикат isFunction, который возвращает true, если моделируемое "отношение" однозначно. Это предикат, который проверяет в одном случае, но не в другом. Затем код в подпрограмме Main проверяет, что ( dom = {1,2,3,4}, pair = { (1,1), (2,2), (3,3), (4,4) }) является однозначным (функция). Однако, когда я инкапсулирую наборы доменов и пар в классе и создаю предикаты в функциях-членах, тот же код в Main больше не проверяет.

НЕЗАВИСИМАЯ ВЕРСИЯ:

/*
Represent a finite binary relation on a set, S, 
as a pair: the set S and a set of pairs (to be
drawn from S)
*/ 
type relationS<T> = (set<T>,set<(T,T)>)


/*
A de-facto Valid() predicate that checks that that each 
value in each pair in pairs is a member ofthe domain set.
*/
function method relS<T(!new)>(dom: set<T>, pairs: set<(T,T)>): 
relationS<T> 
    requires forall x, y :: (x, y) in pairs ==> x in dom && y in dom
{
    (dom, pairs)
}

/*
Projection function: Given a relation on S, return its co/domain set.
*/
function method domS<T>(r: relationS<T>): set<T>
{
    r.0
}

/*
Projection function: Given a relation on S, return its set of pairs.
*/
function method pairsS<T>(r: relationS<T>): set<(T,T)>
{
    r.1
}

/*
Return true iff the relation is single-valued (a function)
*/
predicate isFunctionS<T>(r: relationS<T>)
{
  forall x, y, z :: x in domS(r) && y in domS(r) && z in domS(r) &&
                    (x, y) in pairsS(r) && 
                    (x, z) in pairsS(r) ==> 
                    y == z  
}

method Main()
{
    var d := {1, 2, 3, 4};
    var h := { (1,1), (2,2), (3,3), (4,4) };
    var r1 := relS(d,h);
    assert isFunctionS(r1);        // Verifies
}

ENCAPSULAT VERSION (извините за немного другие идентификаторы)

/*
Abstraction of a finite binary relation on a 
set, S. Underlying representation is a pair: 
the domain set, S, and a set of pairs over S.
*/ 
class binRelationS<T(!new,==)>
{
    var d: set<T>;
    var p: set<(T,T)>;
    predicate Valid()
        reads this;
    {
        forall x, y :: (x, y) in p ==> x in d && y in d
    }

    /*
    Constructor requires that all values appearing in 
    any of the pairs in p be in d. That is, the pairs
    in p must represent a relation on domain, d.
    */
    constructor(dom: set<T>, pairs: set<(T,T)>)
        requires forall x, y :: 
            (x, y) in pairs ==> x in dom && y in dom;
        ensures Valid();
    {
        d := dom;
        p := pairs;
    }

    function method dom(): set<T>
        requires Valid();
        reads this;
        ensures Valid();
    {
        d
    }

    function method rel(): set<(T,T)>
        requires Valid();
        reads this
        ensures Valid();
    {
        p
    }

    /*
    Return true iff the relation is single-valued (a function)
    */
    predicate isFunction()
        requires Valid();
        reads this;
        ensures Valid();
    {
        forall x, y, z :: 
            x in d && y in d && z in d &&
            (x, y) in p && (x, z) in p ==> 
            y == z  
    }
}

method Main()
{
    var d := {1, 2, 3, 4};
    var h := { (1,1), (2,2), (3,3), (4,4) };
    var r := new binRelationS(d,h);
    assert r.isFunction();          // assertion violation
}

Answer 1

Вы просто пропускаете постусловие из конструктора.

ensures d == dom && p == pairs

Это необходимо, поскольку, как и методы, тела конструкторов не открываются вызывающим. Так Main понятия не имеет, что делает конструктор, кроме того, что указано в его спецификации.