prodigy.analysis¶

Forward Analysis¶

The semantics transformation of the forwards analysis is mainly specified in the instruction handlers. They provide the actual semantics on a generic level without knowing any specific encoding of a probability distribution.

The Semantics¶

The semantics of a probabilistic program is defined as a distribution transformer. Each individual program instruction is handled via a dedicated instruction handler. These handlers describe on a generic level, how the input distribution is changed after executing the program instruction. This is oftentimes not computable, i.e., when the input distribution has infinite support, or in case of while-loop instructions.

Distribution¶

Distributions are the core objects to transform by a probabilistic program. This class specifies a generic interface with desired convenience methods needed, in order to abstract away from an actual distribution encoding. In fact, we deliver two types of distribution backends:

A sympy implementation of generating functions
A GiNaC C++ implementation shipped as the pybind11 module prodigy_ginac (package prodigy-ppl-ginac).

Analysis Configuration¶

Sometimes, intermediate steps of the computation are desired. This and more configurations can be setup in a ForwardAnalysisConfig object. Here also different backend Engines can be chosen.

Modules

`ai_candidates`	Loop invariants proposed by a language model and checked by Prodigy.
`analyzer`
`config`	Forward Analysis Config
`equivalence`	Equivalence Checking
`evtinvariants`
`exceptions`
`independence`	Static Analysis
`instructionhandler`
`loop_strategies`	Loop strategies (registry)
`lowerbounds`
`optimization`	Optimization
`result`	Analysis results (JSON format)
`session`	Analysis sessions
`solver`