                                                                  Application of property-based testing tools
                                                                           for metamorphic testing

                                                                      Nasser Alzahrani, Maria Spichkova, James Harland
                                                                 School of Computing Technologies, RMIT University, Melbourne, Australia
                                                              s3297335@student.rmit.edu.au, {maria.spichkova,james.harland}@rmit.edu.au




                                         Keywords:     Software Testing, Metamorphic Testing, Property-Based Testing, Formal Specification

                                         Abstract:     Metamorphic testing (MT) is a general approach for the testing of a specific kind of software systems –
arXiv:2211.12003v1 [cs.SE] 22 Nov 2022




                                                       so-called “non-testable”, where the “classical” testing approaches are difficult to apply. MT is an effective
                                                       approach for addressing the test oracle problem and test case generation problem. The test oracle problem is
                                                       when it is difficult to determine the correct expected output of a particular test case or to determine whether
                                                       the actual outputs agree with the expected outcomes. The core concept in MT is metamorphic relations
                                                       (MRs) which provide formal specification of the system under test. One of the challenges in MT is effective
                                                       test generation. Property-based testing (PBT) is a testing methodology in which test cases are generated
                                                       according to desired properties of the software. In some sense, MT can be seen as a very specific kind of PBT.
                                                       In this paper, we show how to use PBT tools to automate test generation and verification of MT. In addition to
                                                       automation benefit, the proposed method shows how to combine general PBT with MT under the same testing
                                                       framework.

                                                       Preprint. Accepted to the 17th International Conference on Evaluation of Novel Approaches to Soft-
                                                       ware Engineering (ENASE 2022). Final version published by SCITEPRESS, http://www.scitepress.org



                                         1    INTRODUCTION                                               on actual code which help in finding subtle faults on
                                                                                                         live running systems [15]. One of the main attributes
                                         Formal specification is an essential tool for managing          of PBT is that it can automatically generate tests to
                                         the complexity of specifying and verifying the design           cover edge cases that are not so obvious to identify
                                         and the development of critical software systems. The           manually. Two main elements of PBT approach make
                                         formal approach removes ambiguity, improves preci-              this possible: (1) a random test generator, responsible
                                         sion, and used to verify that the requirements are ful-         for generating random values in a controlled way, and
                                         filled. Appel et al. summarised a number of desired             (2) a so-called shrinker, minimizing the number of the
                                         qualities that the specification should have in order           generated tests cases to allow for easier debugging.
                                         to be effective, see [3]. Firstly, the specification has            Metamorphic Testing (MT) is a special PBT tech-
                                         to be formal, where the specification should be math-           nique elaborated for the cases where it’s complicated
                                         ematically precise. It should be rich, i.e. precisely           to specify “classical” test cases having input and out-
                                         expressing the intended behaviour of the system (we             put data flows - in some cases, it’s difficult to iden-
                                         could reformulate this quality as completeness). The            tify what could be the correct output for each partic-
                                         specification has to be two-sided where the specifica-          ular input. For “classical” testing we need to have a
                                         tion is exercised by both implementations and clients.          so-called an oracle that can determine whether or not
                                         Finally, the specification has to be live where it is au-       the output is correct wrt. the provided input and this
                                         tomatically checked against actual code rather than             decision should be taken in a reasonable amount of
                                         some abstract model.                                            time, see [30]. In the case an oracle cannot be cre-
                                              Formal languages like TLA+ [18], or Alloy [16]             ated, the system are typically called non-testable (or
                                         are generally concerned with specifying systems                 untestable), but MT can provide an effective solution
                                         against some models rather than the actual code under           to the oracle problem using Metamorphic Relations
                                         development. On the other hand, property-based test-            (MR), see e.g., [24]. MT was initially introduced in
                                         ing (PBT) facilitates the use of formal specifications          [5] in the domain of numerical analysis. Since then, it
has developed and been applied in many application           phic testing.
areas, such as compilers, medical systems, embedded              In validity checks, one writes functions to check
applications, search engines, service computing, sim-        some invariants of the system under test or the
ulation software, image processing systems, machine          datatypes used in the system. This process also in-
learning software and optimizing software [6].               cludes writing properties to check test-case generator
     PBT tools for testing functional programs were          and test-case shrinker both produce valid results. The
