Abstract
We present the first slicing approach for probabilistic programs based on specifications. Concretely, we show that when probabilistic programs are accompanied by their functional specifications in the form of pre and postcondition, one can exploit this semantic information to produce specificationpreserving slices strictly more precise than slices yielded by conventional techniques based on data/control dependency.
To illustrate this, assume that Alice and Bob repeatedly flip a fair coin until observing a matching outcome, either both heads or both tails. However, Alice decides to "trick" Bob and switches the outcome of her coin, before comparing it to Bob’s. The game can be encoded by the program below, which is instrumented with a variable n that tracks the required number of rounds until observing the first match. The program terminates after K loop iterations with probability 1/(2^K) provided K > 0, and with probability 0 otherwise, satisfying the annotated specification.
\\ pre: 1/(2^K) [K > 0]
n := 0;
a, b := 0, 1;
while (a ̸= b) do
n := n + 1;
{a := 0} [1/2] {a := 1};
a := 1 − a;
{b := 0} [1/2] {b := 1}
\\ post: [n = K]
Traditional slicing techniques based on data/control dependencies conclude that the only valid slice of the program (w.r.t. output variable n) is the very same program. However, our slicing approach allows removing the assignment a := 1a from the loop body, while preserving the program specification.
At the technical level, our slicing technique works by propagating postconditions backward using the greatest preexpectation transformer  the probabilistic counterpart of Dijkstra’s weakest precondition transformer. This endows programs with an axiomatic semantics, expressed in terms of a verification condition generator (VCGen) that yields quantitative proof obligations.
In particular, we design (and prove sound) VCGens for both the partial (allowing divergence) and the total (requiring termination) correctness of probabilistic programs, making our slicing technique terminationsensitive. To handle iteration, we assume that program loops are annotated with invariants. To reason about (probabilistic) termination, we assume that loop annotations also include (probabilistic) variants.
Another appealing property of our slicing technique is its modularity: It yields valid slices of a program from valid slices of its subprograms. Most importantly, this involves only local reasoning.
Besides developing the theoretical foundations of our slicing approach, we also exhibit an algorithm for computing program slices. Interestingly, the algorithm computes the least slice that can be derived from the slicing approach, according to a proper notion of slice size, using, as main ingredient, a shortestpath algorithm.
Finally, we demonstrate the applicability of our approach by means of a few illustrative examples and a case study from the probabilistic modeling field.
BibTeX  Entry
@InProceedings{navarro_et_al:LIPIcs.ECOOP.2022.34,
author = {Navarro, Marcelo and Olmedo, Federico},
title = {{Slicing of Probabilistic Programs Based on Specifications}},
booktitle = {36th European Conference on ObjectOriented Programming (ECOOP 2022)},
pages = {34:134:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772259},
ISSN = {18688969},
year = {2022},
volume = {222},
editor = {Ali, Karim and Vitek, Jan},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16262},
URN = {urn:nbn:de:0030drops162628},
doi = {10.4230/LIPIcs.ECOOP.2022.34},
annote = {Keywords: probabilistic programming, program slicing, expectation transformer semantics, verification condition generator}
}
Keywords: 

probabilistic programming, program slicing, expectation transformer semantics, verification condition generator 
Collection: 

36th European Conference on ObjectOriented Programming (ECOOP 2022) 
Issue Date: 

2022 
Date of publication: 

23.06.2022 