Marco Ciccalè

In strongly-typed languages, types are verified at compile time, while dynamically typed languages, such as Prolog, perform type consistency checks entirely at run-time. Extending dynamic languages with assertions allows expressing both classical types and more general properties, providing high expressiveness, but at the cost of run-time overhead. Abstract interpretation allows safely approximating such program properties at compile time, which has been used to reduce the number of properties that require run-time checks, while still reporting unverified properties that can guide further static analyses, testing, or domain refinement. In this work, we first study how to selectively integrate the run-time semantics of assertion properties into a multivariant, top-down, goal-directed abstract interpretation algorithm. We then show how multiple inferred calling patterns can be exploited to reduce the number of properties that must be checked at run-time, thus minimizing the overhead. Finally, we report on an implementation of our approach in the Ciao system and provide performance results supporting that better results can be obtained

Higher-order constructs enable more expressive and concise code by allowing procedures to be parameterized by other procedures. Assertions allow expressing partial program specifications, which can be verified either at compile time (statically) or run time (dynamically). In higher-order programs, assertions can also describe higher-order arguments. While in the context of (C)LP, run-time verification of higher-order assertions has received some attention, compile-time verification remains relatively unexplored. We propose a novel approach for statically verifying higher-order (C)LP programs with higher-order assertions. Although we use the Ciao assertion language for illustration, our approach is quite general and we believe is applicable to similar contexts. Higher-order arguments are described using predicate properties—a special kind of property which exploits the (Ciao) assertion language. We refine the syntax and semantics of these properties and introduce an abstract criterion to determine conformance to a predicate property at compile time, based on a semantic order relation comparing the predicate property with the predicate assertions. We then show how to handle these properties using an abstract interpretation-based static analyzer for programs with first-order assertions by reducing predicate properties to first-order properties. Finally, we report on a prototype implementation and evaluate it through various examples within the Ciao system.

We propose a demonstration of the Ciao Prolog Playground and the Active Logic Documents (ALDs) approach as a practical toolset designed to facilitate the teaching and learning of Prolog and formal methods, both on-line and in the classroom.

Higher-order constructs enable more expressive and concise code by allowing procedures to be parameterized by other procedures, resulting in more modular and maintainable code. Assertions are linguistic constructs for writing partial program specifications, which can then be verified either at compile time (i.e., statically) or run time (i.e., dynamically). In the case of higher-order programs, assertions provide descriptions of the higher-order arguments of procedures. In the context of (C)LP, the run-time verification of such higher-order assertions has received some attention. However, verification at compile time remains relatively unexplored. We propose a novel approach for the compile-time verification of higher-order (C)LP programs with assertions that describe higher-order arguments. Although our presentation is based for concreteness on the Ciao assertion language, the approach is quite general and flexible, and we believe it can be applied to similar gradual approaches. Higher-order arguments are described using predicate properties, a special kind of properties that allow using the full power of the (Ciao) assertion language for such arguments. We first present a refinement of both the syntax and semantics of these properties. Next, we introduce an abstract criterion to determine whether a predicate conforms to a predicate property at compile time, based on a semantic order relation to compare the definition of a predicate property and the partial specification of a predicate. We then propose a technique for dealing with these properties using an abstract interpretation-based static analyzer for programs with first-order assertions, by reducing predicate properties to first-order properties that are natively understood by such an analyzer. Finally, we report on a prototype implementation and study the effectiveness of the approach with various examples within the Ciao system.

The software industry has consistently experienced rapid and transformative changes since its beginning. A significant aspect of this evolution lies in the tools and utilities available for creating software solutions. These tools enable developers to focus on crafting solutions while minimizing time spent on non-essential tasks. Among these tools, the text editor is arguably one of the most crucial. In recent years, Visual Studio Code has emerged as the most widely used text editor globally. It allows users to extend its functionality through extensions implemented using modern web technologies. This project aims to explain the design and implementation of a Visual Studio Code extension for the Ciao programming language. The extension integrates core tools such as the Ciao preprocessor (CiaoPP) and the autodocumenter for (C)LP systems (LPdoc) in an intuitive and comprehensive way inside a modern and accessible text editor. This integration makes the extension suitable for developers of all expertise levels in logic programming and software verification.