first introduced in the Haskell programming language         last step is to write property for the functions under
by [11], where QuickCheck, a library for random test-        test which performs a single random call and checks
ing of program properties, was implemented. Since            that the return value is valid. For instance, when test-
then, many libraries have been developed following           ing the functionality of inserting a value into a tree
this approach for different programming languages.           datatype, we demand that all the keys in a left subtree
The main components of QuickCheck are the gener-             must be less than the key in the node, and all the keys
ator of random values, the shrinker, and the checker         in the right subtree must be greater.
which runs these random values with pre-selected                 A postcondition is a property that should be true
functions. In our work, we extend the generator and          after a call. One can come up with such property by
the shrinker in order to automate MT test generation         asking what would be the expected state of the system
and verification.                                            after calling some function. A postcondition usually
     The idea of generating random tests is not new,         tests one function after calling this function with some
see for example [8]. However, using PBT tools such           random argument and then checking an expected re-
QuickCheck has many advantages. First of all, PBT            lationship between the result and its argument. For
has many tools for automating and controlling the            Instance, after calling insert (which inserts a value in
generation of random test cases. Secondly, these tools       some tree datatype), we should be able to find the key
allow controlled strategies for generating random data       inserted without changing previously inserted keys.
of complicated data types, i.e., it is possible to config-       A model-based property is used to test some func-
ure how the random values distribute over the input          tion by making a single call and comparing its result
domain. Although [7] argues that one of MT’s main            with the result of some abstract operation. The model
advantages is the ease of test case automation, the MT       refers to the abstraction functions which map the real
automation is a complex task, when using PBT tools           arguments and results to abstract values.
such as QuickCheck as a tool to test MR relations.               Inductive properties are the properties that one can
     Contributions: The main contribution of this pa-        use induction to assert that the only function that can
per is a systematic approach in which we utilize the         pass the tests is the correct one. This is usually done
random generation of test cases and automatic test-          by relating a call of the function under test to calls
ing capabilities of PBT tools to automate some steps         with smaller arguments. The set of inductive prop-
of metamorphic testing: More precisely, we auto-             erties covering all possible cases allows the testing
mate test case generation and test case verification by      of the base case and induction steps of an inductive
extending QuickCheck’s shrinker and generator with           proof-of-correctness.
our customized shrinker and generator. These variants            The canonical example in the literature to explain
are simpler and more amendable to customization in           property based testing is the reversing a list. One
the context of MT.                                           property that should hold for all lists is that reversing
                                                             a list x twice returns the original list:
                                                                              reverse (reverse x) = x
2    BACKGROUND:                                             In the case of functional oracle-based testing, we
     PROPERTY-BASED TESTING                                  would need to identify the equivalence partitions (the
                                                             sets of inputs that have to be handled equivalently as
Property-based testing (PBT) is an approach to test-         they have to provide the same type of output but with
ing software by defining general specifications and          possibly different values), and then specify at least
properties that must hold for all the executions of ran-     one test case for each partition, or use boundary val-
domly generated test cases. The inputs to these test         ues in partitions that are ranges. Thus, for reverse
cases are random. If these properties do not hold,           function this could be an empty list [] and some non-
a minimized failing tests are reported. In PBT, test         empty list, e.g, [1, 2, 3], i.e., our test cases would be
cases are generated randomly according to universally                   reverse (reverse []) = []
quantified properties. Examples of quantified proper-                   reverse (reverse [1, 2, 3]) = [1, 2, 3]
ties include; validity checks, postconditions, model-        In contrast to this approach, in PBT the checks take
based properties, inductive properties, and metamor-         place on the return value of the function under test,
instead of checking values “hard-coded” in the test         outputs. When implementing MT, we first generate
cases such as [] and [1, 2, 3]. That is, the input to       source test cases. Then use the MR to generate new
the function under test would be automatically gener-       input. This new input is then used to compare the
ated and the library chooses random values for testing      output from the first set of the tests with the last ones.
rather than the tester specifying particular values. For        In our proposed method, we show how to auto-
example, for the reverse function, one could call the       mate the test case generation and verification of MT
reverse function twice and expect the original list to      using QuickCheck. Our method can be generalized to
be returned. The library generates many random test         work with other PBT tools other than QuickCheck as
cases and reports a failure if it finds a counterexample.   our method extends features of QuickCheck that are
    In the case of QuickCheck, the property to be           common in other PBT tools.
passed to the library is reverse (reverse x) = x, the           Figure 1 illustrates MT in the context of testing
library will generate the random values for x, and will     a compiler. There are two paths that are expected to
report a failure if it finds a counterexample.              lead to the same output:
    It is worth noting that there are some anti-patterns    (1) We start with Program 1, it is compiled to obtain
