Databases Reference
In-Depth Information
is interpreted to mean the following: If the programProgis started with
an initial expectation Pre
E
, then it results in the expectation Post
E
after
execution.
Assertions are ordered by implication ordering. Expectations are ordered
by the partial order V. Given two expectations A
E
and B
E
, we say that
A
E
V B
E
holds if for all states , we have that A
E
() B
E
(). Given
an assertion A the expectation [A] is dened to map every state to 1 if
satisfies A and to 0 otherwise.
Suppose A
E
V B
E
. Consider a sampler that samples states using the
expectations as a probability measure. Then, for any threshold t and state
, if A
E
() > t, then it is the case that B
E
() > t. In other words, for any
sampler with any threshold t, sampling over A
E
results in a subset of states
than those obtained by sampling over B
E
.
Traditional axiomatic proofs are done using weakest preconditions. The
weakest precondition operator is denoted byWP. By definition, for any pro-
gramProgand assertion A, we have thatWP(Prog;A) to be the weakest as-
sertion B (weakest is defined with respect to the implication ordering between
assertions) such that the Hoare triple fBgProgfAg holds.
McIver and Morgan extend the weakest preconditions to expectations, and
define for an expectation A
E
and a probabilistic programProg,WP(Prog; A
E
)
is the weakest expectation B
E
(weakest is defined with respect to the or-
dering V between expectations) such that the probabilistic Hoare triple
fB
E
gProgfA
E
g holds. Given two probabilistic programsSpecandImpl with
respect to a post expectation Post
E
, we say that Impl renesSpec if
WP(Spec; Post
E
) VWP(Impl; Post
E
).
Refinement between constraint systems. We now model constraints A1
and B1 from Section 11.2 as probabilistic programs with an appropriate post
expectation, and derive relationships between the parameters of A1 and B1
such that A1 renes B1.
Consider any directed acyclic graph G = hV;Ei, where E V V . In
this simple setting, nodes with in-degree 0 are potential sources, nodes with
out-degree 0 are potential sinks, and other nodes (internal nodes with both
in-degree and out-degree greater than 0) are potential sanitizers. We want
to classify every node in V with a boolean value 0 or 1. That is, we want a
mapping m : V ! f0; 1g, with the interpretation that for a potential source
s 2 V , m(s) = 1 means that s is classied as a source, and that for a potential
sink n 2 V , m(n) = 1 means that n is classied as a sink, and that for a
potential sanitizer w 2 V , m(w) = 1 means that w is classied as a sanitizer.
We extend the mapping m to operate on paths (triples) over G by applying
m to every vertex along the path (triple).
We want mappings m that satisfy the constraint that for any path p =
s;w
1
;w
2
;:::;w
m
;n that starts at a potential source s and ends in a potential
sink, the string m(p) 62 10
1, where 10
1 is the language of strings that begin
and end with 1 and have a sequence of 0's of arbitrary length in-between.
Search WWH ::
Custom Search