AuthenticationService.java

1 
package com.popx.servizio;
2
3 
import com.popx.modello.UserBean;
4 
import com.popx.persistenza.UserDAO;
5 
import com.popx.persistenza.UserDAOImpl;
6
7 
/*@ public invariant userDAO != null; @*/
8 
public class AuthenticationService {
9
10 
    private UserDAO userDAO;
11
12 
    /*@ ensures this.userDAO != null; @*/
13 
    public AuthenticationService() {
14 
        // Production / integration behavior (UNCHANGED)
15 
        this.userDAO = new UserDAOImpl();
16 
    }
17
18 
    /*@
19 
      @ requires userDAO != null;
20 
      @ ensures this.userDAO == userDAO;
21 
      @*/
22 
    public AuthenticationService(UserDAO userDAO) {
23 
        this.userDAO = userDAO;
24 
    }
25
26 
    /*@
27 
      @ public normal_behavior
28 
      @ requires email != null && !email.isEmpty();
29 
      @ requires password != null && !password.isEmpty();
30 
      @
31 
      @ ensures \result != null ==>
32 
      @      (\result.getEmail().equals(email));
33 
      @
34 
      @ signals (Exception e)
35 
      @      e.getMessage().equals("Invalid credentials");
36 
      @*/
37 
    public UserBean login(String email, String password) throws Exception {
38 
        UserBean user = userDAO.getUserByEmail(email);
39
40 2 1. login : negated conditional → KILLED
2. login : negated conditional → KILLED
 
        if (user != null && SecurityService.checkPassword(password, user.getPassword())) {
41 1 1. login : replaced return value with null for com/popx/servizio/AuthenticationService::login → KILLED
 
            return user;
42 
        }
43 
        throw new Exception("Invalid credentials");
44 
    }
45
46 
    /*@
47 
      @ public normal_behavior
48 
      @ requires user != null;
49 
      @ requires user.getEmail() != null && !user.getEmail().isEmpty();
50 
      @
51 
      @ ensures \result == true || \result == false;
52 
      @ signals (Exception e)
53 
      @      e.getMessage().equals("User already exists");
54 
      @*/
55 
    public boolean registerUser(UserBean user) throws Exception {
56 1 1. registerUser : negated conditional → KILLED
 
        if (userDAO.getUserByEmail(user.getEmail()) == null) {
57 2 1. registerUser : replaced boolean return with true for com/popx/servizio/AuthenticationService::registerUser → SURVIVED
2. registerUser : replaced boolean return with false for com/popx/servizio/AuthenticationService::registerUser → KILLED
 
            return userDAO.saveUser(user);
58 
        }
59 
        throw new Exception("User already exists");
60 
    }
61
62 
    /*@
63 
      @ public normal_behavior
64 
      @ requires email != null && !email.isEmpty();
65 
      @ ensures \result == true || \result == false;
66 
      @ signals (Exception) true;
67 
      @*/
68 
    public boolean isEmailRegistered(String email) throws Exception {
69 2 1. isEmailRegistered : negated conditional → KILLED
2. isEmailRegistered : replaced boolean return with true for com/popx/servizio/AuthenticationService::isEmailRegistered → KILLED
 
        return userDAO.getUserByEmail(email) != null;
70 
    }
71
72 
    /*@
73 
      @ public normal_behavior
74 
      @ requires email != null && !email.isEmpty();
75 
      @ ensures \result != null;
76 
      @ ensures \result.equals( userDAO.getUserByEmail(email).getRole() );
77 
      @ signals (Exception) true;
78 
      @*/
79 
    public String retrieveRole(String email) throws Exception {
80 
        UserBean user = userDAO.getUserByEmail(email);
81 1 1. retrieveRole : replaced return value with "" for com/popx/servizio/AuthenticationService::retrieveRole → KILLED
 
        return user.getRole();
82 
    }
83 
}

Mutations

40

1.1
Location : login
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:login_userNotFound_throwsException()] negated conditional → KILLED

2.2
Location : login
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:login_wrongPassword_throwsException()] negated conditional → KILLED
41

1.1
Location : login
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:login_successful()] replaced return value with null for com/popx/servizio/AuthenticationService::login → KILLED
56

1.1
Location : registerUser
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:registerUser_successful()] negated conditional → KILLED
57

1.1
Location : registerUser
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:registerUser_successful()] replaced boolean return with false for com/popx/servizio/AuthenticationService::registerUser → KILLED

2.2
Location : registerUser
Killed by : none replaced boolean return with true for com/popx/servizio/AuthenticationService::registerUser → SURVIVED
69

1.1
Location : isEmailRegistered
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:isEmailRegistered_userDoesNotExist_returnsFalse()] negated conditional → KILLED

2.2
Location : isEmailRegistered
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:isEmailRegistered_userDoesNotExist_returnsFalse()] replaced boolean return with true for com/popx/servizio/AuthenticationService::isEmailRegistered → KILLED
81

1.1
Location : retrieveRole
Killed by : com.popx.unit.servizio.AuthenticationServiceTest.[engine:junit-jupiter]/[class:com.popx.unit.servizio.AuthenticationServiceTest]/[method:retrieveRole_userExists_returnsRole()] replaced return value with "" for com/popx/servizio/AuthenticationService::retrieveRole → KILLED

Active mutators

Tests examined


Report generated by PIT 1.15.2