that could emerge while writing property-based tests.           the corresponding executable code Executable 1.
Because it is sometimes difficult to think about a              Then, we run Executable 1 with some input data
property, practitioners usually fall into the trap of du-       x to get an output.
plicating the implementation of the code in tests. The
literature on PBT has many other examples of such           (2) We modify Program 1 to a semantically equiv-
anti-patterns and how to avoid them. One solution to            alent but syntactically different Program 2 (e.g.,
avoid this problem is MT.                                       by unrolling a loop or removing a comment etc.),
    MT is a successful method in solving the oracle             then apply the same compilation method to get the
problem in software testing. The core idea is this: in          corresponding executable code Executable 2. Af-
the cases when it’s hard to specify in advance what             ter that, we run Executable 2 with the same input
exactly should be the output of a function, we may be           data x to get an output.
able to observe the change to the output when chang-        When both outputs are obtained, we compare them: if
ing the input. That is, valuable information about the      they are not exactly the same, the compiler is faulty.
function would be whether and how its input changes             One of the benefits of using PBT for MT is the
when we change its input. For instance, even if the         rich sets of tools available. For instance, PBT tools
expected result of a function such as inserting a key       allow the creation of strategies for generating random
into a tree is difficult to predict, we may still be able   data for complicated data types with minimal setup.
to express an expected relationship between this re-        In MT, the operations and data types are usually more
sult and the result of some other call. In this case, if    complicated than simple data types such as integers
we insert an additional key into t before calling insert    or lists. Existing approaches for creating these data
k v, then we expect the additional key to appear in the     types are ad-hoc [9]. In these other approaches, one
result also.                                                has to do almost the same setup work for every kind
                                                            of data type in order to generate the random values.
                                                            PBT tools, on the other hand, are more general and
                                                            cover more data types without the need to duplicate
                                                            the code for every kind of data type or model. In ad-
                                                            dition, PBT requires less code than these other ap-
                                                            proaches with more control over the distribution of
                                                            the test cases space. These approaches evenly dis-
                                                            tribute the test cases over the input space.
                                                                Creating a random BST using any PBT library re-
                                                            quires less setup work. One only required to define
                                                            the data type and pass it to the library. However, since
  Figure 1: Testing compilers using Metamorphic testing     we are using these PBT tools for MT, some more
                                                            setup and customization are required.

Metamorphic Relations (MRs) are a central element
of MT. The MRs are properties of the function under
test. An important (and usually missed) attribute of
MR is that they relate multiple inputs to their expected
3    RELATED WORK                                         4    PROPOSED APPROACH
The effectiveness of MT in alleviating the oracle         In this section, we present a systemic method to
problem has allowed it to appear in many different        use PBT tools to test MRs. We specifically choose
application domains. However, many of these appli-        QuickCheck to illustrate the proposed approach. Our
cations do not provide a systematic way to automate       method is general and can be implemented using
some parts MT.                                            other PBT libraries as well. Our proposed method
    The automation of MT was first introduced in          consists of three aspects. First, we develop a new gen-
[13] where they proposed a framework that utilizes        erator for generating test cases for MT. Second, we
Constraint Logic Programming techniques to find test      develop a new test case shrinker. Finally, we use the
data that violate a given metamorphic relation. How-      newly designed generator and the shrinker instead of
ever, they require the usage of special metamorphic-      QuickCheck’s default generator and shrinker. In the
relations, such as permutation-based relations, to        rest of the section, we present the core features and
speed up the search among the possible test data.         steps of our approach, and then discuss the advantages
    There are few other efforts to automate MT steps.     of this approach.
For instance, Zhu created a tool for automating meta-         QuickCheck is a library for random testing of pro-
morphic testing for Java unit tests, see [32]. This       gram properties. The programmer provides a spec-
method is specific to Java unit tests. Our method is      ification of the program, in the form of properties
more general and can be applied in any programming        that functions should satisfy. The library then gener-
language which has library support for PBT.               ates a large number of random test cases and checks
    An automatic MT framework for compilers is pro-       that the property holds. Specifications are expressed
posed in [29]. Their approach in generating the test      in Haskell. The Haskell programming language also
cases is similar to the approach presented in this pa-    provides functions to define properties, observe the
per. However, their approach is tailored to the domain    distribution of test data, and define test data genera-
of testing compilers, where we propose a generally        tors, which is an important advantage for system spec-
applicable solution.                                      ification.
    In [20], the authors propose a method that allows         When using PBT tools such as QuickCheck there
