Preconditions in classic Hoare Logic are \emph{hypothetical}: there is no
requirement that a precondition should hold before executing code, but if it
does then on completion the postcondition is true.  However, several
applications of Hoare Logic use a stricter interpretation where a precondition
must hold before code is executed.  This is the \emph{contract} approach of
Meyer, and also appears in the JML \texttt{requires} clause.  The distinction
shows up in variations of the Hoare rule for procedure call, and its
corresponding weakest precondition.  Strict preconditions are also appropriate
when encoding rich type systems into program logics, where function
application demands that arguments are of a given type.

However, the conventional semantics of Hoare triples as statements about state
relations does not support this strict interpretation.  We propose a refined
semantics for Hoare logic, based on existing notions of resource algebras,
that captures strict preconditions.  A key novelty is that the validity of
triples becomes relative to procedure specifications, even --- recursively ---
for those procedures themselves.  In joint work with Alberto Momigliano and
Randy Pollack, we are adapting Nipkow's shallow encoding of Hoare logic in
Isabelle to account for strict preconditions.