Slicing of probabilistic programs based on specifications

Abstract

The goal of program slicing is, given a program and a slicing criterion, for example, a set of variables, to identify and safely remove program fragments that do not affect the program behavior, with respect to the slicing criterion. The outcome is known as a slice of the original program. Primary applications of program slicing include testing, program comprehension, program debugging, and the extraction of reusable components. Since the introduction of program slicing, several approaches have been proposed. These techniques primarily focus on data and control dependencies and have been applied to diverse program types. However, these techniques only offer partial support for randomization. In the domain of probabilistic programming, making progress in more advanced slicing techniques offers several advantages. In addition to the benefits mentioned earlier, it leads to improved performance in inference calculations —to determine an explicit representation of the probability distribution implicitly represented by a program—. It would also aid in the comprehension of these programs, which are significantly more complex than deterministic programs, often requiring in-depth knowledge of probability theory. Motivated by these reasons, in this study, we have developed the first slicing technique for probabilistic programs based on specifications. We show that when probabilistic programs are accompanied by their specifications in the form of pre- and post-condition, we can exploit this semantic information to produce specification-preserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency. The developed technique is termination-sensitive, allowing to preserve the partial as well as the total correctness of probabilistic programs with respect to their specifications. It is modular, featuring a local reasoning principle, and is formally proved correct. As fundamental technical ingredients of our technique, we design and prove sound verifi- cation condition generators for establishing the partial and total correctness of probabilistic programs, which are of interest on their own and can be exploited elsewhere for other pur- poses. On the practical side, we demonstrate the applicability of our approach by means of a few illustrative examples and a case study from the probabilistic modelling field. We also describe an algorithm for computing least slices among the space of slices derived by our technique.

El objetivo del slicing de programas es, dado un programa y un criterio de slicing, por ejemplo, un conjunto de variables, identificar y eliminar los fragmentos del programa que no afecten su comportamiento, con respecto a dicho criterio de slicing. El resultado se conoce como un slice del programa original. Las aplicaciones principales del slicing de programas incluyen testing, comprensión de programas, depuración de programas y extracción de componentes reutilizables. Se han propuesto varios enfoques desde la introducción del slicing de programas, centrados principalmente en el análisis de dependencias de datos y control en diferentes tipos de programas. Sin embargo, estas técnicas solo brindan un soporte parcial para la aleatorización. En programación probabilística, avanzar en técnicas de slicing ofrece varias ventajas. Además de las aplicaciones mencionadas anteriormente, conduce a un mejor rendimiento en el proceso de inferencia —determinar una representación explícita de la distribución de probabilidad inducida implícitamente por un programa—. También ayudaría a la comprensión de estos programas, que son significativamente más complejos que los programas deterministas y que a menudo requiere un conocimiento profundo de la teoría de la probabilidad. Debido a las razones anteriores, en este estudio hemos desarrollado la primera técnica de slicing para programas probabilísticos basada en especificaciones. Mostramos que cuando los programas probabilísticos están acompañados de sus especificaciones en la forma de prey post-condición, podemos aprovechar esta información semántica para producir slices, que preservan las especificaciones, estrictamente más precisos que los slices producidos por técnicas convencionales basadas en dependencia de datos y control. La técnica desarrollada es sensible a las propiedades de terminación de los programas, permitiendo preservar tanto la corrección parcial como total de los programas respecto a sus especificaciones. Es modular, con un principio de razonamiento local, y demostramos formalmente su correctitud. Como ingredientes técnicos fundamentales de nuestra técnica, diseñamos generadores de condiciones de verificación para establecer la corrección parcial y total de los programas probabilísticos y demostramos su correctitud, resultado que es de interés por sí mismos y pueden ser explotados en otros estudios independientes. En el aspecto práctico, demostramos la aplicabilidad de nuestro enfoque mediante algunos ejemplos ilustrativos y un estudio de caso del campo de la modelación probabilística. También describimos un algoritmo para computar los slices más pequeños dentro del conjunto de slices derivados por nuestra técnica.