CarrelloBean.java

1 
package com.popx.modello;
2
3 
import java.util.List;
4
5 
/*@
6 
  @ public invariant clienteEmail == null
7 
  @                 || !clienteEmail.isEmpty();
8 
  @
9 
  @ public invariant prodottiCarrello == null
10 
  @                 || (\forall int i;
11 
  @                        0 <= i && i < prodottiCarrello.size();
12 
  @                        prodottiCarrello.get(i) != null);
13 
  @*/
14 
public class CarrelloBean {
15
16 
    private String clienteEmail;
17 
    private List<ProdottoCarrelloBean> prodottiCarrello;
18
19 
    /*@
20 
      @ ensures this.clienteEmail == null;
21 
      @ ensures this.prodottiCarrello == null;
22 
      @*/
23 
    public CarrelloBean() {}
24
25 
    /*@
26 
      @ requires clienteEmail != null && !clienteEmail.isEmpty();
27 
      @ requires prodottiCarrello != null;
28 
      @ requires (\forall int i;
29 
      @              0 <= i && i < prodottiCarrello.size();
30 
      @              prodottiCarrello.get(i) != null);
31 
      @
32 
      @ ensures this.clienteEmail == clienteEmail;
33 
      @ ensures this.prodottiCarrello == prodottiCarrello;
34 
      @*/
35 
    public CarrelloBean(String clienteEmail, List<ProdottoCarrelloBean> prodottiCarrello) {
36 
        this.clienteEmail = clienteEmail;
37 
        this.prodottiCarrello = prodottiCarrello;
38 
    }
39
40 
    /*@ ensures \result == clienteEmail; @*/
41 
    public String getClienteEmail() {
42 1 1. getClienteEmail : replaced return value with "" for com/popx/modello/CarrelloBean::getClienteEmail → KILLED
 
        return clienteEmail;
43 
    }
44
45 
    /*@
46 
      @ requires clienteEmail != null && !clienteEmail.isEmpty();
47 
      @ ensures this.clienteEmail == clienteEmail;
48 
      @*/
49 
    public void setClienteEmail(String clienteEmail) {
50 
        this.clienteEmail = clienteEmail;
51 
    }
52
53 
    /*@ ensures \result == prodottiCarrello; @*/
54 
    public List<ProdottoCarrelloBean> getProdottiCarrello() {
55 1 1. getProdottiCarrello : replaced return value with Collections.emptyList for com/popx/modello/CarrelloBean::getProdottiCarrello → KILLED
 
        return prodottiCarrello;
56 
    }
57
58 
    /*@
59 
      @ requires prodottiCarrello != null;
60 
      @ requires (\forall int i;
61 
      @              0 <= i && i < prodottiCarrello.size();
62 
      @              prodottiCarrello.get(i) != null);
63 
      @ ensures this.prodottiCarrello == prodottiCarrello;
64 
      @*/
65 
    public void setProdottiCarrello(List<ProdottoCarrelloBean> prodottiCarrello) {
66 
        this.prodottiCarrello = prodottiCarrello;
67 
    }
68 
}

Mutations

42

1.1
Location : getClienteEmail
Killed by : com.popx.unit.modello.CarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.CarrelloBeanTest]/[method:carrelloBean_gettersAndSetters_workCorrectly()] replaced return value with "" for com/popx/modello/CarrelloBean::getClienteEmail → KILLED
55

1.1
Location : getProdottiCarrello
Killed by : com.popx.unit.modello.CarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.CarrelloBeanTest]/[method:carrelloBean_gettersAndSetters_workCorrectly()] replaced return value with Collections.emptyList for com/popx/modello/CarrelloBean::getProdottiCarrello → KILLED

Active mutators

Tests examined


Report generated by PIT 1.15.2