MagliettaOrdine.java

1 
package model.maglietta;
2
3 
public class MagliettaOrdine {
4 
    /*@ public invariant magliettaBean != null;
5 
      @ public invariant quantita >= 1;
6 
      @ public invariant
7 
      @ taglia != null ==> (taglia.equals("XS") || taglia.equals("S") || taglia.equals("M")
8 
      @     || taglia.equals("L") || taglia.equals("XL") || taglia.equals("XXL"));
9 
      @*/
10 
    private /*@ spec_public @*/ MagliettaBean magliettaBean;
11 
    private /*@ spec_public @*/ int quantita;
12 
    private /*@ spec_public @*/ String taglia;
13
14 
    /*@ public normal_behavior
15 
      @ requires magliettaBean != null;
16 
      @ requires taglia != null;
17 
      @ requires taglia.equals("XS") || taglia.equals("S") || taglia.equals("M")
18 
      @     || taglia.equals("L") || taglia.equals("XL") || taglia.equals("XXL");
19 
      @ ensures this.magliettaBean == magliettaBean;
20 
      @ ensures this.taglia == taglia;
21 
      @ ensures this.quantita == 1;
22 
      @*/
23 
    public MagliettaOrdine(MagliettaBean magliettaBean, String taglia) {
24 
        this.magliettaBean = magliettaBean;
25 
        this.taglia = taglia;
26 
        quantita = 1;
27 
    }
28
29 
    /*@ public normal_behavior
30 
      @ ensures \result == magliettaBean;
31 
      @ pure
32 
      @*/
33 
    public /*@ non_null @*/ MagliettaBean getMagliettaBean() {
34 1 1. getMagliettaBean : replaced return value with null for model/maglietta/MagliettaOrdine::getMagliettaBean → KILLED
 
        return magliettaBean;
35 
    }
36
37 
    /*@ public normal_behavior
38 
      @ requires magliettaBean != null;
39 
      @ assignable this.magliettaBean;
40 
      @ ensures this.magliettaBean == magliettaBean;
41 
      @*/
42 
    public void setMagliettaBean(/*@ non_null @*/ MagliettaBean magliettaBean) {
43 
        this.magliettaBean = magliettaBean;
44 
    }
45
46 
    /*@ public normal_behavior
47 
      @ ensures \result == taglia;
48 
      @ pure
49 
      @*/
50 
    public /*@ non_null @*/ String getTaglia() {
51 1 1. getTaglia : replaced return value with "" for model/maglietta/MagliettaOrdine::getTaglia → KILLED
 
        return taglia;
52 
    }
53
54 
    /*@ public normal_behavior
55 
      @ requires taglia != null;
56 
      @ requires taglia.equals("XS") || taglia.equals("S") || taglia.equals("M")
57 
      @     || taglia.equals("L") || taglia.equals("XL") || taglia.equals("XXL");
58 
      @ assignable this.taglia;
59 
      @ ensures this.taglia == taglia;
60 
      @*/
61 
    public void setTaglia(/*@ non_null @*/ String taglia) {
62 
        this.taglia = taglia;
63 
    }
64
65 
    /*@ public normal_behavior
66 
      @ ensures \result == quantita;
67 
      @ pure
68 
      @*/
69 
    public int getQuantita() {
70 1 1. getQuantita : replaced int return with 0 for model/maglietta/MagliettaOrdine::getQuantita → KILLED
 
        return quantita;
71 
    }
72
73 
    /*@ public normal_behavior
74 
      @ requires quantita >= 1;
75 
      @ assignable this.quantita;
76 
      @ ensures this.quantita == quantita;
77 
      @*/
78 
    public void setQuantita(int quantita) {
79 
        this.quantita = quantita;
80 
    }
81
82 
    /*@ public normal_behavior
83 
      @ requires this.quantita < Integer.MAX_VALUE;
84 
      @ assignable this.quantita;
85 
      @ ensures this.quantita == \old(this.quantita) + 1;
86 
      @*/
87 
    public void incrementaQuantita() {
88 1 1. incrementaQuantita : Replaced integer addition with subtraction → KILLED
 
        quantita++;
89 
    }
90
91 
    /*@ public normal_behavior
92 
      @ requires this.quantita > 1;
93 
      @ assignable this.quantita;
94 
      @ ensures this.quantita == \old(this.quantita) - 1;
95 
      @*/
96 
    public void decremenetaQuantita() {
97 1 1. decremenetaQuantita : Replaced integer subtraction with addition → KILLED
 
        quantita--;
98 
    }
99
100 
    /*@ public normal_behavior
101 
      @ requires magliettaBean.getPrezzo() >= 0.0f;
102 
      @ ensures \result == this.quantita * this.magliettaBean.getPrezzo();
103 
      @ ensures \result >= 0.0f;
104 
      @ pure
105 
      @*/
106 
    public float getPrezzoTotale() {
107 2 1. getPrezzoTotale : replaced float return with 0.0f for model/maglietta/MagliettaOrdine::getPrezzoTotale → KILLED
2. getPrezzoTotale : Replaced float multiplication with division → KILLED
 
        return quantita * magliettaBean.getPrezzo();
108 
    }
109 
}

Mutations

34

1.1
Location : getMagliettaBean
Killed by : model.CarrelloModelTest.[engine:junit-jupiter]/[class:model.CarrelloModelTest]/[method:rimuovi_idNonPresente_nessunaRimozione()] replaced return value with null for model/maglietta/MagliettaOrdine::getMagliettaBean → KILLED

51

1.1
Location : getTaglia
Killed by : model.CarrelloModelTest.[engine:junit-jupiter]/[class:model.CarrelloModelTest]/[method:rimuovi_presente_elimina()] replaced return value with "" for model/maglietta/MagliettaOrdine::getTaglia → KILLED

70

1.1
Location : getQuantita
Killed by : model.maglietta.MagliettaOrdineTest.[engine:junit-jupiter]/[class:model.maglietta.MagliettaOrdineTest]/[method:setQuantita_negativa_impostaValore()] replaced int return with 0 for model/maglietta/MagliettaOrdine::getQuantita → KILLED

88

1.1
Location : incrementaQuantita
Killed by : model.maglietta.MagliettaOrdineTest.[engine:junit-jupiter]/[class:model.maglietta.MagliettaOrdineTest]/[method:getPrezzoTotale_quantita2_prezzo10()] Replaced integer addition with subtraction → KILLED

97

1.1
Location : decremenetaQuantita
Killed by : model.maglietta.MagliettaOrdineTest.[engine:junit-jupiter]/[class:model.maglietta.MagliettaOrdineTest]/[method:decremenetaQuantita_da1_a0()] Replaced integer subtraction with addition → KILLED

107

1.1
Location : getPrezzoTotale
Killed by : model.maglietta.MagliettaOrdineTest.[engine:junit-jupiter]/[class:model.maglietta.MagliettaOrdineTest]/[method:getPrezzoTotale_quantita2_prezzo10()] replaced float return with 0.0f for model/maglietta/MagliettaOrdine::getPrezzoTotale → KILLED

2.2
Location : getPrezzoTotale
Killed by : model.maglietta.MagliettaOrdineTest.[engine:junit-jupiter]/[class:model.maglietta.MagliettaOrdineTest]/[method:getPrezzoTotale_quantita2_prezzo10()] Replaced float multiplication with division → KILLED

Active mutators

Tests examined


Report generated by PIT 1.22.0