      Property-Based Testing: Climbing the Stairway to
                        Verification
                    Zilin Chen                                     Christine Rizkallah                                 Liam O’Connor
                UNSW Sydney                                      University of Melbourne                           University of Edinburgh
               Sydney, Australia                                   Melbourne, Australia                                Edinburgh, UK
       zilin.chen@student.unsw.edu.au                      christine.rizkallah@unimelb.edu.au                       l.oconnor@ed.ac.uk

                 Partha Susarla                                         Gerwin Klein                                    Gernot Heiser
              Melbourne, Australia                             Proofcraft and UNSW Sydney                               UNSW Sydney
              partha@spartha.org                                     Sydney, Australia                                 Sydney, Australia
                                                                   kleing@unsw.edu.au                                gernot@unsw.edu.au

                                                                      Gabriele Keller
                                                                     Utrecht University
                                                                    Utrecht, Netherlands
                                                                      g.k.keller@uu.nl

Abstract                                                                               Keywords: QuickCheck, functional programming, formal
Property-based testing (PBT) is a powerful tool that is widely                         verification, systems programming
available in modern programming languages. It has been                                 ACM Reference Format:
used to reduce formal software verification effort. We demon-                          Zilin Chen, Christine Rizkallah, Liam O’Connor, Partha Susarla,
strate how PBT can be used in conjunction with formal ver-                             Gerwin Klein, Gernot Heiser, and Gabriele Keller. 2022. Property-
ification to incrementally gain greater assurance in code                              Based Testing: Climbing the Stairway to Verification. In Proceedings
correctness by integrating PBT into the verification frame-                            of the 15th ACM SIGPLAN International Conference on Software
work of Cogent—a programming language equipped with                                    Language Engineering (SLE ’22), December 06–07, 2022, Auckland,
a certifying compiler for developing high-assurance systems                            New Zealand. ACM, New York, NY, USA, 14 pages. https://doi.org/
components. Specifically, for PBT and formal verification to                           10.1145/3567512.3567520
work in tandem, we structure the tests to mirror the refine-
ment proof that we used in Cogent’s verification framework:                            1    Introduction
The expected behaviour of the system under test is captured                            Property-based testing (PBT), in the style of QuickCheck [20],
by a functional correctness specification, which mimics the                            is a popular testing methodology and is supported in many
formal specification of the system, and we test the refinement                         modern programming languages [50]. In PBT, tests are spec-
relation between the implementation and the specification.                             ified using logical properties, which are automatically exe-
We exhibit the additional benefits that this mutualism brings                          cuted on randomly generated inputs in search of counter-
to developers and demonstrate the techniques we used in                                examples. PBT is not only useful in finding bugs in programs,
this style of PBT, by studying two concrete examples.                                  it has also been leveraged to reduce the effort in formal verifi-
                                                                                       cation [15, 29, 37, 47]. Subjecting code to extensive PBT prior
CCS Concepts: • Software and its engineering Software                                  to verification reduces the number of defects and specifica-
testing and debugging; Functionality; Formal software                                  tion inconsistencies, thus reducing verification cost. Proof
verification; Designing software.                                                      engineers can first test a property and only attempt to prove
                                                                                       it after having gained reasonable confidence in its validity.
                                                                                          In program verification, it is common practice to prove
Permission to make digital or hard copies of all or part of this work for              the correctness of a program against a formal specification.
personal or classroom use is granted without fee provided that copies are not
made or distributed for profit or commercial advantage and that copies bear            The specification can be given in various forms (e.g. state
this notice and the full citation on the first page. Copyrights for components         machines, process calculi, modal logics), depending on the
of this work owned by others than ACM must be honored. Abstracting with                application domain. To show that the implementation con-
credit is permitted. To copy otherwise, or republish, to post on servers or to         forms to the specification, the notion of refinement [7, 24, 52]
redistribute to lists, requires prior specific permission and/or a fee. Request        is frequently used to establish the formal connection.
permissions from permissions@acm.org.
SLE ’22, December 06–07, 2022, Auckland, New Zealand
                                                                                          In this work, we explore the combination of PBT and
© 2022 Association for Computing Machinery.                                            refinement-based formal verification. We borrow from veri-
ACM ISBN 978-1-4503-9919-7/22/12. . . $15.00                                           fication the functional correctness specification that is used to
https://doi.org/10.1145/3567512.3567520                                                dictate the behaviour of the system in question, and give it



                                                                                  84
SLE ’22, December 06–07, 2022, Auckland, New Zealand               Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


to PBT. Instead of testing logical properties about the sys-               We examine these benefits by integrating PBT into the
tem, which is what PBT is typically designed for, we test               Cogent framework. The BilbyFs file system [3], developed
the refinement relation between the implementation and                  in Cogent, provides an example of this effect. The entire Bil-
the specification. Using logical properties to describe the             byFs had been formally specified but only partially verified.
behaviour of a system has been criticised for its practicabil-          By applying PBT, we uncovered bugs in the specification and
ity [43], especially if the full functional correctness of the          the implementation of BilbyFs. PBT has therefore already
system is desired. Instead, high-level properties of a system           reduced the cost of verifying the remainder of the system by
can be proved on top of its functional specification.                   uncovering mistakes early on.
   We introduce PBT to our development cycle, parallel to                  This work builds on top of a preliminary investigation [18].
the refinement-based verification framework. Specifically,              To summarise, we make the following contributions:
we formulate the refinement between the implementation                       • We demonstrate how to integrate PBT into a refine-
and the functional specification as the property to be tested,                 ment verification framework by using Cogent as the
which is an under-explored application of PBT. Employing                       target platform. Unlike previous use of PBT, our test
PBT in the formal verification context brings additional ben-                  specification is defined in terms of refinement proper-
efits beyond detecting bugs in the implementation of the                       ties (Section 3).
systems.                                                                     • We argue why PBT is suitable to be employed in paral-
   In contrast to the high-effort all-or-nothing of a full func-               lel with formal verification, and explain the important
tional correctness proof, PBT provides a continuum ranging                     role that PBT plays in the design and implementation
from no assurance (no tests), to some assurance (good test                     of the systems (Section 4).
coverage), to better assurance (some properties proved, some                 • We provide two concrete examples from the testing of
tested), and all the way to high assurance (all properties                     components of the BilbyFs file system to demonstrate
proved). This allows users to make trade-offs between cost                     techniques that we used for specifying refinement re-
and assurance according to the criticality of a component.                     lations, modularising the tests, using mocks, handling
   Tests are more immune to program evolution than formal                      non-determinism, and efficiently generating test data
proofs. A proof may require significant changes whenever                       (Section 5 and Section 6).
the code changes, even in scenarios where the specifica-                     • We discuss the engineering implications of our ap-
tion remains the same (e.g. optimisation). On the contrary,                    proach and lessons learnt and proposals resulting from
PBT only requires developers’ input when the specification                     them (Section 7).
changes. Therefore, PBT can provide quicker feedback on
the correctness of the change, reducing code maintenance
                                                                        2     Background
cost. Furthermore, all proofs depend on assumptions such as
the correctness of the hardware or the external software in-            2.1 Cogent
volved. Some of these assumptions can be tested to increase             From the experience of formally verifying the seL4 microker-
the correctness of the overall system.                                  nel, Klein et al. [41] have observed that the proofs connecting
   It is usually challenging to verify software that was not            the high-level specifications with the low-level C systems
designed for verification, as the code has to be structured in          code are time consuming and tedious to develop, but are
a modular fashion, around clearly stated correctness prop-              not particularly involved. As such they are good candidates
erties. This means that it is vital to have an effective means          for automation. The Cogent verification framework was
for developers to express their design requirements in order            conceived to partly automate these proofs.
to experiment with and evaluate their design, and to have a                Cogent [55, 56, 58] is a purely functional language
good set of design guidelines [14] for them to write programs           that was developed to reduce the cost of developing high-
that can be readily specified and verified.                             assurance systems components. Similar to the Rust lan-
   In large-scale software verification projects, such as               guage [39], Cogent is equipped with a uniqueness type sys-
seL4 [41], systems developers and verification experts are              tem [8, 11, 25, 66] that ensures memory safety, easing the bur-
typically from two separate teams. We posit that PBT specifi-           den of verification. Cogent’s type system allows imperative-
cations can be used to enhance the communication between                style destructive updates, while retaining a purely functional
these two groups. While the properties are similar to formal            semantics. The type system eliminates the need for a garbage
specifications, they represent tests and, as such, feel more            collector, making the language more suitable for systems
familiar to software engineers than abstract proof require-             code and also easier to verify.
ments. Since PBT gives almost immediate benefit to software                The uniqueness types come at a cost: it is impossible in
engineers, there is an incentive for them to design their code          Cogent to implement data structures and functions which,
such that these properties are meaningful and easy to ex-               even temporarily, rely on sharing. Instead, they have to be
press, thereby structuring their code for formal specification,         implemented in C, verified separately, and imported as ab-
making it amenable to verification.                                     stract types and abstract functions through a foreign function



                                                                   85
