\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}