-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathData.java
More file actions
60 lines (51 loc) · 1.55 KB
/
Copy pathData.java
File metadata and controls
60 lines (51 loc) · 1.55 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
public interface Data<E> {
/**
* Overview: Contenitore di un parametro generico con associate descrizione, autore e insieme degli amici
* che hanno inserito un like
*
* TE: <element, friends, numLikes>,
* element != null &&
* friends = { friend_1, friend_2, ..., friends_getLikes() } &&
* likes = #friends
*/
// Mofica il valore di el
/**
*
* @param el, el != null
* @throws NullPointerException if el = null
* @modifies this.element
* @effects post(this.element) = el
*
*/
public void updateData(E el);
// Restituisce il valore dell'elemento
/**
*
* @return element
*/
public E getData();
// Restituisce il numero di like associati al dato
/**
*
* @return this.likes
*/
public int getLikes();
// Stampa il valore di element
/**
*
* @effects stampa in formato stringa element
*/
public void Display();
/**
* @param friend t.c. forall i = 1, ..., getLikes() | friend_i != friend
* @throws DuplicateLikeException if exist i = 1, ..., getLikes() | friend_i = friend
* @modifies this.likes && this.friends
* @effects post(this.likes) = this.likes + 1 && post(this.friends) = pre(this.friends) U friend
*/
public void insertLike(String friend) throws NullPointerException, DuplicateLikeException;
/**
*
* @return una deep copy di this
*/
public Data<E> cloneData();
}