  We present a novel formal system for proving quantitative-leakage properties
of programs. Based on a theory of Quantitative Information Flow (QIF) that
models information leakage as a noisy communication channel, it uses
"gain-functions" for the description and measurement of expected leaks.
  We use a small imperative programming language, augmented with leakage
features, and with it express adversaries' activities in the style of, but more
generally than, the Hoare triples or expectation transformers that
traditionally express deterministic or probabilistic correctness but without
information flow.
  The programs are annotated with "gain-expressions" that capture simple
adversarial settings such as "Guess the secret in one try." but also much more
general ones; and our formal syntax and logic -based framework enables us to
transform such gain-expressions that apply after a program has finished to ones
that equivalently apply before the program has begun.
  In that way we enable a formal proof-based reasoning system for QIF at the
source level. We apply it to the %programming language we have chosen, and
demonstrate its effectiveness in a number of small but sometimes intricate
situations.