the composition of new metamorphic relations based        is some expected setup that needs to be done before
on previously defined ones, their case study showed       defining the properties. One such setup is shrinking.
that new metamorphic relations can be constructed         The main objective of shrinking is to produce a mini-
by compositing some existing metamorphic relations.       mum failing test cases which facilitate the debugging
They assert that the new derived metamorphic relation     of the program. Another required setup is the random
delivers better metamorphic testing than the original     values generator which can be configured depending
metamorphic relation as well as reduces the number        on the scenario. More importantly, the generator and
of test cases.                                            shrinker need to be designed to work together when
    Work related to verifying authenticated data struc-   testing MRs. Otherwise, if we use the default test
tures (ADS) is presented in [23]. The approach of         case generator and shrinker, the checkers might miss
Miller provides a semantics for a programming lan-        some test cases or generate invalid tests. The pro-
guage LambdaAuth, which supports ADS. This ap-            posed method ensures that does not happen.
proach provides many benefits, however, it might be           The steps needed to systematically test MR rela-
hard to convince practitioners to use it which is less    tions using PBT tools are as follows:
likely to be widely spread among engineers and is dif-    (1) Specify an MR property
ficult to have an impact. In [4], the authors used Is-
abelle proof assistant to formally verify LambdaAuth.     (2) Customize the test case generator
They also assert that they found several mistakes in      (3) Customize the test case shrinker
the semantics of lambdaAuth. In our work, we use          (4) Run the checker
a mainstream programming language (Haskell) to de-
sign such ADS and verify our implementation of these      Our main contributions are in Steps 2 and 3. Let us
ADS using PBT and MT.                                     now discuss these steps and our solution in more de-
                                                          tail.
                                                               Step 1: Specify an MR property. Specifying
                                                          suitable MRs is key in MT. Although identifying MRs
                                                          is not a difficult task, this is typically a manual pro-
                                                          cedure, see [21], and we don’t intend to automate
                                                          it within our approach. However, there have been
some approaches intending to automate this step [10],           is it uses partially defined test values. If a prop-
and in our future work, we consider combining our               erty returns a Boolean result for a partially defined
method with these approaches.                                   value, the shrinker does not enumerate more ver-
     Step 2: Customize the test case generator. The             sions of this value. The benefit is that the checker
first thing that all PBT libraries do is to generate ran-       will stop as soon it encounters the first failing test
dom inputs for the functions under test. In the PBT             which improves the speed of the checker.
literature, this is known as generation. For every type,        One of the differences between QuickCheck
there is an associated random test generator.               shrinker and our shrinker is that our method of shrink-
     For example, to generate a list of values, one has     ing is integrated into generation. It is worth noting
to use the generator together with two parameters.          that almost all PBT tools in many different program-
The first parameter is the number of elements in the        ming languages use a similar shrinking methodology
list. The second parameter is the size which depends        as the one used in QuickCheck. The main problem
on the type of values being generated and the con-          with this approach is that shrinking is defined based
text. For example, the size can be the maximum value        on datatypes. This constraints the ways in which val-
of Integer type, the maximum length of a list, or the       ues are shrinked. That is, there is only one way to de-
depth of a binary search tree.                              fine shrinking for the same data type without taking
     For MT, the generator has to be customized to pro-     into consideration the way it was generated. On the
duce valid test cases. In Section 5 we will present an      other hand, our shrinker is composed with the gener-
example of BST, where the values should not be gen-         ator and the generator controls how the values it pro-
erated uniformly.                                           duces shrinks.
     Step 3: Customize the test case shrinker. Al-              Our approach to shrinking has many benefits. For
most all PBT libraries and frameworks have a mech-          example, shrinking happens even if there is no defined
anism to reduce the set of generated test cases that        shrinker on the datatype. This allows the shrinker
fails a property to a minimum number of failing test        to share the same variants as the generator and, at
cases that is necessary for the debugging process, as       the same time, reduce the effort needed to write a
an unnecessary large number of the failed tests cases       separate shrinker for each datatype involved in the
(where many cases might refer to the same error) will       test. Another benefit of our shrinker is that failure
make debugging process more complicated and time-           reported is more revealing than the shrinker defined
consuming. This mechanism is known in the litera-           as datatype. For instance, in QuickCheck, errors are
ture as shrinking.                                          sometimes shrinked to different errors, which is un-
     Step 4: Run the checker. In this step, we pass         desirable since the error we expect is being reduced
