1,721,160 research outputs found
Budget-aware random testing with T3: benchmarking at the SBST2016 testing tool contest
No full textRandom testing has the advantage that it is usually fast. An interesting use case is to use it for bulk smoke testing, e.g. to smoke test a whole project. However, on a large project, even with random testing it may still take hours to complete. To optimize this, we have adapted an automated random testing tool called T3 so that it becomes aware of the time budget we set for a given target class. Test suites are now generated incrementally, and their refinements are adaptively scheduled towards maximizing the coverage, given the remaining time. This paper presents an evaluation of the performance of this adaptation, using the benchmark provided by the SBST 2016 Java Unit Testing Tool Contest
DOMain Specific Type Error Diagnosis (DOMSTED)
No full textDomain-specic languages (DSLs) have the potential both to reduce the eort of programming, and to result in programs that are easier to understand and maintain. For various good reasons, researchers have proposed to embed DSLs (then called EDSLs) into a general purpose host language. An important disadvantage of such an embedding is that it is very hard to make type error diagnosis domain-aware, because inconsistencies are by default explained in terms of the host language. In earlier work we have developed a method to make type error diagnosis domain-specic, and we have applied the method to Haskell 98. The practice of Haskell programming shows that currently applications and libraries employ type system features well beyond those oered by Haskell 98. Here lie both a practical and fundamental challenge that the project aims to address. It is practical because only after meeting this challenge, can our ideas be employed in everyday programming; it is fundamental because an essential understanding of Haskell's type system features, such as GADTs and type families, is necessary to achieve the necessary control over the type system that can then be passed on to the EDSL developer. Our work will enable EDSL developers to safely, transparently and noninvasively provide domain specic type error diagnosis. It is transparent because the designer of the rules does not need to have intimate knowledge of the internals of the compiler, safe because it cannot be used to circumvent the strong type system, and non-invasive since the EDSL code itself need not be changed. The work in this project will be undertaken by a PhD student under the supervision of the rst author of this paper, in collaboration with Atze Dijkstra and others at Utrecht University
A predicate transformer semantics for effects: Functional Pearl
No full textReasoning about programs that use effects can be much harder than reasoning about their pure counterparts. This paper presents a predicate transformer semantics for a variety of effects, including exceptions, state, non-determinism, and general recursion. The predicate transformer semantics gives rise to a refinement relation that can be used to relate a program to its specification, or even calculate effectful programs that are correct by construction
Verified Timing Transformations in Synchronous Circuits with λπ -Ware
No full textWe define a DSL for hardware description, called λπ -Ware, embedded in the dependently-typed language Agda, which makes the DSL well-scoped and well-typed by construction. Other advantages of dependent types are that circuit models can be simulated and verified in the same language, and properties can be proven not only of specific circuits, but of circuit generators describing (infinite) families of circuits. This paper focuses on the relations between circuits computing the same values, but with different levels of statefulness. We define common recursion schemes, in combinational and sequential versions, and express known circuits using these recursion patterns. Finally, we define a notion of convertibility between circuits with different levels of statefulness, and prove the core convertibility property between the combinational and sequential versions of our vector iteration primitive. Circuits defined using the recursion schemes can thus have different architectures with a guarantee of functional equivalence up to timing
Unfolding Semantics of the Untyped λ-Calculus with lectrec-Calculus with letrec
No full textWe investigate the relationship between finite terms in lambda-letrec, the lambda calculus with letrec, and the infinite lambda terms they express. We say that a lambda-letrec term expresses a lambda term if the latter can be obtained as an infinite unfolding of the former. Unfolding is the process of substituting occurrences of function variables by the right-hand side of their definition. We consider the following questions: (i) How can we characterise those infinite lambda terms that are lambda-letrec-expressible? (ii) given two lambda-letrec terms, how can we determine whether they have the same unfolding? (iii) given a lambda-letrec term, can we find a more compact version of the term with the same unfolding? To tackle these questions we introduce and study the following formalisms: - a rewriting system for unfolding lambda-letrec terms into lambda terms - a rewriting system for `observing' lambda terms by dissecting their term structure - higher-order and first-order graph formalisms together with translations between them as well as translations from and to lambda-letrec We identify a first-order term graph formalism on which bisimulation preservesand reflects the unfolding semantics of lambda-letrec and which is closed under functional bisimulation. From this we derive efficient methods to determine whether two terms are equivalent under infinite unfolding and to compute the maximally shared form of a given lambda-letrec term
T3, a Combinator-based Random Testing Tool for Java: Benchmarking
No full textT3 is the next generation of the light weight automated testing tool T2 for Java. In the heart T3 is still a random testing tool; but it now comes with some new features: pair-wise testing, concurrent generators, and a combinator-based approach ala QuickCheck. This paper presents the result of benchmarking of T3 on its default configuration against a set of real world classes
Security Type Error Diagnosis for Higher-Order Polymorphic Languages
No full textWe combine the type error slicing and heuristics based approaches to type error diagnostic improvement within the context of type based security analysis on a let-polymorphic call by value lambda calculus extended with lists, pairs and the security specific constructs declassify and protect. We define and motivate four classes of heuristics that help diagnose inconsistencies among the constraints, and show their effect on a selection of security incorrect programs
Type-based Exception Analysis for Non-strict Higher-order Functional Languages with Imprecise Exception Semantics
No full textMost statically typed functional programming languages allow programmers to write partial functions: functions that are not defined on all the elements of their domain as specified by their type. Applying a partial function to a value on which it is not defined will raise a run-time exception, thus in practice well-typed programs can and do still go wrong. To warn programmers about such errors, contemporary compilers for functional languages employ a local and purely syntactic analysis to detect partial case-expressions--those that do not cover all possible patterns of constructors. As programs often maintain invariants on their data, restricting the potential values of the scrutinee to a subtype of its given or inferred type, many of these incomplete case-expressions are harmless. Such an analysis does not account for these invariants and will thus report many false positives, overwhelming the programmer. We develop a constraint-based type system that detects harmful sources of partiality and prove it correct with respect to an imprecise exception semantics. The analysis accurately tracks the flow of both exceptions--the manifestation of partiality gone wrong--and ordinary data through the program, as well as the dependencies between them. The latter is crucial for usable precision, but has been omitted from previously published exception analyses
Exploiting Attribute Grammars to Achieve Automatic Tupling
No full textTupling of function results is a well-known technique in functional programming to avoid multiple traversals over the same data. When expressing these programs as attribute grammars, function results are expressed as shared attributes for which tupling is done automatically. In this paper we show how we can get tupling for free by using attribute grammars as an intermediate language. We evaluate the effectiveness of the approach by showing some benchmark results
- …
