27
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Beyond correct and fast: Inspection Testing

      Preprint

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          Occasionally, developers need to ensure that the compiler treats their code in a specific way that is only visible by inspecting intermediate or final compilation artifacts. This is particularly common with carefully crafted compositional libraries, where certain usage patterns are expected to trigger an intricate sequence of compiler optimizations -- stream fusion is a well-known example. The developer of such a library has to manually inspect build artifacts and check for the expected properties. Because this is too tedious to do often, it will likely go unnoticed if the property is broken by a change to the library code, its dependencies or the compiler. The lack of automation has led to released versions of such libraries breaking their documented promises. This indicates that there is an unrecognized need for a new testing paradigm, inspection testing, where the programmer declaratively describes non-functional properties of an compilation artifact and the compiler checks these properties. We define inspection testing abstractly, implement it in the context of Haskell and show that it increases the quality of such libraries.

          Related collections

          Most cited references17

          • Record: found
          • Abstract: not found
          • Article: not found

          Valgrind

            Bookmark
            • Record: found
            • Abstract: found
            • Article: not found

            Contraction-free sequent calculi for intuitionistic logic

            Gentzen's sequent calculus LJ, and its variants such as G3 [21], are (as is well known) convenient as a basis for automating proof search for IPC (intuitionistic propositional calculus). But a problem arises: that of detecting loops, arising from the use (in reverse) of the rule ⊃⇒ for implication introduction on the left. We describe below an equivalent calculus, yet another variant on these systems, where the problem no longer arises: this gives a simple but effective decision procedure for IPC.
              Bookmark
              • Record: found
              • Abstract: not found
              • Article: not found

              QuickCheck

                Bookmark

                Author and article information

                Journal
                19 March 2018
                Article
                1803.07130
                25393ae8-a700-4c48-88fe-f03a242155cf

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                21 pages. Submitted to ICFP'18
                cs.PL

                Comments

                Comment on this article