Fundamenta Informaticae - Volume 173, issue 4

Authors: Fioravanti, Fabio | Gallagher, John P. | Proietti, Maurizio

Article Type: Other

DOI: 10.3233/FI-2020-1923

Citation: Fundamenta Informaticae, vol. 173, no. 4, pp. i-ii, 2020

Authors: Frühwirth, Thom

Article Type: Research Article

Abstract: We present a concise source-to-source transformation that introduces justifications for user-defined constraints into the rule-based Constraint Handling Rules (CHR) programming language. There is no need to introduce a new semantics for justifications. This leads to a conservative extension of the language, as we can show the equivalence of rule applications. A scheme of two rules suffices to allow for logical retraction (deletion, removal) of CHR constraints during computation. Without the need to recompute from scratch, these rules remove the constraint and also undo all its consequences. We prove a confluence result concerning the rule scheme. We prove its correctness …in general and tighten the results for confluent programs. We give an implementation, show its correctness, present two classical examples of dynamic algorithms, and improve the implementation. The computational overhead of introducing justifications and of performing logical retraction, i.e. the additional time and space needed, is proportional to the derivation length in the original program. This overhead may increase space complexity, but does not change the worst-case time complexity. Show more

Keywords: Truth Maintenance, Rule-Based Programming, Logic Programming, Computational Logic, Source-to-Source Program Transformation, Constraint Deletion, Confluence

DOI: 10.3233/FI-2020-1924

Citation: Fundamenta Informaticae, vol. 173, no. 4, pp. 253-283, 2020

Authors: Hanus, Michael

Article Type: Research Article

Abstract: Static type systems are usually not sufficient to express all requirements on function calls. Hence, contracts with pre- and postconditions can be used to express more complex constraints on operations. Contracts can be checked at run time to ensure that operations are only invoked with reasonable arguments and return intended results. Although such dynamic contract checking provides more reliable program execution, it requires execution time and could lead to program crashes that might be detected with more advanced methods at compile time. To improve this situation for declarative languages, we present an approach to combine static and dynamic contract checking …for the functional logic language Curry. Based on a formal model of contract checking for functional logic programming, we propose an automatic method to verify contracts at compile time. If a contract is successfully verified, it can be omitted from dynamic checking. This method decreases execution time without degrading reliable program execution. In the best case, when all contracts are statically verified, it provides trust in the software since crashes due to contract violations cannot occur during program execution. Show more

Keywords: Declarative programming, contracts, verification

DOI: 10.3233/FI-2020-1925

Citation: Fundamenta Informaticae, vol. 173, no. 4, pp. 285-314, 2020

Authors: Skeirik, Stephen | Stefanescu, Andrei | Meseguer, José

Article Type: Research Article

Abstract: Reachability logic has been applied to 𝕂 rewrite-rule-based language definitions as a language-generic logic of programs to verify a wide range of sophisticated programs in conventional languages. Here we study how reachability logic can be made not just language-generic, but also rewrite-theory-generic , so that we can verify both conventional programs based on their rewriting logic operational semantics and distributed system designs specified as rewrite theories. A theory-generic reachability logic is presented and proved sound for a wide class of rewrite theories. Particular attention is given to increasing the logic’s automation by means of constructor-based semantic …unification, matching, narrowing, and satisfiability procedures. The relationships to Hoare logic and LTL are discussed, new methods for proving invariants of possibly never terminating distributed systems are developed, and experiments with a prototype implementation illustrating the new methods are presented. Show more

Keywords: reachability and rewriting logics, deductive verification

DOI: 10.3233/FI-2020-1926

Citation: Fundamenta Informaticae, vol. 173, no. 4, pp. 315-382, 2020