the MR property, which was specified in Step 1 to the       to another error we do not care about. To mitigate
checker. If the function under test does not satisfy the    this problem, one has to duplicate the constraint logic
MR, the PBT library will report the failing test case       both in the generator and in the shrinker. In our im-
that violated the MR property.                              plemented shrinker, the main idea is that we shrink the
                                                            outputs by shrinking the inputs. This help in finding
As mentioned in Step 3, we cannot use the de-               possible more shrinks based on that representation.
fault QuickCheck’s shrinker for testing MR proper-              Our designed shrinker covers the range between
ties. Thus, we modify QuickCheck generator with our         the smallest value of some type and increases the
designed generator. The default QuickCheck’s gener-         value until the test fails. It repeats this process until
ator is based on [12] which is found to require some        the test passes. In this case, it reports the largest value
efforts to use in MT. On this basis, we design a mod-       from the previous step as the smallest test case that
ified generator and instruct QuickCheck to use it in-       fails the property, i.e., the boundary values. For exam-
stead of its default one. The advantage of the pro-         ple, suppose that we are testing whether the value of
posed approach is that the testing of MT can together       variable x of type Integer is less than 77 (x < 77). Sup-
with other properties under the same testing frame-         pose that the first random value that is generated (by
work. Thus, the same shrinker and verifier can be           the generator) is 90 which will cause the test to fail.
used for both MT and general properties to test.            Then, the shrinker will generate new random values
    Our version of shrinker has the following features:     and in random steps ranging from zero to 89. Now,
 • The values are enumerated by depth instead of            maybe the new failing value is 89. The shrinker will
   size and for this reason, the number of values           repeat the same process again for the values between
   tends to grow quickly as our shrinker explores fur-      zero and 88. The shrinking repeats until the random
   ther test cases.                                         value is 78 after which the smallest failing test value
 • The modified shrinker exploits laziness [14]. That       is 77. After which the shrinker stops.
    The way we ensure the validity of the generated        ues into a BST. Starting with the Tree at the top, we
(then shrinked) test cases is by adding a precondition.    insert some key k1 and some value v1 to get some
The main objective of a precondition is to inform the      modified tree. Then, another key k2 and value v2 is
generator not to generate invalid test cases using the     inserted into the modified tree to get the out put tree
valid function that we have to implement. The valid        (whatever it is). We repeat the same operation to the
function checks the property before passing it to the      original tree but we change the inputs to insert. That
generator. The generator will still generate random        is, we insert k2 and v2 followed by inserting k1 and v1
test cases but they will not be executed. The valid        to get the out put tree. The metamorphic relation as-
function depends on the context. For instance, in the      serts that the two out put trees should be the same oth-
context of Binary Search Trees, the valid function         erwise insert is faulty. The notion of quality between
checks that the keys in the left subtree are less than     two trees depends on the operations under test. For
the key at the root node and all the keys on the right     insert, we can just assert that if the keys and values
subtree is greater than the key at the root node.          in both trees are the same the trees are semantically
                                                           equivalent.

5    EXAMPLE: BINARY SEARCH
     TREE
As a running example to explain the proposed method
of applying the PBT tool QuickCheck for MT, we
consider the operations of inserting into and deleting
from a binary search tree (BST). This example not
trivial but is simple enough to explain the proposed
method. Another reason for choosing BST is that the
same approach can be used for testing more elaborate       Figure 2: MR property: Tree 1 and Tree 2 are semantically
                                                           equivalent
kinds of trees such as Merkle trees [22], see also our
discussion future works in Section 6. To evaluate the
proposed approach, we also introduce faulty variants       To test the effectiveness of the proposed method, we
of the operations under test, insert and delete.           intentionally introduce faulty variants of insert and
    A BST is a type of data structure for storing val-     delete and test them in a similar way. The faulty vari-
ues such as integers in an organized way. The internal     ants are:
nodes of BST store a key greater than all the keys in
                                                               Fault 1 insert removes the original tree and re-
the node’s left subtree and less than those in its right
                                                               turns just the newly inserted value in a single
subtree. BST are usually used for fast lookup, in-
                                                               node.
