1

某些在 Dafny 类之外进行验证的代码在封装时无法验证。我想知道（1）为什么，以及（2）如何两全其美：封装/抽象和验证。该代码将“关系”建模为一对：一个域集和域集上的一组对。下面介绍两个版本。第一个验证，第二个没有。

该代码定义了一个有效性条件，该条件要求对集中的对实际上在域上。它定义了一个谓词 isFunction，如果如此建模的“关系”是单值的，则返回 true。这是在一种情况下验证但在另一种情况下不验证的谓词。然后，在 Main 例程中的代码验证 ( dom = {1,2,3,4}, pairs = { (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
}

封装版本（抱歉标识符略有不同）

/*
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
}
4

1 回答 1

1

您只是缺少构造函数的后置条件。

ensures d == dom && p == pairs

这是必要的，因为与方法一样，构造函数的主体不会显示给调用者。所以Main除了规范中的内容外，不知道构造函数做了什么。

于 2018-02-28T16:33:18.370 回答