\begin{frame}[fragile,t]{Hoare Triples} \vspace*{-1.35ex} \begin{block}{} A \emph{Hoare triple} is a program specification $\hoaretriple{\aform}{\aprog}{\bform}$ where: \begin{itemize} \item $\aform$ is the \emph{precondition}, \item $\aprog$ a core program, \item $\bform$ is the \emph{postcondition}. \end{itemize} \end{block} \pause Quantifiers in $\aform$ and $\bform$ \alert{only} bind variables \alert{not in} $\aprog\, $! \pause \begin{block}{} A \emph{state} (or \emph{store}) of core programs is a function $\saluf$ that to each variable $x$ assigns an integer $\aluf{x}$. \end{block} \pause The formulas $\aform$, $\bform$ are predicate logic formulas over \begin{talign} \asetfuncs & = \setexp{\const{0}{\scriptstyle /0},\, \const{1}{\scriptstyle /0},\, \sbinfunc{-}{\scriptstyle /2},\, \sbinfunc{+}{\scriptstyle /2}, \sbinfunc{*}{\scriptstyle /2}} & & & \asetpreds & = \setexp{ \sbinpred{<}{\scriptstyle /2},\, \sbinpred{=}{\scriptstyle /2} } \end{talign} \pause we define for all states $\saluf\,$: \begin{talign} \saluf \satisfies \aform \;\;\Longleftrightarrow\;\; \standardZ \satisfieslookup{\saluf} \aform \end{talign} where $\saluf$ is viewed as environment, and $\standardZ$ has domain $\ints$, and interprets function and predicate symbols in standard manner. \vspace{10cm} \end{frame}