sert and delete of value items. Testing insert function
which inserts a key and value in a binary search tree          Fault 2 delete does not build the tree above the
is difficult. Using MT approach, we can change the             key being deleted. That is, it only returns the rest
input using a new key and value and then observe the           of the tree instead.
relationship to the original call to insert function. MT
allows more numbers of properties to be tested. Us-        Starting with the declaration of the data type, a BST
ing the example of trees, we can use insert with delete    for some key k and value v, is either a Lea f or a
and test the output. Inversely, we can use delete with     Branch containing left subtree, key k, value v and the
insert and test the output. This is true for any combi-    right subtree, respectively.
nation of the operations under test.                           Step 1: Specify an MR property. This is the
    One possible mistake when testing properties of        property that we wish the PBT tool to check. Before
the insertion and deletion of BST, is that the test code   we can choose the MR, we need to pick the functions
is the same as the implementation. Therefore, if there     that we want to test. For this example we choose in-
is a bug in the implementation, it will also be in the     sert and delete. insert takes key k, value v and the tree
tests which renders the tests useless. One solution to     and returns the modified tree after the insertion. The
this problem is to get an appropriate metamorphic re-      delete function takes key k and value v and returns the
lation to test the intended behaviour. This way we can     modified tree after the deletion.
verify the correctness of the implementation without           Since we want to test two distinct functions (in-
a expecting concrete output.                               sert and delete), there are, at least, two MRs that we
    Figure 2 shows the MT of inserting keys and val-
identify. The MRs that we want to check are the fol-           and generate the minimum failing examples for both
lowing:                                                        of the introduced faults. However, one interesting ob-
  • MR 1: Inserting into the tree after modifying it           servation is that fault 1 is missed by the checker when
    with a delete operation should be the same as do-          we don’t check both MR at the same time. There-
    ing the deleting before inserting                          fore, it is recommended to include as many MRs as
                                                               necessary in a single test to specify properties of the
  • MR 2: Deleting from the tree after modifying it            function under test.
    with inserting, should be the same as doing the                One misconception of MT is that any property can
    inserting before deleting                                  be considered as an MR, see [7]. It is true that MR
    Table 1 shows the precise Metamorphic Relations            is a property but the inverse is not true. Therefore,
(properties) for inserting and deleting in the context         when using PBT tools to test MR properties, we al-
of a binary search tree. The first set shows the inser-        most always use two operations, at least, in a single
tion of key k and value v into the tree modified by the        metamorphic test. More precisely, when using PBT
deletion of key k0 from the original tree. The MR as-          tools to test metamorphic relations, we should either
serts this should be equivalent to deleting k from the         change the input to same function as shown in Figure
tree modified by insertion key k and value v into the          2 or use two distinct operations as shown in Table 1.
same tree. The second is set of operations shows the
deletion of key k into the tree t modified by the inser-
tion of key k0 and value v0 . Again, the MR asserts this
should be equivalent to doing the deletion of k first,
                                                               6    CONCLUSIONS
then, inserting k0 and v0 .
                                                               In this paper, we presented a systemic method for
    This demonstrates how effective MT can be for
                                                               using PBT tools to automate the test generation and
generating properties. That is, if the number of opera-
                                                               verification of metamorphic relations. Many existing
tions is n, the number of derived operations is O(n2 ),
                                                               efforts for automating MT are domain-specific, i.e.
see also [19].
                                                               the automation of the MT steps is elaborated to work
    Step 2: Customize the test case generator. We
                                                               only for specific application domains such as web ser-
use the generator defined in section 4 which generate
                                                               vices and specific programming languages. The work
random trees by creating a random list of keys and
                                                               presented in this paper is more general and can be
a random list of values and inserting them into the
                                                               used in many different scenarios where MT is needed.
empty tree using insert function. We also have to de-
                                                               Its advantage is in using authenticated data structures
fine valid function which ensures the following:
                                                               (ADS) to solve the issue.
  • All the keys in the left subtree is less than the key          PBT tools are generally used for testing univer-
    at the root node                                           sal properties other than MR such as postconditions,
  • All the keys in the right subtree is greater than the      inductive properties, and model-based properties. In
    key at the root node                                       this paper, we have shown a method to created a spe-
    Step 3: Customize the test case shrinker. Using            cialized test-case generator and test-case shrinker to
