dafny 다른 클래스의 회원 값을 확인하는 방법

Question

나는 dafny를 배우려고 노력 중이며 이해가 안되는 문제를 발견했습니다. 사용자가 배열에 존재하는지 확인해야하며이를 위해 술어를 사용하고 싶습니다. 사용자 배열이 있고 각 사용자마다 ID가 있습니다. 그래서 User 클래스에 속한 ID를 확인하고 싶습니다.

나는 다른 건 다 잘 작동 Test.dfy(57,24): Error: member id does not exist in array type array

은 (내가 생각하는)이 오류를 얻을.

그럼 개체 배열 (사용자)이있을 때 술어에서 다른 클래스의 멤버를 읽거나 액세스하려면 어떻게해야합니까?

도움 주셔서 감사합니다. users가 배열이며, 배열은 id 필드를 가지고 있지 않기 때문에 `

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; 
    } 
} 

Answer 1

문제는 reads 절 this.users`id의 일부입니다.

reads 절의이 부분은 전혀 필요하지 않습니다. 그냥 삭제하십시오. 그러면 프로그램에서 확인하기 전에 몇 가지 다른 문제를 해결해야합니다.