Web Services:ATM

### Program Information

Name: Web Services:ATM
Domain: Numerical program
Functionality: The electronic payment service is selected as the subject program.And select the transfer feature for the case study.
Input: The input of the transfer operation, and it is represented as a 4-tuple integer vector (A, B, P, M), where (1)$A$ and $B$ denote the sender and recipient account numbers for the transfer transaction,respectively.They consist of 10 digits.  (2)$P$ denotes the transfer type. Its value ranges from 0 to 3, corresponding to type I to IV.(Transfer types I-IV refer to the transfer between two accounts in the same bank and city, in the same bank but different cities, in the same city but different banks, in different cities and different banks, respectively.) (3)$M$ denotes the amount of a transfer transaction, ranging from 0 to 50000, inclusive.
Output: It is represented as a 2-tuple positive real vector $(\Delta A,\Delta B)$, where (1)$\Delta A$ denotes the difference between the balances of account $A$ before transaction and after transaction. (2)$\Delta B$ denotes the difference between the balances of account $B$ after transaction and before transaction.

#### Reference

 Metamorphic Testing for Web Services: Framework and a Case Study https://doi.org/10.1109/ICWS.2011.65

### MR Information

#### MR1------

Description:
Property: $M'=2M \Rightarrow \Delta A' \leq 2\Delta A$ and $\Delta B'=2\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P,M')$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P,M')$ where $M'=2M$
Output relation: $\Delta A' \leq 2\Delta A$ and $\Delta B'=2\Delta B$
Pattern:

#### MR2------

Description:
Property: $P=1$ and $P'=2 \Rightarrow \Delta A' - \Delta B'=\Delta A-\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P',M)$
Follow-up output:  $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P',M)$ where $P=1$ and $P'=2$
Output relation: $\Delta A' - \Delta B'=\Delta A-\Delta B$
Pattern:

#### MR3------

Description:
Property: $P=0$ and $P'\neq 0 \Rightarrow \Delta A' - \Delta B' > \Delta A-\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input:  $(A,B,P',M)$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P',M)$ where $P=0$ and $P'\neq 0$
Output relation: $\Delta A' - \Delta B' > \Delta A-\Delta B$
Pattern:

#### MR4------

Description:
Property: $P=3$ and $P'\neq 3 \Rightarrow \Delta A' \leq \Delta B'=\Delta A-\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P',M)$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P',M)$ where $P=3$ and $P'\neq 3$
Output relation: $\Delta A' - \Delta B' \leq \Delta A-\Delta B$
Pattern:

#### MR5------

Description:
Property: $M'>M \Rightarrow \Delta A' > \Delta A$ and $\Delta B'>\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input:  $(A,B,P,M')$
Follow-up output:  $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P,M')$ where $M'>M$
Output relation: $\Delta A' > \Delta A$ and $\Delta B'>\Delta B$
Pattern:

#### MR6------

Description:
Property: $A'=B$ and $B'=A \Rightarrow \Delta A' = \Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input:  $(A',B',P,M)$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A',B',P,M)$ where $A'=B$ and $B'=A$
Output relation: $\Delta A' = \Delta B$
Pattern:

#### MR7------

Description:
Property: $M'=M+1 \Rightarrow \Delta B' > \Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P,M')$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P,M')$ where $M'=M+1$
Output relation: $\Delta B' > \Delta B$
Pattern:

#### MR8------

Description:
Property: $M'=M-1 \Rightarrow \Delta B' < \Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P,M')$
Follow-up output:  $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P,M')$ where $M'=M-1$
Output relation: $\Delta B' > \Delta B$
Pattern:

#### MR9------

Description:
Property: $M'=0.5*M \Rightarrow \Delta B' \leq 0.5*\Delta B$
Source input: $(A,B,P,M)$
Source output: $\Delta A,\Delta B$
Follow-up input: $(A,B,P,M')$
Follow-up output: $\Delta A',\Delta B'$
Input relation: $(A,B,P,M) \Rightarrow (A,B,P,M')$ where $M'=0.5*M$
Output relation: $\Delta B' \leq 0.5*\Delta B$
Pattern:
Insert title here