Property-Based Testing: Climbing the Stairway to Verification                                         SLE ’22, December 06–07, 2022, Auckland, New Zealand


          manual       legend                                                         1 type H
                                      Functional specification (Isabelle/HOL)         2 type Bag = { count : U32, sum : U32 }
          generated
               proof                                                                  3 newBag : H → <Success (Bag, H) | Failure H >
                                                                                      4 freeBag : (H, Bag) → H




                                               re nes
                                                                                      5
        COGENT
        source                                                                        6 addToBag : (U32, Bag) → Bag
                          generates   Shallow embedding of                            7 addToBag (x, b { count = c, sum = s })




                                                                       re nes
                                      COGENT in Isabelle/HOL
                                                                                      8    = b { count = c + 1, sum = s + x }
         COGENT                                                                       9


                                               re nes
                          generates
        compiler                                                                     10 averageBag : Bag! → <Success U32 | EmptyBag >
                                                                                     11 averageBag b = if b.count == 0 then EmptyBag
                          generates                                                  12                  else Success (b.sum / b.count)
                                                 C                 C library
                                                                                     13
   fi
                                                                                     14 type List a
                                                                                     15 reduce : ∀ (a, b). ((List a)!, (a!,b) → b, b) → b
Figure 1. An overview of Cogent’s verification framework                             16
                                                                                     17 average : (H, (List U32)!) → (H, U32)
                                                                                     18 average (h, ls) = newBag h

interface (FFI) that requires the uniqueness constraints to                          19    | Success (b, h') →
                                                                                     20        let b' = reduce (ls, addToBag, b)
be satisfied at the interface level. Besides, Cogent does not                        21         in averageBag b' !b'
natively support loops or recursion; they also need to be                            22            | Success n → (freeBag (h', b'), n)
implemented in C. We refer to this collection of C code as                           23            | EmptyBag → (freeBag (h', b'), 0)
the C library.                                                                       24    | Failure h' → (h',0)

   Cogent’s certifying compiler [58, 59], presented in Fig-
ure 1, generates C code, a shallow embedding of the Cogent                                 Figure 2. A simple example of a Cogent program
code in the interactive theorem prover Isabelle/HOL [54],
and a proof connecting the two. The generated proof ensures
that the C code correctly refines the Isabelle/HOL shallow                           similar to Haskell’s IO monad. The newBag function returns a
embedding. As such any correctness properties proved about                           variant (or sum) type to indicate the possibility of allocation
the shallow embedding also hold for the C code. Automating                           failure. The addToBag function, which adds a new data point
the refinement proof from Cogent to C drastically reduced                            to the bag, is defined on lines 6–8. The averageBag function
the verification effort required compared to directly verifying                      (lines 10–12) returns, if possible, the average of the numbers
C code [4].                                                                          added to the Bag. The input type Bag! indicates that the input
   While the Cogent compiler generates C refinement proofs                           is a read-only, non-unique view of a Bag, which is created
automatically, it cannot prove full functional correctness,                          on line 21 using the ! notation. Lastly, lines 17–24 define the
which is specified manually by the developer in a functional                         overall average function, which uses the Bag to compute the
correctness specification in Isabelle/HOL. This leaves two                           average of the elements of a List.
steps that require manual verification (the two solid arrows
in Figure 1): (1) verifying that the purely functional shallow                       2.2    Property-Based Testing and QuickCheck
embedding of the Cogent code refines the overall functional                          PBT is a quick and effective method for detecting bugs and
correctness specification, and (2) verifying that each C ADT                         finding inconsistencies in specifications [38]. Similar to for-
refines its functional specification. The former, albeit manual,                     mal verification, PBT uses logical predicates to specify the
is eased by virtue of equational reasoning. The latter proof,                        desired behaviour of functions, by defining the allowed rela-
which is directly on the C level, is more involved. However,                         tions between inputs and outputs of the functions. It evalu-
the C library is to be shared across multiple systems and                            ates the properties on a large set of automatically generated
hence the effort is amortised over time.                                             input values in search of counter-examples.
   Figure 2 provides an example of a Cogent program. Given                              While PBT is effective, it is not universally applicable—in
an abstract List datatype with a reduce function (line 15) that                      practice, it is often hard to describe the full behaviour of
aggregates the List content using a provided aggregation                             a system solely in terms of logical properties [43]. In the
function and identity element, the function average (line 17)                        context of formal verification, however, using a functional
computes the average of a list of 32-bit unsigned integers. It                       specification to describe the behaviour of a systems is very
accomplishes this by storing the running total and count in a                        common. Thus proof engineers can first run extensive tests
heap-allocated data structure, called a Bag, defined on line 2,                      on the conjectures before attempting any proof development.
with external allocation and free functions on lines 3 and 4.                        This technique is not new and has witnessed great success
Because Cogent is a purely functional language, intrinsically                        in the verification community [10].
impure functions, like the memory (de-)allocation functions,                            QuickCheck [20] is a combinator library in Haskell for
need to have the heap H threaded through them. This is                               PBT. While the QuickCheck functionality is now available



                                                                                86
SLE ’22, December 06–07, 2022, Auckland, New Zealand               Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


in many programming languages [50] and theorem provers                             manual      legend
                                                                                                                Executable specification (Haskell)
[15, 29, 47], we interface Cogent to the Haskell QuickCheck                        generated
library, as it is mature, feature-rich and integrates well with                     testing




                                                                                                                        re nes
Cogent and C.                                                                                                                    (1)
                                                                                 COGENT
                                                                                 source




                                                                                                                                       re nes
                                                                                                  generates   Shallow embedding of
                                                                                                                                                (3)




                                                                                                                                                         re nes
2.3   Data Refinement                                                                                           COGENT in Haskell                                 (2)

Prior verification work in Cogent, e.g. of BilbyFs [3], con-                      COGENT




                                                                                                                        re nes
nects the functional specification to the Cogent implemen-                       compiler                                        (4)
tation, and the Cogent implementation to the compiled C
                                                                                                  generates
code [59] by proving refinement relations. The notation of                                                                C                           C library
refinement is also central to our testing framework, in which               fi



they are expressed as QuickCheck properties. We use a text-
                                                                        Figure 3. An overview of the Cogent QuickCheck frame-
book definition of refinement [24]. Informally, a program 𝐶
                                                                        work
is a refinement of a program 𝐴 if every possible behaviour in
the model of 𝐶 is observable in that of 𝐴.
   In an imperative setting, a simple model for both the ab-            statement merely requires the single concrete result to cor-
stract specification and the concrete implementation would              respond to one of the possible abstract results:
be relations on states, describing every possible behaviour of                        𝑅𝑋 𝑖𝑎 𝑖𝑐 =⇒ ∃𝑜 𝑎 ∈ abs 𝑖𝑎 . 𝑅𝑌 𝑜 𝑎 (conc 𝑖𝑐 )
the program as the manipulation of some global state. This
means that if we prove a property about every execution for             Defining the notation
our abstract specification, we know that the property holds                                                       def
                                                                                                  corres 𝑅 𝑎 𝑐 = ∃𝑜 ∈ 𝑎. 𝑅 𝑜 𝑐
for all executions of our concrete implementation.
   This state-based model for specifying the behaviours of              the refinement statement can be formulated as:
systems is a very common paradigm in the world of model-                                𝑅𝑋 𝑖𝑎 𝑖𝑐 =⇒ corres 𝑅𝑌 (abs 𝑖𝑎 ) (conc 𝑖𝑐 )
based testing (MBT) [33, 43, 64]. However, as mentioned in              Theorems that capture the functional correctness of Cogent
Section 1, Cogent’s purely functional semantics provides                systems typically have this corres format. We therefore aim to
a simple formal model of a program’s behaviour; specifi-                encode these as machine-testable properties in QuickCheck.
cally, it enables reasoning about programs using equational
principles. The equational semantics is fortunately widely              3        The Cogent QuickCheck Framework
available in PBT libraries, including QuickCheck.
                                                                        The integration of PBT into the Cogent framework mirrors
   Since Cogent is a purely functional, deterministic, total
                                                                        the verification tasks, as shown in Figure 3. The developer
language, there is no global state, and all functions are mod-
                                                                        manually writes a Haskell executable specification, which
elled as plain mathematical functions. In such a scenario,
                                                                        plays a similar role to the Isabelle/HOL functional correct-
the only state involved consists of the inputs and outputs to
                                                                        ness specification. The compiler now generates a Haskell
the function, simplifying the refinement statement. Given
                                                                        shallow embedding of the Cogent code for PBT. Although
an abstract function abs :: 𝑋𝑎 → 𝑌𝑎 , and a concrete Cogent
                                                                        not formally connected, the Haskell and Isabelle/HOL em-
function conc :: 𝑋𝑐 → 𝑌𝑐 , then, assuming the existence of re-
                                                                        beddings are very similar.
finement relations 𝑅𝑋 and 𝑅𝑌 , we can express the statement
                                                                           The framework supports testing the C implementation of
that conc refines abs as:
                                                                        ADTs against the Haskell executable specification, shown as
                                                                        arrow (2) in Figure 3; Section 5 provides an example. It fur-
              𝑅𝑋 𝑖𝑎 𝑖𝑐 =⇒ 𝑅𝑌 (abs 𝑖𝑎 ) (conc 𝑖𝑐 )                       thermore supports testing the Cogent program along with
                                                                        ADTs that the Cogent program uses, against the Haskell exe-
