1

我正在尝试学习 dafny，但遇到了一个我不明白的问题。我需要检查用户是否存在于数组中，并且我想为此使用谓词。我有一组用户，每个用户都有一个 ID。所以我想检查属于 User 类的 id。

我收到这个错误Test.dfy(57,24): Error: member id does not exist in array type array

其他一切都很好（我认为）。

那么当我有一个对象数组（用户）时，如何读取/访问谓词中另一个类的成员？

谢谢您的帮助。`

class Test {

    var users : array<User>;
    var size : int;
    var index : int;

    method Init(c : int)
    modifies this;   
    requires c > 0;
    ensures fresh(users);   
    ensures size == c; 
    ensures Check();
    ensures Empty();

{
    users := new User[c];   
    size := c;    
    index := -1;        
}

predicate Empty()
reads this`index;
{
    index == -1
}

predicate Full()
reads this`index, this`size;
{
    index == (size - 1)
}

predicate Check()
reads this;
{
    users != null && 
    size > 0 && 
    size == users.Length && 
    index >= -1 && 
    index < size 
}

method AddUser(u : User)
modifies this.users, this`index;
requires Check();
requires !Full();

ensures Check();
ensures index == old(index) + 1;
ensures users[index] == u;
{
    index := index + 1;   
    users[index] := u; 
}

predicate FindUserById(n : int)
reads this.users, this.users`id;
requires Check();
{
    exists i :: 0 <= i < users.Length ==> users[i].id == n
}

method Main()
{
    var t := new Test;
    t.Init(3);
    var u1 := new User.Init(1,23);
    var u2 := new User.Init(2,24);
    var u3 := new User.Init(3,25);
    t.AddUser(u1);
    t.AddUser(u2);
    t.AddUser(u3);
}
}

class User {

   var id : int;
   var phone : int;

   method Init(i : int, p : int)
   modifies this`id, this`phone;
   requires 0 < i < 99999;
   requires 0 < p < 99999;
   ensures id == i;
   ensures phone == p;
   {
        id := i;
        phone := p;
   }
}
4

1 回答 1

0

问题是reads子句的一部分this.users`id，因为users它是一个数组，而数组没有id字段。

您根本不需要这部分reads条款；只是删除它。然后，您必须在程序验证之前修复一些其他问题。

于 2017-12-01T20:44:13.593 回答