RigaOrdineBean.java

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

Mutations

46

1.1
Location : getOrdineId
Killed by : com.popx.unit.modello.RigaOrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.RigaOrdineBeanTest]/[method:parameterizedConstructor_setsFieldsCorrectly()] replaced int return with 0 for com/popx/modello/RigaOrdineBean::getOrdineId → KILLED
59

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

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

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

Active mutators

Tests examined


Report generated by PIT 1.15.2