This, however, places unnecessary constraints on our ab-                cutable specification. This is depicted as arrow (1) in Figure 3
stract specification. While Cogent is deterministic and total,          (the included ADTs are not shown in the figure); Section 6
our abstract specification need not be. In fact, it is often de-        provides a case-study. The included ADTs can either be real
sirable to allow non-determinism to reduce the complexity               C implementations (via Haskell’s C FFI) or Haskell mocks,
of the abstract specification. In the context of testing, we are        depending on whether the ADTs are also considered the
required to restrain the degree of non-determinism in the               system under test.
specification, for the sake of efficient execution of the test             The refinement relation between the C code and the
script. This, however, does not preclude us from having a               Haskell embedding of the Cogent program (arrow (4)) can
non-deterministic specification.                                        also be tested, although it does not concern us as much, since
   We model non-determinism by allowing abstract func-                  it is certified by the automatic proof. One scenario where
tions to return a set of possible results. Then, our refinement         this test can be beneficial is during the development of the



                                                                   87
Property-Based Testing: Climbing the Stairway to Verification                          SLE ’22, December 06–07, 2022, Auckland, New Zealand


Cogent compiler, before the automatic refinement proof                  when the Isabelle/HOL specification is developed prior to the
pipeline is fully restored.                                             Haskell executable specification. This however is not always
   The complete compiled executable, depicted in Figure 3               the case, and in fact in the workflow that we proposed, the
as the grey dotted box at the bottom, can be tested against             Haskell specification is used to guide the formulation of the
the executable specification in theory, as indicated by arrow           Isabelle/HOL one.
(3). However, we typically do not perform this test using
the QuickCheck framework in Cogent, as the gap between
their state spaces is usually too large to handle effectively.
                                                                        4   PBT and Systems Design Go
The final system can normally be deployed in the production                 Hand-in-Hand
environment and be tested against third-party test suites               We argue that the employment of PBT and the design of the
for their specific application domain. In the context of the            systems are interlinked with each other: appropriate systems
BilbyFs, for example, there exist tools such as fstest [9].             design assures the effectiveness of testing, and the use of
   On the formal verification end, the Isabelle/HOL func-               PBT encourages the programmers to design their systems in
tional correctness specification may be highly non-                     a fashion that is amenable to formal verification.
deterministic in order to succinctly characterise external fac-            As a purely functional language, Cogent is well suited
tors such as the elapsed time of an operation, out-of-memory            for PBT and verification: the result of a executing a function
errors or hardware errors. The Haskell specification must               only depends on the input, with no hidden state. Instead, a
also be capable of modelling non-determinism, but in a more             system state must be explicitly threaded through an impure
controlled manner, as the specification must be executable.             function. If the function is not designed appropriately, it is
Simulating a non-deterministic model can be exponential                 possible that a PBT test suite hardly yields counter-examples.
in time and space. To allow modelling a minimal amount                  Systems code often involves large global states. However, a
of non-determinism in the Haskell specification, the tester             function typically only accesses a small portion of the state.
has to ensure that the search domain is finite and reasonably           If the entire state is passed in, any random variations to the
small by carefully examining the needed quantifiers in the              parts of the state that are irrelevant to the function will have
specification.                                                          no effect on the execution of the function. In this case a large
   For example, in the Isabelle/HOL abstract specification              proportion of the randomly generated test cases in PBT will
of BilbyFs, the afs_get_current_time function is defined as             be wasted, rendering the test suite ineffective.
follows:                                                                   In practice, this means that to be suitable for PBT, the
  definition                                                            functions must be designed to keep the inputs minimal and
    afs_get_current_time :: afs_state ⇒ (afs_state ×                    relevant, which is unlikely when naïvely translating exist-
       TimeT) cogent_monad                                              ing C code with global state into Cogent. While this may
  where
    afs_get_current_time afs ≡ do
                                                                        seem like a high price to pay, a verification-friendly design
       time ′ ← return (a_current_time afs);                            has the same requirement for modularity and compartmen-
       time ← select {x. x ≥ time ′ };                                  talisation [3, 5]. Thus PBT imposes few restrictions beyond
       return (afsL a_current_time := time M, time ′ )                  existing requirements of verification, and instead helps guide
     od                                                                 the design.
It non-deterministically picks a time, which is no earlier than            In the context of Cogent, developers typically do not have
the time stored in the file system state afs. This abstract             a formal specification to begin with when implementing a
specification is not suitable for testing, due to the infinitely        new system. Systems programmers, together with verifica-
large set of values. In contrast, on line 13 of Figure 5b, the          tion experts, not only need to ensure that they are imple-
specification non-deterministically chooses an error code               menting the systems right, but also to ensure that they are
from a small set of {eIO, eNoMem, eInval, eBadF, eNoEnt}.               implementing the right systems. PBT helps them structure
This moderate state explosion can potentially be handled by             the implementation, as well as the specification. Having
the testing framework, depending on the context in which                good design decisions, such as keeping the states threaded
the afs_readpage function is applied.                                   through small and relevant as we mentioned above, is dou-
   The Haskell executable specification is thus often strictly          bly rewarding: it keeps the refinement relation between the
less abstract than the Isabelle/HOL functional specification.           concrete and the abstract states simple, both in PBT and in
Although it is not necessary to formally connect the two,               verification.
as the gap only affects the quality of the tests, ideally we               Expressing design requirements for verification is an on-
would want one specification to be generated from the                   going challenge, and we observed in the past that when veri-
other one. Automatic refinement mechanisms that allow                   fying real-world systems, it is difficult for proof engineers to
verified generation of Haskell from Isabelle/HOL have been              communicate these requirements effectively to the software
explored [44, 45]. Generating the Haskell specification from            engineers. The seL4 project [41] overcame this problem by
the Isabelle/HOL abstract specification is undoubtedly handy,           using an executable Haskell specification of the system as



                                                                   88
SLE ’22, December 06–07, 2022, Auckland, New Zealand             Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


    prop_corres_wordarray_set_u8 :: Property                          the polymorphic wordarray_set function, whose refinement
    prop_corres_wordarray_set_u8 = monadicIO $                        statement is given in Figure 4. It can be read roughly as:
      forAllM gen_wordarray_set_u8_arg $ \args → run $ do
                                                                      for any type-correct concrete input ic and its abstraction
        let ia = mk_hs_wordarray_set_u8_arg args
            oa = uncurry4 hs_wordarray_set ia
                                                                      ia, check that the result (i.e. oc) of applying the concrete
        ic ← mk_c_wordarray_set_u8_arg args                           function cogent_wordarray_set_u8 and that of the abstract
        oc ← cogent_wordarray_set_u8 ic                               function hs_wordarray_set (i.e. oa) are related via the refine-
        corresM' rel_wordarray_u8 oa oc                               ment relation rel_wordarray_u8. The corresM' function is a
                                                                      monadic variant of our corres notation for situations where
Figure 4. The refinement statement for wordarray_set (de-             the specification is deterministic.
allocation is omitted for simplicity)                                     Although the corres predicate contains an existential quan-
                                                                      tifier for the result of the non-deterministic abstract specifi-
                                                                      cation, our implementation does not require QuickCheck to
an interface between these two groups [40]. We posit that             guess the quantified value from a set of all possible values.
QuickCheck properties is a highly suitable language for com-          Instead, our test driver enumerates over all possible output
municating design requirements. They readily translate to             values of the abstract function to find the existentially quan-
formal specifications, but are expressed in a programming             tified value. In Section 6, we show how to restrict the size of
language, and thus familiar to software developers. As they           the abstract function’s codomain for the enumeration to be
lead to effective test generation, software developers get im-        tractable.
mediate benefit from using these specifications to structure              For the WordArray type, we relate the abstract input data
their code to maximize their use, which consequently makes            and the concrete input data in the following way: we ran-
the code easier to verify.                                            domly generate test data on a middle-ground type, and
                                                                      then use two thin wrappers mk_hs_wordarray_set_u8_arg
5     Example: The WordArray Library                                  and mk_c_wordarray_set_u8_arg to convert the generated
We apply the Cogent QuickCheck framework to the                       data to the types expected by the abstract and the concrete
WordArray library, which implements common functions ma-              functions. The test data generation is not very involved, be-
nipulating arrays of machine words and is shared by all               cause the correspondence between the two types is straight-
of our systems implementations. Most of these WordArray               forward, and the C type is not very convoluted in its under-
functions are implemented in C, and are invoked via the FFI           lying representation, in particular it does not heavily use
mechanism available in Cogent.                                        pointers.
   We want to test whether each function observes the refine-             Although in the refinement statement, the refinement re-
ment property from Section 2.3. For example, the behaviour            lation between the input data is expressed as a predicate, this
of the ADT function wordarray_set (similar to memset in C)—           is usually not the way to implement the test driver. Checking
which fills the first n elements starting at a certain index          a predicate is often straightforward, but it requires two sets
frm into an array arr with a constant value a—is manually             of random data generators and forces the two generators to
specified in Haskell as follows:                                      be coupled. Otherwise the correspondence predicate is likely
    -- Haskell spec.                                                  to reject the vast majority of the generated data, rendering
    type WordArray a = [a]                                            the test very inefficient (see Section 7.4).
    hs_wordarray_set :: WordArray a → Word32 → Word32                     Broadly speaking, it is more convenient to relate the input
                      → a → WordArray a                               data if we implement the refinement relation as an abstrac-
    hs_wordarray_set arr frm n a =
      let len = length arr in                                         tion function, computing the abstract data according to its
       if | frm > len = arr                                           concrete counterpart. This is contrary to model-based testing
          | frm + n > len                                             approaches [64], in which the test cases are derived from the
          = take frm arr ++ replicate (len - frm) a                   more abstract model. We use abstraction functions because
          | otherwise
          = take frm arr ++ replicate n a ++
                                                                      typically the concrete state contains more data than its ab-
            drop (frm + n) arr                                        stract counterpart. In order to derive a concrete input from
                                                                      the randomly generated abstract input, more data need to be
