Testing of Boyer Program

### Program Information

Name: Testing of Boyer Program
Domain: Algorithm
Functionality: The program returns the index of the first occurrence of a specified pattern within a given text.
Input: $(x_1,y_1),(x_1,y_1),(x_3,y_3)$ are test cases for the function $f(x, y)$.   $x_1,x_2,x_3,y_1,y_2,y_3$, and $s$ are arbitrary strings.  $x+y$ appends string $y$ to string $x$.  $x/y$ removes string $y$ from string $x$.  $x.substr(m,n)$  returns a new string that is a substring of $x.len(x)$ returns the length of string $x$.  $upperlowercase(x)$ changes each character in string $x$ from lower case to upper case and vice versa. $offset(x)$ offsets each character in string $x$ to get a new string.  $reverse(x)$ reverses the string $x$.  $duplicate(x)$ duplicates each character in string $x$ to get a new string.
Output: The function $f(x,y)$ returns the index of pattern $y$ within the string $x$ if $x$ contains $y$; otherwise, return -1.

#### Reference

 An Empirical Comparison between Direct and Indirect Test Result Checking Approaches https://doi.org/10.1145/1188895.1188901

### MR Information

#### MR1------

Description:
Property: $(x_2=x_1+s) \& (y_2=y_1)\& (f(x_1,y_1)>-1) \Rightarrow f(x_1,y_1)=f(x_2,y_2)$
Source input:  $(x_1,y_1)$
Source output:  $f(x_1,y_1)$
Follow-up input: $(x_2.y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2.y_2)$ where $x_2=x_1+s,y_2=y_1$
Output relation: $f(x_1,y_1)=f(x_2,y_2)$ when $(f(x_1,y_1)>-1)$
Pattern:

#### MR2------

Description:
Property: $(x_3=x_1+x_2)\& (y_1=y_2=y_3) \& (f(x_1,y_1)=-1) \Rightarrow f(x_3,y_3) \leq f(x_2,y_2)+len(x_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2),(x_3,y_3)$
Follow-up output: $f(x_2,y_2),f(x_3,y_3)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2),(x_3,y_3)$ where $x_3=x_1+x_2,y_1=y_2=y_3$
Output relation: $f(x_3,y_3) \leq f(x_2,y_2)+len(x_1)$ when $f(x_1,y_1)=-1$
Pattern:

#### MR3------

Description:
Property: $(x_1=x_2) \& (y_2=y_1.substr(0,len(y_1)-1)) \Rightarrow f(x_2,y_2) \leq f(x_1,y_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1,y_2=y_1.substr(0,len(y_1)-1)$
Output relation: $f(x_2,y_2) \leq f(x_1,y_1)$
Pattern:

#### MR4------

Description:
Property:  $(x_3=x_1+x_2) \& (y_1=y_2=y_3) \& (f(x_1,y_1)=-1) \& (f(x_2,y_2) > -1) \Rightarrow f(x_3,y_3) \leq f(x_2,y_2)+len(x_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2),(x_3,y_3)$
Follow-up output: $f(x_2,y_2),f(x_3,y_3)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2),(x_3,y_3)$ where $x_3=x_1+x_2,y_1=y_2=y_3$
Output relation: $f(x_3,y_3) \leq f(x_2,y_2)+len(x_1)$ when $f(x_1,y_1)=-1,f(x_2,y_2)>-1$
Pattern:

#### MR5------

Description:
Property: $(x_2=upperlowercase(x_1)) \& (y_2=upperlowercase(y_1)) \Rightarrow f(x_1,y_1)=f(x_2,y_2)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=upperlowercase(x_1),y_2=upperlowercase(y_1)$
Output relation:  $f(x_1,y_1)=f(x_2,y_2)$
Pattern:

#### MR6------

Description:
Property: $(x_2=offset(x_1)) \& (y_2=offset(y_1)) \Rightarrow f(x_1,y_1)=f(x_2,y_2)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=offset(x_1),y_2=offset(y_1)$
Output relation: $f(x_1,y_1)=f(x_2,y_2)$
Pattern:

#### MR7------

