ProdottoCarrelloBean.java

1 
package com.popx.modello;
2
3 
/*@
4 
  @ public invariant clienteEmail == null || !clienteEmail.isEmpty();
5 
  @ public invariant prodottoId == null || !prodottoId.isEmpty();
6 
  @ public invariant quantity >= 0;
7 
  @ public invariant unitaryCost >= 0;
8 
@*/
9 
public class ProdottoCarrelloBean {
10
11 
    private String clienteEmail;
12 
    private String prodottoId;
13 
    private int quantity;
14 
    private float unitaryCost;
15
16 
    /*@
17 
      @ ensures this.clienteEmail == null;
18 
      @ ensures this.prodottoId == null;
19 
      @ ensures this.quantity == 0;
20 
      @ ensures this.unitaryCost == 0.0f;
21 
    @*/
22 
    public ProdottoCarrelloBean() {}
23
24 
    /*@
25 
      @ requires clienteEmail != null && !clienteEmail.isEmpty();
26 
      @ requires prodottoId != null && !prodottoId.isEmpty();
27 
      @ requires quantity >= 0;
28 
      @ requires unitaryCost >= 0;
29 
      @ ensures this.clienteEmail == clienteEmail;
30 
      @ ensures this.prodottoId == prodottoId;
31 
      @ ensures this.quantity == quantity;
32 
      @ ensures this.unitaryCost == unitaryCost;
33 
    @*/
34 
    public ProdottoCarrelloBean(String clienteEmail, String prodottoId, int quantity, float unitaryCost) {
35 
        this.clienteEmail = clienteEmail;
36 
        this.prodottoId = prodottoId;
37 
        this.quantity = quantity;
38 
        this.unitaryCost = unitaryCost;
39 
    }
40
41 
    /*@ ensures \result == clienteEmail; @*/
42 
    public String getClienteEmail() {
43 1 1. getClienteEmail : replaced return value with "" for com/popx/modello/ProdottoCarrelloBean::getClienteEmail → KILLED
 
        return clienteEmail;
44 
    }
45
46 
    /*@
47 
      @ requires clienteEmail != null && !clienteEmail.isEmpty();
48 
      @ ensures this.clienteEmail == clienteEmail;
49 
    @*/
50 
    public void setClienteEmail(String clienteEmail) {
51 
        this.clienteEmail = clienteEmail;
52 
    }
53
54 
    /*@ ensures \result == prodottoId; @*/
55 
    public String getProdottoId() {
56 1 1. getProdottoId : replaced return value with "" for com/popx/modello/ProdottoCarrelloBean::getProdottoId → KILLED
 
        return prodottoId;
57 
    }
58
59 
    /*@
60 
      @ requires prodottoId != null && !prodottoId.isEmpty();
61 
      @ ensures this.prodottoId == prodottoId;
62 
    @*/
63 
    public void setProdottoId(String prodottoId) {
64 
        this.prodottoId = prodottoId;
65 
    }
66
67 
    /*@ ensures \result == quantity; @*/
68 
    public int getQuantity() {
69 1 1. getQuantity : replaced int return with 0 for com/popx/modello/ProdottoCarrelloBean::getQuantity → KILLED
 
        return quantity;
70 
    }
71
72 
    /*@
73 
      @ requires quantity >= 0;
74 
      @ ensures this.quantity == quantity;
75 
    @*/
76 
    public void setQuantity(int quantity) {
77 
        this.quantity = quantity;
78 
    }
79
80 
    /*@ ensures \result == unitaryCost; @*/
81 
    public float getUnitaryCost() {
82 1 1. getUnitaryCost : replaced float return with 0.0f for com/popx/modello/ProdottoCarrelloBean::getUnitaryCost → KILLED
 
        return unitaryCost;
83 
    }
84
85 
    /*@
86 
      @ requires unitaryCost >= 0;
87 
      @ ensures this.unitaryCost == unitaryCost;
88 
    @*/
89 
    public void setUnitaryCost(float unitaryCost) {
90 
        this.unitaryCost = unitaryCost;
91 
    }
92 
}

Mutations

43

1.1
Location : getClienteEmail
Killed by : com.popx.unit.modello.ProdottoCarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoCarrelloBeanTest]/[method:defaultConstructor_initialValues()] replaced return value with "" for com/popx/modello/ProdottoCarrelloBean::getClienteEmail → KILLED
56

1.1
Location : getProdottoId
Killed by : com.popx.unit.modello.ProdottoCarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoCarrelloBeanTest]/[method:defaultConstructor_initialValues()] replaced return value with "" for com/popx/modello/ProdottoCarrelloBean::getProdottoId → KILLED
69

1.1
Location : getQuantity
Killed by : com.popx.unit.modello.ProdottoCarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoCarrelloBeanTest]/[method:parameterizedConstructor_setsFieldsCorrectly()] replaced int return with 0 for com/popx/modello/ProdottoCarrelloBean::getQuantity → KILLED
82

1.1
Location : getUnitaryCost
Killed by : com.popx.unit.modello.ProdottoCarrelloBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoCarrelloBeanTest]/[method:parameterizedConstructor_setsFieldsCorrectly()] replaced float return with 0.0f for com/popx/modello/ProdottoCarrelloBean::getUnitaryCost → KILLED

Active mutators

Tests examined


Report generated by PIT 1.15.2