  Deductive verification techniques based on program logics (i.e., the family
of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently,
there has been a trend of increasing the expressive power of such logics by
augmenting their rules with additional information to reason about program
side-effects. For example, general program logics have been augmented with cost
analyses, logics for probabilistic computations have been augmented with
estimate measures, and logics for differential privacy with
indistinguishability bounds. In this work, we unify these various approaches
via the paradigm of grading, adapted from the world of functional calculi and
semantics. We propose Graded Hoare Logic (GHL), a parameterisable framework for
augmenting program logics with a preordered monoidal analysis. We develop a
semantic framework for modelling GHL such that grading, logical assertions
(pre- and post-conditions) and the underlying effectful semantics of an
imperative language can be integrated together. Central to our framework is the
notion of a graded category which we extend here, introducing graded Freyd
categories which provide a semantics that can interpret many examples of
augmented program logics from the literature. We leverage coherent fibrations
to model the base assertion language, and thus the overall setting is also
fibrational.
