ProdottoBean.java

1 
package com.popx.modello;
2
3 
import java.io.Serializable;
4 
import java.util.Arrays;
5
6 
public class ProdottoBean implements Serializable {
7 
    /*@ public invariant id != null && !id.isEmpty();
8 
      @ public invariant name != null && !name.isEmpty();
9 
      @ public invariant brand != null && !brand.isEmpty();
10 
      @ public invariant cost >= 0;
11 
      @ public invariant piecesInStock >= 0;
12 
      @ public invariant qty >= 0;
13 
      @ // img, figure e description possono essere null o vuote
14 
      @*/
15
16 
    private static final long serialVersionUID = 1L;
17
18 
    private String id;
19 
    private String name;
20 
    private String description;
21 
    private double cost;
22 
    private int piecesInStock;
23 
    private String brand;
24 
    private byte[] img;
25 
    private String figure;
26
27 
    private int qty;
28
29 
    // Constructors
30
31 
    /*@ ensures id == null && name == null && description == null && cost == 0.0
32 
      @      && piecesInStock == 0 && brand == null && img == null && figure == null
33 
      @      && qty == 0;
34 
      @*/
35 
    public ProdottoBean() {
36 
    }
37
38 
    /*@ requires id != null && !id.isEmpty();
39 
      @ requires name != null && !name.isEmpty();
40 
      @ requires brand != null && !brand.isEmpty();
41 
      @ requires cost >= 0;
42 
      @ requires piecesInStock >= 0;
43 
      @ // description, img, figure possono essere null
44 
      @ ensures this.id == id;
45 
      @ ensures this.name == name;
46 
      @ ensures this.description == description;
47 
      @ ensures this.cost == cost;
48 
      @ ensures this.piecesInStock == piecesInStock;
49 
      @ ensures this.brand == brand;
50 
      @ ensures this.img == img;
51 
      @ ensures this.figure == figure;
52 
      @*/
53 
    public ProdottoBean(String id, String name, String description, double cost, int piecesInStock, String brand, byte[] img, String figure) {
54 
        this.id = id;
55 
        this.name = name;
56 
        this.description = description;
57 
        this.cost = cost;
58 
        this.piecesInStock = piecesInStock;
59 
        this.brand = brand;
60 
        this.img = img;
61 
        this.figure = figure;
62 
    }
63
64 
    /*@ ensures \result == id; @*/
65 
    public String getId() {
66 1 1. getId : replaced return value with "" for com/popx/modello/ProdottoBean::getId → KILLED
 
        return id;
67 
    }
68
69 
    /*@ requires id != null && !id.isEmpty();
70 
      @ ensures this.id == id;
71 
      @*/
72 
    public void setId(String id) {
73 
        this.id = id;
74 
    }
75
76 
    /*@ ensures \result == name; @*/
77 
    public String getName() {
78 1 1. getName : replaced return value with "" for com/popx/modello/ProdottoBean::getName → KILLED
 
        return name;
79 
    }
80
81 
    /*@ requires name != null && !name.isEmpty();
82 
      @ ensures this.name == name;
83 
      @*/
84 
    public void setName(String name) {
85 
        this.name = name;
86 
    }
87
88 
    /*@ ensures \result == description; @*/
89 
    public String getDescription() {
90 1 1. getDescription : replaced return value with "" for com/popx/modello/ProdottoBean::getDescription → KILLED
 
        return description;
91 
    }
92
93 
    /*@ // description può essere null o vuota
94 
      @ ensures this.description == description;
95 
      @*/
96 
    public void setDescription(String description) {
97 
        this.description = description;
98 
    }
99
100 
    /*@ ensures \result == cost; @*/
101 
    public double getCost() {
102 1 1. getCost : replaced double return with 0.0d for com/popx/modello/ProdottoBean::getCost → KILLED
 
        return cost;
103 
    }
104
105 
    /*@ requires cost >= 0;
106 
      @ ensures this.cost == cost;
107 
      @*/
108 
    public void setCost(double cost) {
109 
        this.cost = cost;
110 
    }
111
112 
    /*@ ensures \result == piecesInStock; @*/
113 
    public int getPiecesInStock() {
114 1 1. getPiecesInStock : replaced int return with 0 for com/popx/modello/ProdottoBean::getPiecesInStock → KILLED
 
        return piecesInStock;
115 
    }
116
117 
    /*@ requires piecesInStock >= 0;
118 
      @ ensures this.piecesInStock == piecesInStock;
119 
      @*/
120 
    public void setPiecesInStock(int piecesInStock) {
121 
        this.piecesInStock = piecesInStock;
122 
    }
123
124 
    /*@ ensures \result == brand; @*/
125 
    public String getBrand() {
126 1 1. getBrand : replaced return value with "" for com/popx/modello/ProdottoBean::getBrand → KILLED
 
        return brand;
127 
    }
128
129 
    /*@ requires brand != null && !brand.isEmpty();
130 
      @ ensures this.brand == brand;
131 
      @*/
132 
    public void setBrand(String brand) {
133 
        this.brand = brand;
134 
    }
135
136 
    /*@ ensures \result == img; @*/
137 
    public byte[] getImg() {
138 1 1. getImg : replaced return value with null for com/popx/modello/ProdottoBean::getImg → KILLED
 
        return img;
139 
    }
140
141 
    /*@ // img può essere null
142 
      @ ensures this.img == img;
143 
      @*/
144 
    public void setImg(byte[] img) {
145 
        this.img = img;
146 
    }
147
148 
    /*@ ensures \result == figure; @*/
149 
    public String getFigure() {
150 1 1. getFigure : replaced return value with "" for com/popx/modello/ProdottoBean::getFigure → KILLED
 
        return figure;
151 
    }
152
153 
    /*@ // figure può essere null o vuota
154 
      @ ensures this.figure == figure;
155 
      @*/
156 
    public void setFigure(String figure) {
157 
        this.figure = figure;
158 
    }
159
160 
    /*@ ensures \result == qty; @*/
161 
    public int getQty() {
162 1 1. getQty : replaced int return with 0 for com/popx/modello/ProdottoBean::getQty → KILLED
 
        return qty;
163 
    }
164
165 
    /*@ requires qty >= 0;
166 
      @ ensures this.qty == qty;
167 
      @*/
168 
    public void setQty(int qty) {
169 
        this.qty = qty;
170 
    }
171
172 
    @Override
173 
    public String toString() {
174 1 1. toString : replaced return value with "" for com/popx/modello/ProdottoBean::toString → SURVIVED
 
        return "ProdottoBean{" +
175 
                "id='" + id + '\'' +
176 
                ", name='" + name + '\'' +
177 
                ", description='" + description + '\'' +
178 
                ", cost=" + cost +
179 
                ", piecesInStock=" + piecesInStock +
180 
                ", brand='" + brand + '\'' +
181 
                ", img=" + Arrays.toString(img) +
182 
                ", figure='" + figure + '\'' +
183 
                '}';
184 
    }
185 
}

Mutations

66

1.1
Location : getId
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/ProdottoBean::getId → KILLED
78

1.1
Location : getName
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/ProdottoBean::getName → KILLED
90

1.1
Location : getDescription
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/ProdottoBean::getDescription → KILLED
102

1.1
Location : getCost
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced double return with 0.0d for com/popx/modello/ProdottoBean::getCost → KILLED
114

1.1
Location : getPiecesInStock
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced int return with 0 for com/popx/modello/ProdottoBean::getPiecesInStock → KILLED
126

1.1
Location : getBrand
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/ProdottoBean::getBrand → KILLED
138

1.1
Location : getImg
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with null for com/popx/modello/ProdottoBean::getImg → KILLED
150

1.1
Location : getFigure
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/ProdottoBean::getFigure → KILLED
162

1.1
Location : getQty
Killed by : com.popx.unit.modello.ProdottoBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.ProdottoBeanTest]/[method:prodottoBean_qtyGetterAndSetter_workCorrectly()] replaced int return with 0 for com/popx/modello/ProdottoBean::getQty → KILLED
174

1.1
Location : toString
Killed by : none replaced return value with "" for com/popx/modello/ProdottoBean::toString → SURVIVED

Active mutators

Tests examined


Report generated by PIT 1.15.2