Datalog is a lightweight logic programming language, based on the logic of Horn clauses. Lean, on the other hand, is a proof assistant system and language based on the Calculus of Inductive Constructions (CIC). Datalog is more constrained and less expressive than Lean but has a long history of established deduction algorithms. Writing definitions and queries in the Datalog fragment of Lean would be more succinct and understandable than writing them in Lean itself. This paper outlines the design and implementation of a shallow embedding of Datalog as a Domain Specific Language (DSL) on top of Lean. Bidirectional interoperability between the Datalog DSL and Lean is a primary goal of this design. In addition to rules and facts, backward chaining queries are automatically translated into theorems with tactic-based proofs. The paper also includes three simple examples of how the DSL can be used.
Raw datasets are often too large and unstructured to work with directly, and require a data preparation process. The domain of industrial Cyber-Physical Systems (CPS) is no exception, as raw data typically consists of large amounts of time-series data logging the system's status in regular time intervals. Such data has to be sanity checked and preprocessed to be consumable by data-centric workflows. We introduce CPSLint, a Domain-Specific Language designed to provide data preparation for industrial CPS. We build up on the fact that many raw data collections in the CPS domain require similar actions to render them suitable for Machine-Learning (ML) solutions, e.g., Fault Detection and Identification (FDI) workflows, yet still vary enough to hope for one universally applicable solution. CPSLint's main features include type checking and enforcing constraints through validation and remediation for data columns, such as imputing missing data from surrounding rows. More advanced features cover inference of extra CPS-specific data structures, both column-wise and row-wise. For instance, as row-wise structures, descriptive execution phases are an effective method of data compartmentalisation are extracted and prepared for ML-assisted FDI workflows. We demonstrate CPSLint's features through a proof of concept implementation.
Many software language tools use declarative domain-specific languages (DDSLs) to implement parts of their functionality, such as context-free grammars for parsing or inference rules for type analysis. For interoperability and ease of use, DDSLs often rely on embedded general-purpose language (GPL) code fragments, as in the semantic actions of parser specifications, but require that these GPL fragments fulfill certain semantic properties, such as the absence of observable side effects. Fulfilling these properties is usually up to the developer, and accidental violations can lead to subtle and hard-to-trace bugs. We present TRAGDOR, a tool that dynamically checks for property violations in Reference Attribute Grammars (RAGs) written for the JASTADD metacompiler, and report on the efficacy of four property testing strategies that TRAGDOR employs. Even in a mature RAG like the Java 11 compiler ExtendJ, TRAGDOR was able to find 13 implementation issues, 2 of which we consider to be of high severity. Our manual inspection of TRAGDOR's reports identifies a number of potential RAG anti-patterns and finds evidence that the inherent dependency structure of RAGs often encodes fine-grained implicit contracts.
Mobile devices have become integral to our everyday lives, yet their utility hinges on their battery life. In Android apps, resource leaks caused by inefficient resource management are a significant contributor to battery drain and poor user experience. Our work introduces Alpakka, a source-to-source compiler for Android's Smali syntax. To showcase Alpakka's capabilities, we developed an Alpakka library capable of detecting and automatically correcting resource leaks in Android APK files. We demonstrate Alpakka's effectiveness through empirical testing on 124 APK files from 31 real-world Android apps in the DroidLeaks [12] dataset. In our analysis, Alpakka identified 93 unique resource leaks, of which we estimate 15% are false positives. From these, we successfully applied automatic corrections to 45 of the detected resource leaks.
Feature models evolve in multiple iterations over time. When modellers change a model, they enact syntactical changes in order to produce specific semantic differences between model iterations. Many tools have been developed to analyze such syntactical differences, but the changing semantics of models were harder to assess. Tools for semantic differences between feature model iterations rely on Binary Decision Diagrams (BDDs) or encode each change into SAT, the former leading to BDD scaling issues and the latter requiring editor support or other specialized tooling. We contribute the first concise formalization of feature models and their semantic differences into propositional logic and use it to efficiently and scalably classify semantic differences using SAT solvers. We then extend our definition into QSAT in order to quantify the full list of semantic differences between feature models and enumerate them using QBF tools, without needing specialized feature model solvers. We implement a semantic difference classifier using our UVL processing pipeline based on Booleguru (instead of the more widely used FeatureIDE) and evaluate it on industrial feature model instances in the standardized UVL format. We also evaluate our QSAT-based semantic difference enumerator and reproduce prior results. We provide all software and evaluation results in an artifact.
Software testing is an integral part of modern software development. Testing frameworks are part of the toolset of any software language allowing programmers to test their programs in order to detect bugs. Unfortunately, there is no work on testing in attribute grammars. In this paper we combine the powerful property-based testing technique with the attribute grammar formalism. In such property-based attribute grammars, properties are defined on attribute instances. Properties are tested on large sets of randomly generated (abstract syntax) trees by evaluating their attributes. We present an implementation that relies on strategies to express property-based attribute grammars. Strategies are tree-based recursion patterns that are used to encode logic quantifiers defining the properties.
Fully general parsers permit the syntax specification of formal languages to be unrestricted, allowing language designers to use a syntax specification that supports semantics specification, but also permitting ambiguity. Language workbenches that support fully general grammars need tools which can generate robust default behaviour but also allow experienced designers to specify particular choices when ambiguity is encountered. The standard longest match approach to ambiguity resolution is not robust when a grammar contains cycles. Although cycles can be removed from a grammar, this disrupts the syntax specification. We present an algorithm that safely removes cycles from the shared packed parse forests generated by general parsers and explore the application of the algorithm to the 1997 SML Definition. The algorithm results in a sub-forest to which further designer-specified or default disambiguation rules can be applied.
Algebraic effect handling is a superior abstraction for non-local control flows, unifying over the existing non-local control flow constructs such as try/catch, destructors, shared state, async/await and generators. To encourage the adoption of effect handlers, improving their performance is essential. Despite having a number of implementations, they lack enough focus on tail resumptive handlers which leaves space for an improvement. We believe that tail resumptive handlers are invoked more frequently and contributes more to the overall performance of programs. The characteristic of them implies the possibility of an implementation with little overhead over function invocation. We propose eff-unwind, an implementation of effect handling as a C++ library which is optimized for tail resumptive handlers at the cost of others. Our implementation uses function calling and returning for tail resuming for improved efficiency while using stack copying and setjmp for general resuming and stack unwinding for yielding. It eliminates the need of recomposing the stack or preserving memory in the lifecycle of a tail resumptive handler at the cost of a less efficient yielding and not-tail resuming. Additionally, our library exposes a functional interface and executes C++ destructors. We evaluate our approach based on a total of 12 cases containing both tail resumptive handlers and others. The result shows performance improvement for tail resuming and slowdown for others. We also discover that multishot handlers presents challenges with C++ destructors.