Description:
Property: $(x_1=x_2) \& (y_2=y_1.substr(0,len(y_1)/2)) \Rightarrow f(x_2,y_2) \leq f(x_1,y_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1,y_2=y_1.substr(0,len(y_1)/2)$
Output relation: $f(x_1,y_1) \leq f(x_2,y_2)$
Pattern:

#### MR8------

Description:
Property: $(x_2=x_1.substr(1,len(x_1)-1)) \& (y_1=y_2) \&(f(x_1,y_1 \geq 1))\Rightarrow f(x_2,y_2) = f(x_1,y_1)-1$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1.substr(1,len(x_1)-1),y_2=y_1$
Output relation: $f(x_1,y_1) = f(x_2,y_2)-1$ when $f(x_1,y_1) \geq 1$
Pattern:

#### MR9------

Description:
Property: $(x_2=x_1+y_1) \& (y_1=y_2) \& (f(x_1,y_1)=-1) \Rightarrow f(x_2,y_2) \geq len(x_1)-len(y_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1+y_1,y_2=y_1$
Output relation: $f(x_2,y_2) \geq len(x_1)-len(y_1)$ when $f(x_1,y_1) = -1$
Pattern:

#### MR10------

Description:
Property: $(x_2=reverse(x_1)) \& (y_2=reverse(y_1)) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) > -1$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=reverse(x_1),y_2=reverse(y_1)$
Output relation: $f(x_2,y_2) > -1$ when $f(x_1,y_1) > -1$
Pattern:

#### MR11------

Description:
Property: $(x_2=x_1.substr(0,f(x_1,y_1))) \& (y_1=y_2) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) = -1$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=substr(0,f(x_1,y_1)),y_2=y_1$
Output relation: $f(x_2,y_2) = -1$ when $f(x_1,y_1) > -1$
Pattern:

#### MR12------

Description:
Property: $(x_2=x_1.substr(f(x_1,y_1),len(x_1)-f(x_1,y_1))) \& (y_1=y_2) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) = 0$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation:  $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=substr(f(x_1,y_1),len(x_1)-f(x_1,y_1)),y_2=y_1$
Output relation: $f(x_2,y_2) = 0$ when $f(x_1,y_1) > -1$
Pattern:

#### MR13------

Description:
Property: $(x_2=reverse(x_1)) \& (y_2=reverse(y_1)) \& (f(x_1/y_1,y_1) = -1) \Rightarrow f(x_1,y_1) + f(x_2,y_2) + 2*len(y_1) \geq len(x_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=reverse(x_1),y_2=reverse(y_1)$
Output relation: $f(x_1,y_1) + f(x_2,y_2) + 2*len(y_1) \geq len(x_1)$ when $f(x_1/y_1,y_1) = -1$
Pattern:

#### MR14------

Description:
Property: $(x_2=duplicate(x_1)) \& (y_2=duplicate(y_1)) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) = f(x_1,y_1)*2$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=duplicate(x_1),y_2=duplicate(y_1)$
Output relation: $f(x_2,y_2) = f(x_1,y_1)*2$ when $f(x_1,y_1) > -1$
Pattern:

#### MR15------

Description:
Property: $(x_2=x_1.substr(0,f(x_1,y_1)+len(y_1))) \& (y_1=y_2) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) = f(x_1,y_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1.substr(0,f(x_1,y_1)+len(y_1)),y_2=y_1$
Output relation: $f(x_2,y_2) = f(x_1,y_1)$ when $f(x_1,y_1) > -1$
Pattern:

#### MR16------

Description:
Property: $(x_2=reverse(x_1)) \& (y_2=reverse(y_1)) \& (f(x_1,y_1) > -1) \Rightarrow f(x_1,y_1) + f(x_2,y_2) + len(y_1) \leq len(x_1)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input:  $(x_2,y_2)$
Follow-up output:  $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=reverse(x_1),y_2=reverse(y_1)$
Output relation: $f(x_1,y_1) + f(x_2,y_2) + len(y_1) \leq len(x_1)$ when $f(x_1,y_1) > -1$
Pattern:

#### MR17------

Description:
Property: $(x_2=reverse(x_1)) \& (y_2=reverse(y_1)) \& (f(x_1,y_1) = -1) \Rightarrow f(x_2,y_2) = -1$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=reverse(x_1),y_2=reverse(y_1)$
Output relation: $f(x_2,y_2) = -1$ when $f(x_1,y_1) = -1$
Pattern:

#### MR18------

Description:
Property: $(x_2=x_1.substr(0,f(x_1,y_1)+len(y_1))) \& (y_1=y_2) \& (f(x_1,y_1) > -1) \Rightarrow f(x_2,y_2) = len(x_2) - len(y_2)$
Source input:   $(x_1,y_1)$
Source output:   $f(x_1,y_1)$
Follow-up input: $(x_2,y_2)$
Follow-up output: $f(x_2,y_2)$
Input relation: $(x_1,y_1) \Rightarrow (x_2,y_2)$ where $x_2=x_1.substr(0,f(x_1,y_1)+len(y_1)),y_2=y_1$
Output relation: $f(x_2,y_2) = len(x_2) - len(y_2)$ when $f(x_1,y_1) > -1$
Pattern:
Insert title here