In Cogent, the function is defined as an abstract function,
                                                                      created and this calls for another set of random data genera-
whose definition is given in C. The Cogent function inter-
                                                                      tors. On the other hand, when we generate a concrete input
face looks like:
                                                                      and abstract it, it only requires a lossy abstraction function.
    type WordArray a                                                      In the case of WordArray, we compute the abstract in-
    wordarray_set : (WordArray a, U32, U32, a) → WordArray a
                                                                      put data from the concrete one, relating them by construc-
While Cogent and Haskell both support polymorphism, C                 tion. However, not all values of a C type are valid inputs:
does not, and QuickCheck cannot perform genuine polymor-              for instance, a null pointer does not correspond to a valid
phic testing [12]. In this example, we test the U8 instance of



                                                                 89
Property-Based Testing: Climbing the Stairway to Verification                          SLE ’22, December 06–07, 2022, Auckland, New Zealand


WordArray. To exclude invalid input data, we manually im-               memcpy in C), the old implementation implicitly assumed that
plement a test data generator gen_wordarray_set_u8_args                 the index into the source array was always within bounds.
which generates values that are isomorphic to valid con-                This precondition was satisfied by our file system implemen-
crete inputs only, and we convert them to Haskell inputs and            tations, but it was unspecified. In fact, the wordarray_copy
C inputs using functions mk_hs_wordarray_set_u8_arg and                 function, as part of a generic library, should not carry this
mk_c_wordarray_set_u8_arg respectively.                                 implicit precondition. Otherwise it may introduce bugs to
   The refinement statement as shown in Figure 4 is largely             other customers of this library function but do not perform
boilerplate code. To generate this code, we designed a small            the check.
domain-specific language (DSL), whose prototype has been                   PBT also helped us uncover problems in the Isabelle/HOL
implemented [27]. In this DSL, programmers can specify the              ADT specifications, which had overly specific assumptions
function names, the definition of the abstraction function for          about inputs. While these assumptions are valid for the func-
the inputs and the refinement relation between the outputs,             tions we verified, they do not hold in general. Thus, the
and other properties about the refinement statement, such               specifications we had written did not represent a general
as the determinism of the abstract function and whether                 purpose specification of the function.
the concrete function needs to operate under the IO monad.                 The WordArray library in Cogent was initially axiomatised
The DSL is written in JSON format, which can be readily                 in the verification of the file systems [4], and then tested
parsed using third-party libraries such as aeson [57]. A piece          using the PBT framework, before they were finally formally
of sample code is give below:                                           verified [19]. This is an example of how the developers can
                                                                        progressively increase their confidence in the correctness
1 {
2     "name" : "wordarray_set_u8",                                      of the code by upgrading PBT to formal verification in a
3     "monad" : true,                                                   modular fashion.
4     "nondet": false,
5     "absf" : ... // the abstraction function
6     "rrel" : ... // ref. rel. between outputs
                                                                        6     Example: A Top-Level File System
7 }                                                                           Operation
Haskell program texts can be embedded in the JSON struc-                BilbyFs [3] is a flash file system that was designed from
ture as the values of the "absf" and "rrel" attributes (lines           scratch, focusing on modularity and verifiability; it has 19
5 and 6). This allows programmers to either call a Haskell              top-level file system operations. Two functions have been
function defined elsewhere, or directly write the definition            previously verified in Isabelle/HOL to demonstrate how Co-
in-place. The lens [42] style of code is particularly suitable          gent facilitates equational reasoning. fsop_sync, a top-level
for accessing and relating parts of deeply nested algebraic             function, consists of about 300 lines of Cogent code and
datatypes.                                                              took approximately 3.75 person months to verify with 5700
   In the refinement statement, the Cogent-compiled C code              lines of proof. The other function, iget, directly called by the
can be called from Haskell using its C FFI facility. The Haskell        top-level fsop_lookup function, consists of approximately
representation of C types, marshalling functions, and foreign           200 lines of code, and took about one person month to verify
function calls are generated by the Cogent compiler and                 with 1800 lines of proof.
are further compiled by FFI tools such as hsc2hs [32] and                  We conducted PBT on one of BilbyFs’s top-level func-
c2hs [16].                                                              tion fsop_readpage [17], which had previously been formally
   Running a small number of randomly generated tests                   specified in Isabelle/HOL but not yet verified. Figure 5 shows
(by default 100 but this can be customised) by passing                  the Isabelle/HOL specification as well as the manually writ-
prop_corres_wordarray_set_u8 to the quickCheck function,                ten Haskell executable specification; they are very similar in
we get:                                                                 this case. Therefore, testing gives us reasonably high assur-
*WordArray> quickCheck prop_corres_wordarray_set_u8                     ance of the implementation with respect to the Isabelle/HOL
+++ OK, passed 100 tests.                                               specification. As discussed in Section 3 , this is not always
We have specified most of the ADT functions for WordArrays              the case, making it occasionally more difficult to connect
and tested them [17]. We found bugs in two C functions,                 the two specifications, and sometimes requiring additional
which had not been uncovered by our earlier test suites nor             manual reasoning.
the file systems built with them. The bugs went undetected
as they involved invalid inputs and corner cases which were             6.1   The Haskell Executable Specification
handled by the callers, whereas the Haskell specification in            In a nutshell, as shown in the Haskell specification in Fig-
our QuickCheck framework does not preclude these input                  ure 5a, the function hs_fsop_readpage fetches a designated
values.                                                                 data block of a specific file to the buffer. The argument afs is
   For example, for the wordarray_copy function that copies a           a map from inode numbers to files; each file is represented as
