UserBean.java

1 
package com.popx.modello;
2
3 
import java.io.Serializable;
4
5 
/*@
6 
  @ invariant username == null || !username.isEmpty();
7
8 
  @ invariant email == null
9 
      || (!email.isEmpty()
10 
          && email.contains("@")
11 
          && email.indexOf('@') > 0
12 
          && email.substring(email.indexOf('@') + 1).contains(".")
13 
          && email.indexOf('.') > email.indexOf('@') + 1
14 
          && email.lastIndexOf('.') < email.length() - 1);
15
16 
  @ invariant password == null
17 
      || (password.length() >= 8
18 
          && password.length() <= 16
19 
          && (\exists int i; 0 <= i && i < password.length();
20 
                Character.isLowerCase(password.charAt(i)))
21 
          && (\exists int i; 0 <= i && i < password.length();
22 
                Character.isUpperCase(password.charAt(i)))
23 
          && (\exists int i; 0 <= i && i < password.length();
24 
                Character.isDigit(password.charAt(i))));
25
26 
  @ invariant role == null
27 
      || role.equals("Gestore")
28 
      || role.equals("User")
29 
      || role.equals("Admin");
30 
@*/
31 
public class UserBean implements Serializable {
32
33 
    private String username;
34 
    private String email;
35 
    private String password;
36 
    private String role;
37
38 
    /*@
39 
      @ ensures this.username == null
40 
      @      && this.email == null
41 
      @      && this.password == null
42 
      @      && this.role == null;
43 
    @*/
44 
    public UserBean() {}
45
46 
    /*@
47 
      @ requires username != null && !username.isEmpty();
48
49 
      @ requires email != null;
50 
      @ requires !email.isEmpty();
51 
      @ requires email.contains("@");
52 
      @ requires email.indexOf('@') > 0;
53 
      @ requires email.substring(email.indexOf('@') + 1).contains(".");
54 
      @ requires email.indexOf('.') > email.indexOf('@') + 1;
55 
      @ requires email.lastIndexOf('.') < email.length() - 1;
56
57 
      @ requires password != null;
58 
      @ requires password.length() >= 8 && password.length() <= 16;
59 
      @ requires (\exists int i; 0 <= i && i < password.length();
60 
                    Character.isLowerCase(password.charAt(i)));
61 
      @ requires (\exists int i; 0 <= i && i < password.length();
62 
                    Character.isUpperCase(password.charAt(i)));
63 
      @ requires (\exists int i; 0 <= i && i < password.length();
64 
                    Character.isDigit(password.charAt(i)));
65
66 
      @ requires role != null;
67 
      @ requires role.equals("Gestore")
68 
             || role.equals("User")
69 
             || role.equals("Admin");
70
71 
      @ ensures this.username.equals(username)
72 
      @      && this.email.equals(email)
73 
      @      && this.password.equals(password)
74 
      @      && this.role.equals(role);
75 
    @*/
76 
    public UserBean(String username, String email, String password, String role) {
77 
        this.username = username;
78 
        this.email = email;
79 
        this.password = password;
80 
        this.role = role;
81 
    }
82
83 
    /*@ ensures \result == username; @*/
84 1 1. getUsername : replaced return value with "" for com/popx/modello/UserBean::getUsername → KILLED
 
    public String getUsername() { return username; }
85
86 
    /*@
87 
      @ requires username != null && !username.isEmpty();
88 
      @ ensures this.username.equals(username);
89 
    @*/
90 
    public void setUsername(String username) { this.username = username; }
91
92 
    /*@ ensures \result == email; @*/
93 1 1. getEmail : replaced return value with "" for com/popx/modello/UserBean::getEmail → KILLED
 
    public String getEmail() { return email; }
94
95 
    /*@
96 
      @ requires email != null;
97 
      @ requires !email.isEmpty();
98 
      @ requires email.contains("@");
99 
      @ requires email.indexOf('@') > 0;
100 
      @ requires email.substring(email.indexOf('@') + 1).contains(".");
101 
      @ requires email.indexOf('.') > email.indexOf('@') + 1;
102 
      @ requires email.lastIndexOf('.') < email.length() - 1;
103 
      @ ensures this.email.equals(email);
104 
    @*/
105 
    public void setEmail(String email) { this.email = email; }
106
107 
    /*@ ensures \result == password; @*/
108 1 1. getPassword : replaced return value with "" for com/popx/modello/UserBean::getPassword → KILLED
 
    public String getPassword() { return password; }
109
110 
    /*@
111 
      @ requires password != null;
112 
      @ requires password.length() >= 8 && password.length() <= 16;
113 
      @ requires (\exists int i; 0 <= i && i < password.length();
114 
                    Character.isLowerCase(password.charAt(i)));
115 
      @ requires (\exists int i; 0 <= i && i < password.length();
116 
                    Character.isUpperCase(password.charAt(i)));
117 
      @ requires (\exists int i; 0 <= i && i < password.length();
118 
                    Character.isDigit(password.charAt(i)));
119 
      @ ensures this.password.equals(password);
120 
    @*/
121 
    public void setPassword(String password) { this.password = password; }
122
123 
    /*@ ensures \result == role; @*/
124 1 1. getRole : replaced return value with "" for com/popx/modello/UserBean::getRole → KILLED
 
    public String getRole() { return role; }
125
126 
    /*@
127 
      @ requires role != null;
128 
      @ requires role.equals("Gestore")
129 
             || role.equals("User")
130 
             || role.equals("Admin");
131 
      @ ensures this.role.equals(role);
132 
    @*/
133 
    public void setRole(String role) { this.role = role; }
134 
}

Mutations

84

1.1
Location : getUsername
Killed by : com.popx.unit.modello.GestoreOrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.GestoreOrdineBeanTest]/[method:defaultConstructor_setsFieldsToNull()] replaced return value with "" for com/popx/modello/UserBean::getUsername → KILLED
93

1.1
Location : getEmail
Killed by : com.popx.unit.modello.GestoreOrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.GestoreOrdineBeanTest]/[method:defaultConstructor_setsFieldsToNull()] replaced return value with "" for com/popx/modello/UserBean::getEmail → KILLED
108

1.1
Location : getPassword
Killed by : com.popx.unit.modello.GestoreOrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.GestoreOrdineBeanTest]/[method:defaultConstructor_setsFieldsToNull()] replaced return value with "" for com/popx/modello/UserBean::getPassword → KILLED
124

1.1
Location : getRole
Killed by : com.popx.unit.modello.GestoreOrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.GestoreOrdineBeanTest]/[method:defaultConstructor_setsFieldsToNull()] replaced return value with "" for com/popx/modello/UserBean::getRole → KILLED

Active mutators

Tests examined


Report generated by PIT 1.15.2