OrdineBean.java

1 
package com.popx.modello;
2
3 
import java.sql.Date;
4
5 
public class OrdineBean {
6
7 
    /*@ public invariant id >= 0;
8 
      @ public invariant subtotal >= 0;
9 
      @ public invariant customerEmail == null
10 
      @                 || !customerEmail.isEmpty();
11 
      @ public invariant status != null && !status.isEmpty();
12 
      @ public invariant dataOrdine == null
13 
      @                 || dataOrdine.getTime() >= 0;   // Data valida (non futura non esprimibile in JML)
14 
      @*/
15 
    private int id;
16 
    private float subtotal;
17 
    private String customerEmail;
18 
    private String status = "In elaborazione";
19 
    private Date dataOrdine;
20
21 
    /*@
22 
      @ ensures this.id == 0;
23 
      @ ensures this.subtotal == 0.0f;
24 
      @ ensures this.customerEmail == null;
25 
      @ ensures this.status.equals("In elaborazione");
26 
      @ ensures this.dataOrdine == null;
27 
      @*/
28 
    public OrdineBean() {}
29
30 
    /*@
31 
      @ requires subtotal >= 0;
32 
      @ requires customerEmail != null && !customerEmail.isEmpty();
33 
      @ // dataOrdine può essere null
34 
      @ ensures this.id == 0;
35 
      @ ensures this.subtotal == subtotal;
36 
      @ ensures this.customerEmail == customerEmail;
37 
      @ ensures this.status.equals("In elaborazione");
38 
      @ ensures this.dataOrdine == dataOrdine;
39 
      @*/
40 
    public OrdineBean(float subtotal, String customerEmail, Date dataOrdine) {
41 
        this.subtotal = subtotal;
42 
        this.customerEmail = customerEmail;
43 
        this.dataOrdine = dataOrdine;
44 
    }
45
46 
    /*@ ensures \result == id; @*/
47 1 1. getId : replaced int return with 0 for com/popx/modello/OrdineBean::getId → KILLED
 
    public int getId() { return id; }
48
49 
    /*@ requires id >= 0;
50 
      @ ensures this.id == id;
51 
      @*/
52 
    public void setId(int id) { this.id = id; }
53
54 
    /*@ ensures \result == subtotal; @*/
55 1 1. getSubtotal : replaced float return with 0.0f for com/popx/modello/OrdineBean::getSubtotal → KILLED
 
    public float getSubtotal() { return subtotal; }
56
57 
    /*@ requires subtotal >= 0;
58 
      @ ensures this.subtotal == subtotal;
59 
      @*/
60 
    public void setSubtotal(float subtotal) { this.subtotal = subtotal; }
61
62 
    /*@ ensures \result == customerEmail; @*/
63 1 1. getCustomerEmail : replaced return value with "" for com/popx/modello/OrdineBean::getCustomerEmail → KILLED
 
    public String getCustomerEmail() { return customerEmail; }
64
65 
    /*@
66 
      @ requires customerEmail != null && !customerEmail.isEmpty();
67 
      @ ensures this.customerEmail == customerEmail;
68 
      @*/
69 
    public void setCustomerEmail(String customerEmail) {
70 
        this.customerEmail = customerEmail;
71 
    }
72
73 
    /*@ ensures \result == status; @*/
74 1 1. getStatus : replaced return value with "" for com/popx/modello/OrdineBean::getStatus → KILLED
 
    public String getStatus() { return status; }
75
76 
    /*@
77 
      @ requires status != null && !status.isEmpty();
78 
      @ ensures this.status == status;
79 
      @*/
80 
    public void setStatus(String status) { this.status = status; }
81
82 
    /*@ ensures \result == dataOrdine; @*/
83 1 1. getDataOrdine : replaced return value with null for com/popx/modello/OrdineBean::getDataOrdine → KILLED
 
    public Date getDataOrdine() { return dataOrdine; }
84
85 
    /*@
86 
      @ // dataOrdine può essere null
87 
      @ ensures this.dataOrdine == dataOrdine;
88 
      @*/
89 
    public void setDataOrdine(Date dataOrdine) {
90 
        this.dataOrdine = dataOrdine;
91 
    }
92 
}

Mutations

47

1.1
Location : getId
Killed by : com.popx.unit.modello.OrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.OrdineBeanTest]/[method:ordineBean_gettersAndSetters_workCorrectly()] replaced int return with 0 for com/popx/modello/OrdineBean::getId → KILLED
55

1.1
Location : getSubtotal
Killed by : com.popx.unit.modello.OrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.OrdineBeanTest]/[method:ordineBean_parameterizedConstructor_setsAllFields()] replaced float return with 0.0f for com/popx/modello/OrdineBean::getSubtotal → KILLED
63

1.1
Location : getCustomerEmail
Killed by : com.popx.unit.modello.OrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.OrdineBeanTest]/[method:ordineBean_parameterizedConstructor_setsAllFields()] replaced return value with "" for com/popx/modello/OrdineBean::getCustomerEmail → KILLED
74

1.1
Location : getStatus
Killed by : com.popx.unit.modello.OrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.OrdineBeanTest]/[method:ordineBean_gettersAndSetters_workCorrectly()] replaced return value with "" for com/popx/modello/OrdineBean::getStatus → KILLED
83

1.1
Location : getDataOrdine
Killed by : com.popx.unit.modello.OrdineBeanTest.[engine:junit-jupiter]/[class:com.popx.unit.modello.OrdineBeanTest]/[method:ordineBean_parameterizedConstructor_setsAllFields()] replaced return value with null for com/popx/modello/OrdineBean::getDataOrdine → KILLED

Active mutators

Tests examined


Report generated by PIT 1.15.2