the default shrink function, shrink might include in-          automate some parts of MT steps. We showed that
valid trees. The library may shrink the test case before       The default shrinker is not ideal for testing some kinds
reporting it. Or It may produce a valid tree with an in-       of MR as it is difficult to compose previously de-
valid shrinking. Therefore, we must add the precon-            fined MR to create new MRs. In addition, the default
dition discussed in 4 to ensure only valid trees partic-       shrinker may report confusing failure cases since it is
ipates the shrinking process. This precondition holds          based on defining shrinking on datatypes which forces
for any randomly generated test. The precondition is           the user to add additional duplicated code. However,
just the valid function defined in Step 2.                     this workaround is not needed with our shrinker since
    Step 4: Run the checker. The checker is just a             it does not have to be defined on the datatypes and
function that takes any property and returns a Boolean         there would no need to encode the invariants into the
value. We pass the MRs relations to the checker func-          shrinkers, which requires more effort and could be
tion then the library will generate many test cases.           difficult if the scenario is more complicated. We have
The number can be set when configuring the checker.            implemented our method using one particular PBT
    For the correct variants of insert and delete, the         tool QuickCheck. However, our method is general and
PBT library reports a 100 passing tests. The number            can be implemented using any other PBT tool.
of the generated test case can also be configured to               We presented our method using the Binary search
increase the assurance of the test. For the faulty vari-       tree example. The two operations we selected were
ants, the tests report failing of tests after 100 test cases   insert and delete and we introduced faulty versions of
                                 Table 1: Some MR properties for a BST insert and delete
                         op 1       op 2                 Metamorphic properties
                        insert     delete    insert k v (delete k’ t)= delete k’ (insert k v t)
                        delete     insert   delete k (insert k’ v’ t) = insert k’ v’ (delete k t)


these two operations. We showed it is recommended               [8] Tsong Yueh Chen, Fei-Ching Kuo, Robert G
to use as many MRs as necessary to specify the oper-                Merkel, and TH Tse. Adaptive random testing:
ations under test otherwise the test might miss some                The art of test case diversity. Journal of Systems
subtle faults.                                                      and Software, 83(1):60–66, 2010.
    For future work, we plan to combine the proposed            [9] Tsong Yueh Chen, Fei-Ching Kuo, Dave Towey,
approach to our earlier works presented in [1, 2],                  and Zhi Quan Zhou. A revisit of three studies
where we used PBT tools to test models generated                    related to random testing. Science China Infor-
by formal methods tools such as TLA+ [17]. Another                  mation Sciences, 58(5):1–9, 2015.
direction of the future work is to consider the human-
                                                               [10] Tsong Yueh Chen, Pak-Lok Poon, and Xiaoyuan
centered aspects to enhance the proposed framework,
                                                                    Xie. Metric: Metamorphic relation identifica-
following the ideas presented in [25, 28, 27, 26, 31].
                                                                    tion based on the category-choice framework.
                                                                    Journal of Systems and Software, 116:177–190,
                                                                    2016.
REFERENCES                                                     [11] Koen Claessen and John Hughes. QuickCheck:
                                                                    A lightweight tool for random testing of Haskell
 [1] Nasser Alzahrani, Maria Spichkova, and
                                                                    programs. In Functional Programming, pages
     Jan Olaf Blech. Spatio-temporal models for
                                                                    268–279, 2000.
     formal analysis and property-based testing.
     In Federation of International Conferences                [12] Koen Claessen and Michał H Pałka. Splittable
     on Software Technologies: Applications and                     pseudorandom number generators using cryp-
     Foundations, pages 196–206. Springer, 2016.                    tographic hashing. ACM SIGPLAN Notices,
                                                                    48(12):47–58, 2013.
 [2] Nasser Alzahrani, Maria Spichkova, and
     Jan Olaf Blech. From temporal models to                   [13] Arnaud Gotlieb and Bernard Botella. Auto-
     property-based testing. In Evaluation of Novel                 mated metamorphic testing. In Computer Soft-
     Approaches to Software Engineering, pages                      ware and Applications Conference, pages 34–
     241–246. SciTePress, 2017.                                     40. IEEE, 2003.
 [3] Andrew W Appel, Lennart Beringer, Adam                    [14] Paul Hudak, John Hughes, Simon Peyton Jones,
     Chlipala, Benjamin C Pierce, Zhong Shao,                       and Philip Wadler. A history of haskell: being
     Stephanie Weirich, and Steve Zdancewic. Po-                    lazy with class. In History of programming lan-
     sition paper: the science of deep specification.               guages, pages 12–1, 2007.
     Philos. Trans. R. Soc. A., 375(2104), 2017.               [15] John Hughes, Benjamin C Pierce, Thomas Arts,
 [4] Matthias Brun and Dmitriy Traytel. Generic au-                 and Ulf Norell. Mysteries of dropbox: property-
     thenticated data structures, formally. In Interac-             based testing of a distributed synchronization
     tive Theorem Proving, 2019.                                    service. In Software Testing, Verification and
                                                                    Validation, pages 135–145. IEEE, 2016.
 [5] FT Chan, TY Chen, Shing Chi Cheung, MF Lau,
     and SM Yiu. Application of metamorphic test-              [16] Daniel Jackson. Software Abstractions: logic,
     ing in numerical analysis. In Int. Conf. on Soft-              language, and analysis. MIT press, 2012.
     ware Engineering, 1998.                                   [17] Leslie Lamport. The temporal logic of actions.
 [6] Tsong Yueh Chen. Metamorphic testing: A sim-                   ACM Tran. on Programming Languages and
     ple method for alleviating the test oracle prob-               Systems, 16(3):872–923, 1994.
     lem. In Automation of Software Test, pages 53–            [18] Leslie Lamport. Specifying systems, volume
     54. IEEE, 2015.                                                388. Addison-Wesley Boston, 2002.
 [7] Tsong Yueh Chen, Fei-Ching Kuo, Huai Liu,                 [19] Huai Liu, Fei-Ching Kuo, Dave Towey, and
     Pak-Lok Poon, Dave Towey, T. H. Tse, and                       Tsong Yueh Chen. How effectively does meta-
     Zhi Quan Zhou. Metamorphic Testing: A Re-                      morphic testing alleviate the oracle problem?
     view of Challenges and Opportunities. ACM                      IEEE Transactions on Software Engineering,
     Computing Surveys, 51(1):1–27, April 2018.                     40(1):4–22, 2013.
