Las primitivas de orden superior permiten escribir código más expresivo y conciso ya que permiten escribir procedimientos parametrizados por otros procedimientos, resultando en código más modular y mantenible. Las aserciones son un tipo especial de primitivas que permiten expresar especificaciones parciales de programas, que luego pueden ser verificadas en tiempo de compilación (es decir, de forma estática) o en tiempo de ejecución (es decir, de forma dinámica). En el caso de los programas de orden superior, las aserciones describen los argumentos de orden superior de los procedimientos. En el contexto de la programación lógica (y con restricciones) ((C)LP), la verificación dinámica de las aserciones de orden superior ha recibido cierta atención. Sin embargo, la verificación estática sigue siendo un área relativamente poco explorada.
Proponemos un enfoque novedoso para la verificación estática de programas (C)LP de orden superior con aserciones que describen argumentos de orden superior. Aunque nuestra presentación se basa en el lenguaje de aserciones de Ciao, la técnica es bastante general y flexible, y creemos que puede aplicarse a enfoques graduales similares. Los argumentos de orden superior se describen utilizando propiedades de predicados, un tipo especial de propiedades que permiten emplear todo el poder de expresividad del lenguaje de aserciones (de Ciao) para dichos argumentos.
Primero, presentamos una mejora tanto de la sintaxis como de la semántica de estas propiedades. A continuación, introducimos un criterio abstracto para determinar si un predicado cumple con una propiedad de predicado en tiempo de compilación, basado en una relación de orden semántica que compara la definición de una propiedad de predicado con la especificación parcial de un predicado. Luego, proponemos una técnica para tratar estas propiedades utilizando un analizador estático basado en interpretación abstracta para programas con aserciones de primer orden, mediante la reducción de las propiedades de predicados a propiedades de primer orden que dicho analizador puede entender de forma nativa. Finalmente, presentamos una implementación prototipo y estudiamos la efectividad del enfoque con varios ejemplos dentro del sistema Ciao.
–ABSTRACT–
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.
Las primitivas de orden superior permiten escribir código más expresivo y conciso ya que permiten escribir procedimientos parametrizados por otros procedimientos, resultando en código más modular y mantenible. Las aserciones son un tipo especial de primitivas que permiten expresar especificaciones parciales de programas, que luego pueden ser verificadas en tiempo de compilación (es decir, de forma estática) o en tiempo de ejecución (es decir, de forma dinámica). En el caso de los programas de orden superior, las aserciones describen los argumentos de orden superior de los procedimientos. En el contexto de la programación lógica (y con restricciones) ((C)LP), la verificación dinámica de las aserciones de orden superior ha recibido cierta atención. Sin embargo, la verificación estática sigue siendo un área relativamente poco explorada.
Proponemos un enfoque novedoso para la verificación estática de programas (C)LP de orden superior con aserciones que describen argumentos de orden superior. Aunque nuestra presentación se basa en el lenguaje de aserciones de Ciao, la técnica es bastante general y flexible, y creemos que puede aplicarse a enfoques graduales similares. Los argumentos de orden superior se describen utilizando propiedades de predicados, un tipo especial de propiedades que permiten emplear todo el poder de expresividad del lenguaje de aserciones (de Ciao) para dichos argumentos.
Primero, presentamos una mejora tanto de la sintaxis como de la semántica de estas propiedades. A continuación, introducimos un criterio abstracto para determinar si un predicado cumple con una propiedad de predicado en tiempo de compilación, basado en una relación de orden semántica que compara la definición de una propiedad de predicado con la especificación parcial de un predicado. Luego, proponemos una técnica para tratar estas propiedades utilizando un analizador estático basado en interpretación abstracta para programas con aserciones de primer orden, mediante la reducción de las propiedades de predicados a propiedades de primer orden que dicho analizador puede entender de forma nativa. Finalmente, presentamos una implementación prototipo y estudiamos la efectividad del enfoque con varios ejemplos dentro del sistema Ciao.
–ABSTRACT–
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. Read More
Related posts:
Notación imperativa para programación lógica = Imperative notation for logic programming
Cómo podría ser un dirigible transatlántico español
Ecuaciones diferenciales estocásticas: Teoría y Aplicaciones
Second-order Lagrangians admitting a first-order Hamiltonian formalism
Improvements in Ciao Prolog’s development environment: developing a rich development environment for Ciao on visual studio code
Evaluation of Colombian Crops Fibrous Byproducts for Potential Applications in Sustainable Building Acoustics