| 1. |
- Almström Duregård, Jonas, 1984, et al.
(författare)
-
Feat: Functional Enumeration of Algebraic Types
- 2012
-
Ingår i: 2012 ACM SIGPLAN Haskell Symposium, Haskell 2012. Copenhagen, 13 September 2012. - New York, NY, USA : ACM. - 9781450315746 ; , s. 61-72
-
Konferensbidrag (refereegranskat)abstract
- In mathematics, an enumeration of a set S is a bijective function from (an initial segment of) the natural numbers to S. We define "functional enumerations" as efficiently computable such bijections. This paper describes a theory of functional enumeration and provides an algebra of enumerations closed under sums, products, guarded recursion and bijections. We partition each enumerated set into numbered, finite subsets.We provide a generic enumeration such that the number of each part corresponds to the size of its values (measured in the number of constructors). We implement our ideas in a Haskell library called testing-feat, and make the source code freely available. Feat provides efficient "random access" to enumerated values. The primary application is property-based testing, where it is used to define both random sampling (for example QuickCheck generators) and exhaustive enumeration (in the style of SmallCheck). We claim that functional enumeration is the best option for automatically generating test cases from large groups of mutually recursive syntax tree types. As a case study we use Feat to test the pretty-printer of the Template Haskell library (uncovering several bugs).
|
|
| 2. |
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- Gerdes, Alex, 1978, et al.
(författare)
-
Understanding formal specifications through good examples
- 2018
-
Ingår i: Erlang 2018 - Proceedings of the 17th ACM SIGPLAN International Workshop on Erlang, co-located with ICFP 2018. - New York, NY, USA : ACM. ; , s. 13-24
-
Konferensbidrag (refereegranskat)abstract
- Formal specifications of software applications are hard to understand, even for domain experts. Because a formal specification is abstract, reading it does not immediately convey the expected behaviour of the software. Carefully chosen examples of the software’s behaviour, on the other hand, are concrete and easy to understand—but poorly-chosen examples are more confusing than helpful. In order to understand formal specifications, software developers need good examples. We have created a method that automatically derives a suite of good examples from a formal specification. Each example is judged by our method to illustrate one feature of the specification. The generated examples give users a good understanding of the behaviour of the software. We evaluated our method by measuring how well students understood an API when given different sets of examples; the students given our examples showed significantly better understanding.
|
|
| 6. |
- Matsuda, Kazutaka, et al.
(författare)
-
"Bidirectionalization for Free" for Monomorphic Transformations
- 2015
-
Ingår i: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 111:P1, s. 79-109
-
Tidskriftsartikel (refereegranskat)abstract
- Abstract A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. Over the years, a lot of effort has been made to offer better language support for programming such transformations. In particular, a technique known as bidirectionalization is able to analyze and transform unidirectional programs written in general purpose languages, and “bidirectionalize” them. Among others, an approach termed semantic bidirectionalization proposed by Voigtländer stands out in terms of user-friendliness. A unidirectional program can be written using arbitrary language constructs, as long as the function it represents is polymorphic and the language constructs respect parametricity. The free theorems that follow from the polymorphic type of the program allow a kind of forensic examination of the transformation, determining its effect without examining its implementation. This is convenient, as the programmer is not restricted to using a particular syntax; but it does require the transformation to be polymorphic. In this paper, we lift this polymorphism requirement to improve the applicability of semantic bidirectionalization. Concretely, we provide a type class PackM γ α μ , which intuitively reads “a concrete datatype γ is abstracted to a type α, and the ‘observations’ made by a transformation on values of type γ are recorded by a monad μ”. With PackM, we turn monomorphic transformations into polymorphic ones that are ready to be bidirectionalized. We demonstrate our technique with case studies of typical applications of bidirectional transformation, namely text processing, \{XML\} query and graph transformation, which were commonly considered beyond semantic bidirectionalization because of their monomorphic nature.
|
|
| 7. |
- Matsuda, Kazutaka, et al.
(författare)
-
Bidirectionalization for Free with Runtime Recording: Or, a Light-Weight Approach to the View-Update Problem
- 2013
-
Ingår i: Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP 2013. - New York, NY, USA : ACM. - 9781450321549 ; , s. 297-308
-
Konferensbidrag (refereegranskat)abstract
- A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws.Over the years, a lot of effort has been made to offer better language support for programming such transformations. In particular, a technique known as \emph{bidirectionalization} is able to analyze and transform unidirectional programs written in general purpose languages, and "bidirectionalize" them.Among others, a technique termed as semantic bidirectionalization proposed by Voigtländer stands out in term of user-friendliness. The unidirectional program can be written using arbitrary language constructs, as long as the function is polymorphic and the language constructs respect parametricity. The free theorems that follow from the polymorphic type of the program allow a kind of forensic examination of the transformation, determining its effect without examining its implementation. This is convenient, in the sense that the programmer is not restricted to using a particular syntax; but it does require the transformation to be polymorphic.In this paper, we lift this polymorphic requirement to improve the applicability of semantic bidirectionalization. Concretely, we provide a type class PackM; intuitively "PackM c a m'' reads "a concrete datatype c is abstracted to a type a, and the 'observations' made by a transformation on values of type c are recorded by a monad m''. With PackM, we turn monomorphic transformations into polymorphic ones, ready to be bidirectionalized. We demonstrate our technique with a case study of standard XML queries, which were considered beyond semantic bidirectionalization because of their monomorphic nature.
|
|
| 8. |
- Matsuda, Kazutaka, et al.
(författare)
-
FliPpr: A Prettier Invertible Printing System
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642370359 ; 7792:101-120
-
Konferensbidrag (refereegranskat)abstract
- When implementing a programming language, we often write a parser and a pretty-printer. However, manually writing both programs is not only tedious but also error-prone; it may happen that a pretty-printed result is not correctly parsed. In this paper, we propose FliPpr, which is a program transformation system that uses program inversion to produce a CFG parser from a pretty-printer. This novel approach has the advantages of fine-grained control over pretty-printing, and easy reuse of existing efficient pretty-printer and parser implementations.
|
|
| 9. |
- Oliveira, Bruno C D S, et al.
(författare)
-
The visitor pattern as a reusable, generic, type-safe component
- 2008
-
Ingår i: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). - 0730-8566. ; 43:10, s. 439-456
-
Tidskriftsartikel (refereegranskat)abstract
- The VISITOR design pattern shows how to separate the structure of an object hierarchy from the behaviour of traversals over that hierarchy. The pattern is very flexible; this very flexibility makes it difficult to capture the pattern as anything more formal than prose, pictures and prototypes.We show how to capture the essence of the VISITOR pattern as a reusable software library, by using advanced type system features appearing in modern object-oriented languages such as Scala. We preserve type-safety statically and modularly: no reflection or similar mechanisms are used and modules can be independently compiled. The library is generic, in two senses: not only is it parametrised by both the return type and the shape of the object hierarchy, but also it allows a number of implementation choices (internal versus external control, imperative versus functional behaviour, orthogonal aspects such as tracing and memoisation) to be specified by parameters rather than fixed in early design decisions. Finally, we propose a generalised datatype-like notation,on top of our visitor library: this provides a convenient functional decomposition style in object-oriented languages.
|
|
| 10. |
|
|
