|
Next: Probabilistic Semantics
Up: Background
Previous: Abstract Interpretation
In general, the attempt to analyse programs by approximating their
properties can be seen as in line with many engineering approaches:
Instead of attempting the impossible, e.g. total verification or
building an unsinkable ship, a more practical approach suggests that
one considers approximate analysis of software or methods to build
ships with a ``good'' chance to sail for quite some time.
In many cases it would be useful to measure the likelihood (i.e. the
probability) that the intended property is indeed satisfied. We would
then be interested in an exact estimate of the error made in the
approximation. One way to achieve this is to introduce a kind of
(numerical) quantification of the qualities of programs. Such a
quantification of the approximation error would also address one
major shortcoming of classical abstract interpretation, as mentioned
in [40, Section 3.4,]
One shortcoming of the development [...] is that a correct analysis
may be so imprecise as to be practically useless. [...] The notion
of correctness is topological in nature but we would ideally like
something that was a bit more metric in nature so that we could express
how imprecise a correct analysis is. Unfortunately no one has
been able to develop an adequate metric for these purposes.
Semantic models for probabilistic computation will provide us
with a good base to deal with this issue and to develop
a program analysis methodology which is able to quantify the
level of imprecision. This methodology will be applicable to
any program not only to probabilistic ones.
Next: Probabilistic Semantics
Up: Background
Previous: Abstract Interpretation
|