number of bytes from one memory area to another (similar to             a list of blocks of data. The hs_fsop_readpage function looks



                                                                   90
SLE ’22, December 06–07, 2022, Auckland, New Zealand                Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


 1 hs_fsop_readpage :: AfsState
 2                    → VfsInode
 3                    → OSPageOffset
 4                    → WordArray U8
 5                    → NonDet (Either ErrCode (WordArray U8))
 6 hs_fsop_readpage afs vnode n buf =
 7    let size = vfs_inode_get_size vnode :: U64
 8        limit = size `shiftR` bilbyFsBlockShift
 9     in if | n > limit → return $ Left eNoEnt
10           | n == limit && (size `mod` bilbyFsBlockSize == 0) →
11               return $ Right buf
12           | otherwise → return (Right $ fromJust (M.lookup (vfs_inode_get_ino inode) afs) !! n) <|>
13                          (Left <$> [eIO, eNoMem, eInval, eBadF, eNoEnt])

                                                  (a) The Haskell executable specification

 1 definition
 2     afs_readpage :: afs_state
 3                  ⇒ vnode
 4                  ⇒ U64
 5                  ⇒ U8 WordArray
 6                  ⇒ (U8 WordArray × (unit, ErrCode) R) cogent_monad
 7   where
 8     afs_readpage afs vnode n buf ≡
 9      if n > (v_size vnode >> unat bilbyFsBlockShift) then
10       return (WordArrayT.make (replicate (unat bilbyFsBlockSize) 0), Error eNoEnt)
11      else if (n = (v_size vnode >> unat bilbyFsBlockShift)) ∧ ((v_size vnode) mod (ucast bilbyFsBlockSize) = 0)
12           then return (buf, Success ())
13           else do err ← {eIO, eNoMem, eInval, eBadF, eNoEnt};
14                   return (WordArray.make (pad_block ((i_data (the $ updated_afs afs (v_ino vnode))) ! unat n)
          bilbyFsBlockSize), Success ()) ⊓
15                   return (buf, Error err)
16                od

                                                (b) The Isabelle/HOL functional specification

                                 Figure 5. Functional specifications of the fsop_readpage function

up a file, whose inode number is given by vnode, in the map               here is essentially a finite set containing all allowed be-
afs, and copies the n-th block of the file to buf. It returns             haviours. This monad is commonly used in proving refine-
non-deterministically an updated buffer or an error code.                 ment (e.g. [3, 22]). The alternative operator (<|>) acts as a
   As a first step, hs_fsop_readpage calculates the number of             non-deterministic choice, admitting the behaviour of either
blocks that the wanted file occupies. If the block in question            of its operands by taking the union of their behaviours.
is out of bounds (n > limit), the function returns a no-entry
error eNoEnt. If the file size is a multiple of the block size,
n points to the last block in the wanted file, and the last               6.2   Mock Implementations
block is empty (because the file data ends at the prior block
                                                                          It is not always feasible to test systems code in its exact pro-
boundary), then the function returns the original buffer as
                                                                          duction environment [53]. For instance, the fsop_readpage
there is no data to read. Otherwise, hs_fsop_readpage reads
                                                                          example has many low-level functions which call into the
the block by looking up the inode number in the map (see
                                                                          operating system’s kernel, and it is currently not feasible to
Figure 6 for a pictorial example).
                                                                          run QuickCheck tests in kernel mode. Instead of testing the
   This, however, is not the only possible correct behaviour.
                                                                          monolithic object file obtained from compiling the C code,
As the implementation has to access buffers and read from
                                                                          we mock up parts of the code in Haskell. A mock abstracts
the physical medium, this may fail, in which case it should
                                                                          from low-level kernel calls and can be thought of as a black
throw an error. We specify this as a non-deterministic be-
                                                                          box, which provides to its caller the same observable effects
haviour. The specification states that the function can read
                                                                          as the actual implementation.
a block or it can give one of the following five errors: eIO,
                                                                              Mocks can also be used as substitutes for unimplemented
eNoMem, eInval, eBadF, or eNoEnt. The NonDet monad used
                                                                          functions, enabling systems developers to test functionality
                                                                          before they have a full system implementation. The use of



                                                                     91
Property-Based Testing: Climbing the Stairway to Verification                           SLE ’22, December 06–07, 2022, Auckland, New Zealand


                            data                                      the mock to the specific use case of fsop_readpage. The
                                                                      mock ostore_read function can be modelled as a simple map
                                                           (A)        lookup: given a map OstoreState and a key of type ObjId, it
                                                                      returns the corresponding object or an error. The relevant
           block 0      block 1      block 2     block 3              Haskell definitions are given as follows (the use of the Oracle
                                                                      can be ignored for now; it will be explained shortly):
                                                           (B)
                                                                         type OstoreState = Map ObjId Obj
                                                                         data Res a e = Success a | Error e
                          data
                                                                         ostore_read :: Oracle
Figure 6. An example of the read_page algorithm. In case                    → (OstoreState, ObjId) → Res Obj ErrCode
(A), limit = 3. When n = 0, 1, 2 we just read. When n = 3,               ostore_read orc (ostore_st, oid) =
                                                                           if orc == 0 then
because the size of the data is not perfectly aligned at the                 case M.lookup oid ostore_st of
end, we still read. When n ≥ 4, we return the no-entry error.                  Nothing → Error eNoEnt
In case (B), limit = 3. When n = 3, that’s the special case.                   Just obj → Success obj
We return the old buffer unmodified.                                       else Error orc


                                                                      6.3    Oracles and Non-determinism
mocks restricts the scope of debugging to a small number of
functions, reducing the effort required to locate bugs.               The Cogent implementation of ostore_read interacts with
   The Cogent implementation of fsop_readpage calls a                 the physical media and kernel data structures, therefore its
read_block function to fetch one block of file data, which in         behaviour is dependent on that of the underlying systems
turn retrieves the data with the function ostore_read. The            and hardware. However, as we have introduced in Section 2.1,
read_block function, which retrieves the file data from the           Cogent is a total, purely functional language, meaning that
physical medium, is conceptually simple. However it is com-           all functions in Cogent have to be deterministic. This non-
plicated in its internal implementation, which involves a             determinism, therefore, has to be modelled by threading a
red-black tree lookup to locate the address, several layers of        global state SysState through the impure functions, similar
caching, and thorough error-handling.                                 to the H type in Figure 2.
   Because read_block relies on kernel mode access to caches             In the Haskell mock implementation of ostore_read, the
and complex data structures, it is a good candidate for a             non-determinism can be modelled in a different manner for
mock implementation. In addition to the ostore_read func-             simplicity. When testing this function independently, we
tion, we also substitute some kernel ADT functions for                emulate the non-determinism by adding an additional oracle
mock implementations. For WordArray functions invoked                 input orc.1 This oracle can be deemed to be the source of all
by fsop_readpage, we use the Haskell models described in              non-determinism. A similar oracle is passed to our mocks of
Section 5 as mocks.                                                   many WordArray functions, such as wordarray_create, which
   The implementation of a mock is simplified by the fact             allocates memory and creates a fresh array.
that it does not need to provide the full functionality of the           We have seen how oracles can be used in mock implemen-
operation, as long as the callers in the specific test cases          tations to emulate non-determinism. The oracle technique
cannot observe the difference in its behaviours.                      can be similarly applied to the Haskell executable specifi-
   For example, the original Cogent signature of the function         cation. When we test that an oracle-carrying mock refines
ostore_read is:                                                       a non-deterministic specification, the specification can ab-
  type RR x a e = (x, <Success a | Error e>)
                                                                      stract over the values that the oracle can possibly possess
  ostore_read : (SysState, MountState!, OstoreState, ObjId)           with the NonDet monad. If the specification is to be made
             → RR (SysState, OstoreState) Obj ErrCode                 more precise, we can also introduce an oracle to it to ascribe
The function takes a quadruple as input, containing a read-           the source of the non-determinism. In this case, care needs
only (denoted by the ! operator) MountState, and returns the          to be taken to ensure that the oracle in the specification and
parametric RR type, which is further defined as a pair of a           that in the implementation are in synchronisation, so that
variant type <Success a | Error e> and a result type x that           they do not make conflicting choices.
is common to both cases.                                                 Using oracles in the specification can be problematic if
   The purely functional nature of Cogent makes it easy               the implementation is not a mock and is genuinely non-
for developers to identify the observable behaviours—they             deterministic due to, say, the hardware or the operating sys-
are necessarily within the return type of a function. In the          tem. There is in general no way to predict accurately which
case of the fsop_readpage function, the only behaviours               1 In our implementation, we pass the oracle around using GHC Haskell’s
of ostore_read that can be observed are the returned Obj              implicit parameter extension [48], making it more transparent to users. In
value or the error code ErrCode. Therefore, we can tailor             the presentation of this paper, however, we pass them explicitly for clarity.




                                                                 92
SLE ’22, December 06–07, 2022, Auckland, New Zealand                Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


execution path the concrete implementation will take (e.g.               6.5    Results
malloc failures). Hence, the specification and the implemen-             The shape of the top-level refinement statement for the
tation can make inconsistent choices when they encounter                 Haskell shallow embedding of the Cogent fsop_readpage
non-determinism, which can lead to spurious test failures. In            function (shown below) closely resembles that of the
this case, we have to step back and use a non-deterministic              WordArray example. An oracle is also generated and passed to
specification with the NonDet monad instead. This, however,              the Haskell embedding, which will be further passed to the
has a negative cosmetic effect on the entire Haskell specifica-          mock implementation of ostore_read as discussed earlier.
tion, as the NonDet monad is infectious and it would render
                                                                             prop_corres_fsop_readpage :: Property
all ancestor functions in the call graph monadic.
                                                                             prop_corres_fsop_readpage =
   To address this problem, we can establish an equivalence                    forAll gen_fsop_readpage_arg $ \ic →
relation between the non-deterministic specification using                       forAll gen_oracle $ \o →
NonDet and the oracle-carrying deterministic one by testing.                       let ia = abs_fsop_readpage_arg ic
                                                                                       oa = uncurry4 hs_fsop_readpage ia
Concretely, we test that the two specifications return the
                                                                                       oc = fsop_readpage o ic
same set of results, by enumerating every possible oracle                           in corres rel_fsop_readpage_ret oa oc
in the deterministic specification, collecting a finite set of
results, and then checking that set against the set of results           From the counter-examples produced by QuickCheck, we
produced by the non-deterministic specification.                         found that the Haskell executable specification was flawed,
   The NonDet monad and the oracle approach are two ex-                  which in turn exposed a problem with the Isabelle/HOL
tremes of the spectrum, and developers can choose a suitable             abstract specification, from which the Haskell specification
degree of non-determinism by combining these two to meet                 was derived. These specifications did not take errors returned
the needs of a specific test case.                                       from ostore_read into account. Testing the above property
                                                                         helped us rectify this mis-specification.

                                                                         7     Design Decisions and Key Takeaways
                                                                         We have showcased two applications of the PBT framework
6.4   Test Data Generation                                               in Cogent. Since the examples we examined are from a real
By using mocks, not only can we use simpler algorithms to                file system, they have given us some good insights into how
simulate the functionality of the original components, but we            much boilerplate code is required, which components of the
can also fine-tune test data generators to restrict the domain           testing infrastructure can be automatically generated, and
of inputs given to the mock, allowing us to only implement               how these pieces can be integrated.
a partial mock of the original code.
   When testing a cluster of functions and the mock func-                7.1    Modular Testing and Whole-System Testing
tion’s input depends on the output of other functions, the               Our QuickCheck machinery does not require the user to
aforementioned partial mock should be used with care. The                test the entire system at once. Instead, the user may test
input to a function can be directly controlled by the tester             refinement for each function or for a cluster of functions at
by defining appropriate test data generators, while the out-             a time. Typically, the ADTs implemented in C form a com-
put of a function is not so easy to predict as it may have               mon module, shared across many systems. Accordingly, our
been heavily processed and manipulated by the functions.                 framework allows developers to test the ADTs in isolation,
When such an input value reaches the partial mock imple-                 with no regard to how they are used within systems. This
mentation, it is harder to know a priori whether it falls into           modularity is aided by Cogent’s functional semantics.
the unhandled sub-domain of the mock. It poses a greater                    For the fsop_readpage example, we chose to employ modu-
challenge in writing good test data generators to ensure the             lar testing as opposed to whole-system testing, which would
pre-condition of the mock function is met even after the ran-            have required extra effort in developing the infrastructure
domly generated data have flowed through other functions                 to run tests in kernel mode (see Section 7.3). Whole-system
in the system under test. More general remarks on this point             testing allows for more abstract top-level properties to be
can be found in Section 7.4.                                             specified: for instance, that read and write are inverse opera-
   Domain-specific knowledge can be leveraged to write                   tions.2 Alternatively, these logical properties can be tested
good test data generators, which makes the checking pro-
cess more efficient and practicable. For example, when we                2 It might be surprising to some readers that we claim that this property

generate the OstoreState, all entries we generate belong                 is suitable for whole-system testing, instead of PBT. After all, this kind
to the same inode. In reality, there are many data objects               of round-trip properties are typical in the realm of PBT. The reason is
                                                                         that, systems software, or file systems in this case, are not implemented
for other files, or other types of objects; but none of these            cleanly in a purely functional manner. They always involve heavy I/O,
facts will be observed by its caller. This in turn simplifies the        kernel interaction, locking, etc., which cannot be precisely and concisely
implementation of the mock and the abstraction functions.                specified in the functional specification and thus fall under the global state.




                                                                    93
Property-Based Testing: Climbing the Stairway to Verification                            SLE ’22, December 06–07, 2022, Auckland, New Zealand


on top of the executable specification rather than directly on         such as KML [51], House [34] or HaLVM [35] to run PBT in
the concrete implementation.                                           kernel mode. This would allow the testing environment to
   As our specification becomes more abstract, the single              more closely resemble the real run-time environment of the
step simulation style of refinement becomes less relevant,             software. We leave it for future investigation.
because several low-level functions may be specified as a
single function on the abstract level. Modular testing, on             7.4    Test Generation Strategies
the other hand, is more comprehensive, as it also examines             There are two main factors to consider when generating test
the interfaces among different components in a system. In              data for PBT. The first is how to sample the data: we choose
this case, it uncovered issues in the WordArray implementa-            user-guided random test generation à la QuickCheck in this
tion that whole-system testing would have, and indeed had,             work. Exhaustive testing (for small values) is another popular
missed.                                                                strategy and has gained great popularity, e.g. SmallCheck for
                                                                       Haskell [60]. However, the small scope hypothesis on which
7.2   Functional Specification Versus Logical                          SmallCheck is based does not hold in general in the context
      Properties                                                       of systems software.3 For instance, integer overflow, which
Traditional PBT tests specifications against a set of logi-            is a common bug in systems code, can hardly be triggered
cal properties (e.g. get and set are inverse operations on             by small values. The second main concern is the effective
WordArrays). We instead test functions against a full exe-             generation of test data which satisfies the premises of the
cutable specification that models the functions. This is con-          properties. If a property has the form 𝑝 =⇒ 𝑞 and the premise
ceptually similar to model-based testing [43] (also see Sec-           𝑝 is very strong (i.e. difficult to satisfy), and the test data is
tion 8). The functional specification is most akin to the func-        not sampled with great care, then a lot of them will falsify
tional notions of model paradigm as classified in the work             the premise and thus be discarded in the test, rendering the
by Utting et al. [64, § 3.3].                                          test inefficient. All refinement statements in this work have
   It is often easier to use a model rather than a set of prop-        the form 𝑝 =⇒ 𝑞 with a strong precondition 𝑝. The Luck
erties to define the behaviour of functions [43]; our exper-           framework [46] couples the predicates of the property and
iments concurred. For example, functions in the C library              the test data generation, which could simplify writing custom
can be readily modeled in terms of Haskell library functions.          test data generators. There is a rich body of research devoted
Moreover, low-level functions in systems programming, e.g.             to test generation techniques [28]. In the future, we plan to
setting a flag, are often very simple in its functionality, but        explore more options to automate our test data generators.
can hardly be characterised by traditional properties that are
abstract and intuitive enough for users to comprehend.                 7.5    Shrinking
   Using functional specifications encourages composition-             Counter-example shrinking reduces the size of counter-
ality. The functional specification of one module can also             examples before reporting them to testers, which helps
be used as a mock implementation when testing other                    developers better understand and fix bugs. The Haskell
modules that depend on this module. For instance, in our               QuickCheck provides a customisable shrinking library with
fsop_readpage case study, we used the previously defined               a default shrinking algorithm for many datatypes. A rich
Haskell functional specification of the WordArray functions            body of research can be found on more advanced shrinking
as mocks.                                                              algorithms. For example, test data shrinking that preserve
   Furthermore, functional specifications serve as a commu-            invariants about the generated data has been explored in
nication interface between system programmers and proof                [49, 62]. But due to the lack of recursively defined datatypes
engineers. They are key to designing verification-friendly             in Cogent and thus in the Cogent-powered file systems, the
systems programs, whereas logical properties alone fall short          effectiveness of shrinking is dubious, as the size of the input
in this aspect.                                                        data chiefly comes from the sheer complexity of the (non-
                                                                       recursive) datatypes, rather than from recursion. Shrinking
7.3   Testing Kernel Modules
                                                                       is nevertheless useful for testing ADTs, but basic shrinking
A file system is typically compiled as a kernel module and             strategies work reasonably well in our context.
runs in kernel mode, while our test framework runs in user
mode. To handle this discrepancy, for our prototype, we have           8     Related Work
ported our file systems code to run in user mode, using mocks
                                                                       QuickCheck has been used for testing a variety of high-level
to simulate the kernel APIs. Emulating the kernel is common
                                                                       properties, such as information flow control [23, 37], mutual
practice in systems programming, with libraries such as
FUSE [31] facilitating user-space execution of kernel code.            3 The small scope hypothesis is stated in Runciman et al. [60]’s paper as: “(1)
However, these tools expect a complete kernel module, thus             If a program fails to meet its specification in some cases, it almost always
precluding the use of mocks or other user-land code during             fails in some simple case. Or in contrapositive form: (2) If a program does
testing. A possible alternative to explore is using a system           not fail in any simple case, it hardly ever fails in any case.”




                                                                  94
SLE ’22, December 06–07, 2022, Auckland, New Zealand                Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


exclusion [21], and the functional correctness of AUTOSAR                   In the PBT framework we presented, as we test the re-
components [6, 53]. To the best of our knowledge, our frame-             finement statement between the implementation and the
work is the first to use PBT for testing refinement-based                Haskell executable specification, which can be considered
functional correctness statements.                                       a conformance relation, it does appear that we are instead
   The hs-to-coq tool [61] translates Haskell code into the              conducting model-based testing [63, 64]. Our approach does
Coq proof assistant [13]. Breitner et al. [14] used it to verify         indeed share a lot in common with MBT, but we identify
parts of Haskell’s container library in Coq. In addition to              our approach as PBT for the following reasons. Firstly, in
proving the functional correctness of various functions in               MBT, the starting point of testing is a model of the software
the library, they also verified that the QuickCheck proper-              under test. In contrast, as we have demonstrated, testing in
ties that the library is tested against are correct. By contrast,        our framework does not necessarily have an existing model
our QuickCheck properties are refinement properties that                 to start with. In developing formally verifiable operating
directly resemble the those used for full verification. Veri-            systems components, which is the application domain that
fying these properties is already a substantial step towards             concerns us, it is of paramount importance to find the right
proving functional correctness, and in some cases directly               balance between verifiability and performance. PBT gives
implies functional correctness.                                          developers insights in both aspects. Therefore, testing plays
   QuickCheck is available as a built-in tool in Isabelle/HOL            a role in the design of the system, and subsequently its spec-
and is used for quickly finding counter-examples to proposed             ification. This is similar to the iterative development process
lemmas [10, 15]. We chose to build on Haskell’s QuickCheck               reported in the seL4 formal verification work [36]. Secondly,
rather than Isabelle/HOL’s QuickCheck because it is easier               test cases are systematically and algorithmically generated
for Cogent programmers to use a testing framework that                   from the model in MBT. Test inputs are typically concretised
lies in the ecosystem of a functional programming language               from the abstract test suite and the test results are abstracted
rather than interact with a theorem prover. Haskell acts as              to be validated against the model by an adapter. In contrast,
a good communication medium between programmers and                      as we have shown in the examples, our test cases are not gen-
proof engineers [14, 26]. Moreover, due to Isabelle/HOL’s                erated from the specification; test data is directly produced
interactive nature, testers would have to wait for Isabelle to           on the concrete level. Lastly, from the tooling perspective,
re-process the proof scripts affected by a change in a theory            our approach uses a PBT library QuickCheck as the core of
file, before they can run tests again. Even if Isabelle’s quick-         the testing infrastructure.
and-dirty mode is enabled, which skips proofs, testers would
still have to wait for Isabelle/HOL to process definitions. In
fact, a large portion of the time is spent on reading in the             9     Conclusion
deep embeddings of the Cogent program into Isabelle, due                 In this paper, we showed how we augmented the Cogent
to the large terms generated by the Cogent compiler. This                verification framework with PBT. Testing and formal verifi-
would cause a significant and unnecessary reduction to their             cation complement each other, which is well acknowledged
productivity, and destroy the user experience.                           among researchers and developers. In this work, we further
   The SPARK language [2], a formally defined subset of Ada,             demonstrated this common belief in the specific context of
also uses a combination of testing and verification to facil-            PBT and interactive theorem proving. The central idea is to
itate the development of high-reliability software. SPARK                mirror the refinement proof in testing, using a functional
developers can attach contracts, that is, specifications of pre-         specification as the model instead of a set of logical proper-
and postconditions, to critical procedures. Tools of the frame-          ties as commonly done in PBT.
work can use these contracts as input to automatically test                 Using this method, we tested an abstract data type from a
the procedures, or attempt to formally prove that the imple-             library, as well as an operation of a real-world file system.
mentation observes these contracts. Ada language features                The tests exposed several bugs in the ADT implementation
that are hard to verify, such as side-effects in expressions,            and uncovered errors in the specification of the ADT and of
access types, allocators, exception handling and many others,            the file system.
are not permitted in SPARK. SPARK focuses on selectively                    Besides the main purpose of testing—detecting bugs—
verifying safety critical components, rather than fully veri-            we exhibited other benefits of employing PBT. It reduces
fied systems from high-level specification to machine code.              the effort in formal verification, guides the development of
   DoubleCheck [30] integrates PBT into Dracula [65], a ped-             verification-ready specifications and programs, and acts as
agogical programming environment which enables students                  a precise and effective communication media among devel-
to develop programs and then prove theorems about them in                opers. We believe PBT offers developers the opportunity
ACL2 [1], a theorem prover based on term rewriting. As with              to gradually tackle the verification challenge in large and
our work, the motivation of this integration is to facilitate            complex systems development, serving as a helpful stepping
formal verification, though its focus is on education, not on            stone in the endeavour into full formal verification of high
producing verified real-world applications.                              assurance software.



                                                                    95
Property-Based Testing: Climbing the Stairway to Verification                                          SLE ’22, December 06–07, 2022, Auckland, New Zealand


References                                                                           [19] Louis Cheung, Liam O’Connor, and Christine Rizkallah. 2022. Over-
 [1] ACL2. 2022. ACL2. Retrieved October 2022 from http://www.cs.                         coming Restraint: Composing Verification of Foreign Functions with
     utexas.edu/users/moore/acl2/                                                         Cogent. In Proceedings of the 11th ACM SIGPLAN International Confer-
 [2] AdaCore. 2022. SPARK Pro. Retrieved October 2022 from https:                         ence on Certified Programs and Proofs (CPP 2022). ACM, New York, NY,
     //www.adacore.com/sparkpro/                                                          USA, 13–26. https://doi.org/10.1145/3497775.3503686
 [3] Sidney Amani. 2016. A Methodology for Trustworthy File Systems. PhD             [20] Koen Claessen and John Hughes. 2000. QuickCheck: A Lightweight
     Thesis. CSE, UNSW, Sydney, Australia.                                                Tool for Random Testing of Haskell Programs. In Proceedings of the
 [4] Sidney Amani, Alex Hixon, Zilin Chen, Christine Rizkallah, Peter                     5th International Conference on Functional Programming. 268–279.
     Chubb, Liam O’Connor, Joel Beeren, Yutaka Nagashima, Japheth Lim,               [21] Koen Claessen, Michal Palka, Nicholas Smallbone, John Hughes, Hans
     Thomas Sewell, Joseph Tuong, Gabriele Keller, Toby Murray, Gerwin                    Svensson, Thomas Arts, and Ulf Wiger. 2009. Finding Race Conditions
     Klein, and Gernot Heiser. 2016. Cogent: Verifying High-Assurance File                in Erlang with QuickCheck and PULSE. In International Conference on
     System Implementations. In International Conference on Architectural                 Functional Programming. ACM, New York, NY, USA, 149–160. http:
     Support for Programming Languages and Operating Systems. Atlanta,                    //doi.acm.org/10.1145/1596550.1596574
     GA, USA, 175–188.                                                               [22] David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microker-
 [5] Sidney Amani and Toby Murray. 2015. Specifying a Realistic File                      nels, State Monads and Scalable Refinement. In Proceedings of the 21st
     System. In Workshop on Models for Formal Analysis of Real Systems.                   International Conference on Theorem Proving in Higher Order Logics.
     Suva, Fiji, 1–9.                                                                     Springer, Montreal, Canada, 167–182.
 [6] Thomas Arts, John Hughes, Ulf Norell, and Hans Svensson. 2015. Test-            [23] Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine
     ing AUTOSAR software with QuickCheck. In International Conference                    Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy
     on Software Testing, Verification and Validation (ICST) Workshops. Graz,             Pollack, and Andrew Tolmach. 2014. A Verified Information-Flow
     AT, 1–4. https://doi.org/10.1109/ICSTW.2015.7107466                                  Architecture. In ACM SIGPLAN-SIGACT Symposium on Principles of
 [7] R. J. R. Back. 1988. A calculus of refinements for program derivations.              Programming Languages. San Diego, CA, USA, 165–178.
     Acta Informatica 25, 6 (Aug. 1988), 593–624. https://doi.org/10.1007/           [24] Willem-Paul de Roever and Kai Engelhardt. 1998. Data Refinement:
     BF00291051                                                                           Model-Oriented Proof Methods and their Comparison. Number 47 in
 [8] Erik Barendsen and Sjaak Smetsers. 1993. Conventional and Unique-                    Cambridge Tracts in Theoretical Computer Science. Cambridge Uni-
     ness Typing in Graph Rewrite Systems. In Foundations of Software                     versity Press, United Kingdom.
     Technology and Theoretical Computer Science (Lecture Notes in Com-              [25] Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson. 2008.
     puter Science, Vol. 761). 41–51.                                                     Uniqueness Typing Simplified. In Implementation and Application of
 [9] Brian Behlendorf. 2011. POSIX Filesystem Test Suite. Retrieved August                Functional Languages (Lecture Notes in Computer Science, Vol. 5083).
     2022 from https://github.com/zfsonlinux/fstest                                       Springer, 201–218.
[10] Stefan Berghofer and Tobias Nipkow. 2004. Random Testing in Is-                 [26] Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and
     abelle/HOL. In Proceedings of the Software Engineering and Formal                    Manuel M. T. Chakravarty. 2006. Running the Manual: An Approach
     Methods, Second International Conference (SEFM ’04). IEEE Computer                   to High-Assurance Microkernel Development. In Proceedings of the
     Society, Washington, DC, USA, 230–239. http://dx.doi.org/10.1109/                    ACM SIGPLAN Haskell Workshop. Portland, OR, USA.
     SEFM.2004.36                                                                    [27] Oscar Downing. 2021. Enhancements to the Cogent Property-Based
[11] Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R. Newton, Simon                     Testing Framework. Undergraduate Thesis. CSE, UNSW, Sydney, Aus-
     Peyton Jones, and Arnaud Spiwack. 2017. Linear Haskell: Practical                    tralia. https://people.eng.unimelb.edu.au/rizkallahc/theses/oscar-
     Linearity in a Higher-order Polymorphic Language. Proc. ACM Pro-                     downing-honours-thesis.pdf
     gram. Lang. 2, POPL (Dec. 2017), 5:1–5:29. http://doi.acm.org/10.1145/          [28] Jonas Duregård, Patrik Jansson, and Meng Wang. 2012. Feat: Functional
     3158093                                                                              Enumeration of Algebraic Types. In Proceedings of the 2012 Haskell
[12] Jean-Philippe Bernardy, Patrik Jansson, and Koen Claessen. 2010. Test-               Symposium (Haskell ’12). ACM, New York, NY, USA, 61–72. http:
     ing Polymorphic Properties. In Programming Languages and Systems.                    //doi.acm.org/10.1145/2364506.2364515
     Springer Berlin Heidelberg, Berlin, Heidelberg, 125–144.                        [29] Peter Dybjer, Haiyan Qiao, and Makoto Takeyama. 2003. Combining
[13] Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and               Testing and Proving in Dependent Type Theory. In Theorem Proving
     Program Development. Coq’Art: The Calculus of Inductive Constructions.               in Higher Order Logics. Springer Berlin Heidelberg, Berlin, Heidelberg,
     Springer.                                                                            188–203.
[14] Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah,           [30] Carl Eastlund. 2009. DoubleCheck Your Theorems. In Proceedings of
     John Wiegley, and Stephanie Weirich. 2018. Ready, set, verify! applying              the Eighth International Workshop on the ACL2 Theorem Prover and
     hs-to-coq to real-world Haskell code (experience report). PACMPL 2,                  Its Applications (ACL2 ’09). ACM, New York, NY, USA, 42–46. http:
     ICFP (2018), 89:1–89:16.                                                             //doi.acm.org/10.1145/1637837.1637844
[15] Lukas Bulwahn. 2012. The New Quickcheck for Isabelle: Random,                   [31] FUSE. 2022. The FUSE Project. Retrieved October 2022 from https:
     Exhaustive and Symbolic Testing Under One Roof. In International                     //github.com/libfuse/libfuse
     Conference on Certified Programs and Proofs. Springer-Verlag, Berlin,           [32] GHC. 2022. GHC User’s Guide. Retrieved October 2022 from https:
     Heidelberg, 92–108. http://dx.doi.org/10.1007/978-3-642-35308-6_10                   //downloads.haskell.org/ghc/latest/docs/users_guide/
[16] Manuel M. T. Chakravarty. 1999. C → Haskell, or Yet Another Interfac-           [33] Havva Gulay Gurbuz and Bedir Tekinerdogan. 2018. Model-based
     ing Tool. In Implementation of Functional Languages, 11th International              testing for software safety: a systematic mapping study. Software
     Workshop, IFL’99, Lochem, The Netherlands, September 7-10, 1999, Se-                 Quality Journal 26, 4 (Dec 2018), 1327–1372. https://doi.org/10.1007/
     lected Papers. 131–148. https://doi.org/10.1007/10722298_8                           s11219-017-9386-2
[17] Zilin Chen. 2022. Cogent property-based testing case studies. https:            [34] Thomas Hallgren, Mark P. Jones, Rebekah Leslie, and Andrew Tol-
     //github.com/au-ts/cogent/tree/master/impl/fs/bilby/quickcheck.                      mach. 2005. A principled approach to operating system construction
[18] Zilin Chen, Liam O’Connor, Gabriele Keller, Gerwin Klein, and Gernot                 in Haskell. In Proceedings of the 10th International Conference on Func-
     Heiser. 2017. The Cogent Case for Property-Based Testing. In Work-                   tional Programming. Tallinn, Estonia, 116–128.
     shop on Programming Languages and Operating Systems (PLOS). ACM,                [35] HaLVM. 2018. The Haskell Lightweight Virtual Machine (HaLVM)
     Shanghai, China, 1–7.                                                                source archive. Retrieved October 2022 from https://github.com/
                                                                                          GaloisInc/HaLVM



                                                                                96
SLE ’22, December 06–07, 2022, Auckland, New Zealand                             Z. Chen, C. Rizkallah, L. O’Connor, P. Susarla, G. Klein, G.Heiser, and G. Keller


[36] Gernot Heiser, June Andronick, Kevin Elphinstone, Gerwin Klein, Ihor                  every-language
     Kuz, and Leonid Ryzhyk. 2010. The Road to Trustworthy Systems.                   [51] Toshiyuki Maeda. 2015. Kernel Mode Linux: Execute user processes
     In ACM Workshop on Scalable Trusted Computing (ACMSTC). ACM,                          in kernel mode. Retrieved October 2022 from http://web.yl.is.s.u-
     Chicago, IL, USA, 3–10.                                                               tokyo.ac.jp/~tosh/kml/
[37] Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Antal Spector-                  [52] Carroll Morgan. 1990. Programming from Specifications (2nd ed.).
     Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and                          Prentice Hall.
     Leonidas Lampropoulos. 2013. Testing Noninterference, Quickly. In                [53] Wojciech Mostowski, Thomas Arts, and John Hughes. 2017. Modelling
     International Conference on Functional Programming. 455–468.                          of Autosar Libraries for Large Scale Testing. In Workshop on Models
[38] John Hughes. 2016. Experiences with QuickCheck: Testing the Hard                      for Formal Analysis of Real Systems (MARS@ETAPS). 184–199. https:
     Stuff and Staying Sane. In A List of Successes That Can Change the World.             //doi.org/10.4204/EPTCS.244.7
     Lecture Notes in Computer Science, Vol. 9600. Springer, 169–186.                 [54] Tobias Nipkow and Gerwin Klein. 2014. Concrete Semantics with
[39] Steve Klabnik and Carol Nichols. 2017. The Rust Programming Lan-                      Isabelle/HOL. Springer.
     guage. No Starch Press.                                                          [55] Liam O’Connor. 2019. Type Systems for Systems Types. Ph. D. Disser-
[40] Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray,                         tation. UNSW, Sydney, Australia. http://handle.unsw.edu.au/1959.4/
     Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Compre-                       64238
     hensive Formal Verification of an OS Microkernel. ACM Transactions               [56] Liam O’Connor, Zilin Chen, Christine Rizkallah, Sidney Amani,
     on Computer Systems 32, 1 (Feb. 2014), 2:1–2:70.                                      Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, and
[41] Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick,                       Gerwin Klein. 2016. Refinement Through Restraint: Bringing Down
     David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal                   the Cost of Verification. In International Conference on Functional Pro-
     Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon                      gramming. Nara, Japan.
     Winwood. 2009. seL4: Formal Verification of an OS Kernel. In ACM                 [57] Bryan O’Sullivan. 2022. aeson: Fast JSON parsing and encoding. Re-
     Symposium on Operating Systems Principles. ACM, Big Sky, MT, USA,                     trieved August 2022 from https://hackage.haskell.org/package/aeson
     207–220.                                                                         [58] Liam O’Connor, Zilin Chen, Christine Rizkallah, Vincent Jackson, Sid-
[42] Edward A. Kmett. 2022. lens: Lenses, Folds and Traversals. Retrieved                  ney Amani, Gerwin Klein, Toby Murray, Thomas Sewell, and Gabriele
     August 2022 from https://hackage.haskell.org/package/lens                             Keller. 2021. Cogent: uniqueness types and certifying compilation.
[43] Pieter Koopman, Peter Achten, and Rinus Plasmeijer. 2012. Model                       Journal of Functional Programming 31 (2021).
     Based Testing with Logical Properties versus State Machines. In Im-              [59] Christine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell,
     plementation and Application of Functional Languages. Springer Berlin                 Zilin Chen, Liam O’Connor, Toby Murray, Gabriele Keller, and Gerwin
     Heidelberg, Berlin, Heidelberg, 116–133.                                              Klein. 2016. A Framework for the Automatic Formal Verification of
[44] Peter Lammich. 2013. Automatic Data Refinement. In Proceedings of                     Refinement from Cogent to C. In International Conference on Interactive
     the 4th International Conference on Interactive Theorem Proving. Lecture              Theorem Proving. Nancy, France.
     Notes in Computer Science, Vol. 7998. Springer, 84–99.                           [60] Colin Runciman, Matthew Naylor, and Fredrik Lindblad. 2008. Small-
[45] Peter Lammich and Andreas Lochbihler. 2018. Automatic Refinement                      check and Lazy Smallcheck: Automatic Exhaustive Testing for Small
     to Efficient Data Structures: A Comparison of Two Approaches. Journal                 Values. In Proceedings of the First ACM SIGPLAN Symposium on Haskell
     of Automated Reasoning (Mar 2018). https://doi.org/10.1007/s10817-                    (Haskell ’08). ACM, New York, NY, USA, 37–48. http://doi.acm.org/10.
     018-9461-9                                                                            1145/1411286.1411292
[46] Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John                  [61] Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, and
     Hughes, Benjamin C. Pierce, and Li-yao Xia. 2017. Beginner’s Luck: A                  Stephanie Weirich. 2018. Total Haskell is reasonable Coq. In Interna-
     Language for Property-based Generators. In ACM SIGPLAN-SIGACT                         tional Conference on Certified Programs and Proofs. Los Angeles, CA,
     Symposium on Principles of Programming Languages. ACM, New York,                      USA, 14–27.
     NY, USA, 114–129. http://doi.acm.org/10.1145/3009837.3009868                     [62] Jacob Stanley. 2022. Hedgehog will eat all your bugs. Open Source
[47] Leonidas Lampropoulos and Benjamin C. Pierce. 2022. QuickChick:                       Project. Retrieved October 2022 from https://github.com/hedgehogqa/
     Property-Based Testing in Coq. Retrieved October 2022 from https:                     haskell-hedgehog
     //softwarefoundations.cis.upenn.edu/qc-current/index.html                        [63] Jan Tretmans. 2011. Model-Based Testing and Some Steps towards Test-
[48] Jeffrey R. Lewis, John Launchbury, Erik Meijer, and Mark B. Shields.                  Based Modelling. Springer Berlin Heidelberg, Berlin, Heidelberg, 297–
     2000. Implicit Parameters: Dynamic Scoping with Static Types. In ACM                  326. https://doi.org/10.1007/978-3-642-21455-4_9
     SIGPLAN-SIGACT Symposium on Principles of Programming Languages.                 [64] Mark Utting, Alexander Pretschner, and Bruno Legeard. 2012. A Tax-
     ACM, New York, NY, USA, 108–118. http://doi.acm.org/10.1145/325694.                   onomy of Model-Based Testing Approaches. Softw. Test. Verif. Reliab.
     325708                                                                                22, 5 (aug 2012), 297–312. https://doi.org/10.1002/stvr.456
[49] David R. MacIver. 2016. Integrated vs Type-based Shrinking. Article. Re-         [65] Dale Vaillancourt, Rex Page, and Matthias Felleisen. 2006. ACL2 in
     trieved October 2022 from http://hypothesis.works/articles/integrated-                DrScheme. In Proceedings of the Sixth International Workshop on the
     shrinking                                                                             ACL2 Theorem Prover and Its Applications (ACL2 ’06). ACM, New York,
[50] David R. MacIver. 2016. QuickCheck in Every Language. Retrieved                       NY, USA, 107–116. http://doi.acm.org/10.1145/1217975.1217999
     October 2022 from https://hypothesis.works/articles/quickcheck-in-               [66] Philip Wadler. 1990. Linear types can change the world!. In Program-
                                                                                           ming Concepts and Methods.




                                                                                 97
