header
Testing of Boyer Program 

Tag:
Edit edit   Starstar

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