[20] Huai Liu, Xuan Liu, and Tsong Yueh Chen. A             Evaluation of Novel Software Approaches to
     new method for constructing metamorphic rela-          Software Engineering, pages 396–402, 2016.
     tions. In Quality Software, pages 59–68. IEEE,    [32] Hong Zhu. Jfuzz: A tool for automated java unit
     2012.                                                  testing based on data mutation and metamorphic
[21] Johannes Mayer and Ralph Guderlei. An em-              testing methods. In Trustworthy Systems and
     pirical study on the selection of good metamor-        Their Applications, pages 8–15. IEEE, 2015.
     phic relations. In Computer Software and Appli-
     cations Conference, volume 1, pages 475–484.
     IEEE, 2006.
[22] Ralph C Merkle. A digital signature based on a
     conventional encryption function. In Theory and
     application of cryptographic techniques, pages
     369–378. Springer, 1987.
[23] Andrew Miller, Michael Hicks, Jonathan Katz,
     and Elaine Shi.     Authenticated data struc-
     tures, generically. ACM SIGPLAN Notices,
     49(1):411–423, 2014.
[24] S. Segura, D. Towey, Z. Q. Zhou, and T. Y.
     Chen.     Metamorphic testing: Testing the
     untestable. IEEE Software, 37(3):46–53, 2020.
[25] Maria Spichkova, Huai Liu, Mohsen Laali, and
     Heinz W Schmidt. Human factors in software
     reliability engineering. Workshop on Applica-
     tions of Human Error Research to Improve Soft-
     ware Engineering, 2015.
[26] Maria Spichkova and Milan Simic. Human-
     centred analysis of the dependencies within
     sets of proofs. Procedia computer science,
     112:2290–2298, 2017.
[27] Maria Spichkova and Anna Zamansky. Ahr:
     Human-centred aspects of test design. In Inter-
     national Conference on Evaluation of Novel Ap-
     proaches to Software Engineering, pages 111–
     128. Springer, 2016.
[28] Maria Spichkova and Anna Zamansky.        A
     human-centred framework for supporting agile
     model-based testing. In CAiSE Forum, pages
     105–112, 2016.
[29] Qiuming Tao, Wei Wu, Chen Zhao, and Wuwei
     Shen. An automatic testing approach for com-
     piler based on metamorphic testing technique.
     In Asia Pacific Software Engineering Confer-
     ence, pages 270–279. IEEE, 2010.
[30] Elaine J Weyuker. On testing non-testable pro-
     grams. The Computer Journal, 25(4):465–470,
     1982.
[31] Anna Zamansky, Guillermo Rodriguez-Navas,
     Mark Adams, and Maria Spichkova. Formal
     methods in collaborative projects. In Proceed-
     ings of the 11th International Conference on
