\documentclass[12pt,a4paper]{report}

\usepackage{latexsym}

\pagestyle{empty}
\begin{document} \large
\begin{center} \bf\Large
Programas: Sem\^antica e Verifica\c c\~ao
\end{center}

\vspace*{5mm}
\noindent {\bf Sintaxe:} pode ser especificada via BNF.

\vspace*{3mm}
\noindent {\bf Sem\^antica:} usualmente vista informalmente.

\vspace*{5mm}
\noindent {\bf Exemplo:}

\begin{itemize}
 \item Sintaxe do comando {\bf if} de Pascal em BNF:

       $\langle${\em if-stmt}$\rangle$ {\tt ::=}
         {\tt if} $\langle${\em expr}$\rangle$ {\tt then} $\langle${\em stmt}$\rangle$
         $[$ {\tt else} $\langle${\em stmt}$\rangle$ $]$

 \item Sem\^antica (informal): A express\~ao booleana \'e avaliada. Se verdadeira, o comando
       que segue {\tt else} \'e executado, caso contr\'ario, o comando que segue {\tt else}
       \'e executado.
\end{itemize}

\vspace*{5mm}
\noindent {\bf Problema com sem\^antica informal:}

\begin{itemize}
 \item N\~ao h\'a como verificar (formalmente) a
       corre\c c\~ao de um programa.
 \item Deve-se usar teste e depura\c c\~ao.
\end{itemize}


\pagebreak
\noindent {\bf\Large O Sistema dedutivo ${\cal HL}$:}

\vspace*{7mm}
\noindent {\bf\Large Axiomas de dom\'{\i}nio:}

\vspace*{3mm}
\begin{enumerate}
 \item[\ ] Toda f\'ormula verdadeira no dom\'{\i}nio das vari\'aveis do
           programa.
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Axioma da atribui\c c\~ao:}

\begin{enumerate}
 \item[\ ] $\vdash\; \{p(x)\{x\leftarrow t\}\}\; {\tt x := t}\; \{p(x)\}$
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Regra da composi\c c\~ao:}

\begin{enumerate}
 \item[\ ] \begin{tabular}{cc}
            $\vdash\; \{p\}\; S1\; \{q\}$ & \hspace*{5mm}$\vdash\; \{q\}\; S2\; \{r\}$ \\ \hline
            \multicolumn{2}{c}{$\vdash\; \{p\}\; S1\; {\tt ;}\; S2\; \{r\}$}
           \end{tabular}
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Regra da alternativa:}

\begin{enumerate}
 \item[\ ] \begin{tabular}{cc}
            $\vdash\; \{p\wedge B\}\; S1\; \{q\}$ & \hspace*{5mm}$\vdash\; \{p\wedge\neg B\}\; S2\; \{q\}$ \\ \hline
            \multicolumn{2}{c}{$\vdash\; \{p\} \;{\tt if}\; $B$\; {\tt then}\; $S1$\; {\tt else}\; $S2$\; \{q\}$}
           \end{tabular}
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Regra do la\c co:}

\begin{enumerate}
 \item[\ ] \begin{tabular}{c}
            $\vdash\; \{p\wedge B\}\; S\; \{p\}$ \\ \hline
            $\vdash\; \{p\} \;{\tt while}\; $B$\; {\tt do}\; $S$\; \{p\wedge\neg B\}$
           \end{tabular}
\end{enumerate}

\vspace*{5mm}
\noindent {\bf\Large Regra da consequ\^encia:}

\begin{enumerate}
 \item[\ ] \begin{tabular}{ccc}
            $\vdash\; p_1\rightarrow p$ & \hspace*{5mm}$\vdash\; \{p\}\; S\; \{q\}$ &
                \hspace*{5mm}$\vdash\; q\rightarrow q_1$ \\ \hline
            \multicolumn{3}{c}{$\vdash\; \{p_1\} \;S\; \{q_1\}$}
           \end{tabular}
\end{enumerate}


\pagebreak

\noindent {\bf\Large Verifica\c c\~ao de programas/Exemplos}

\vspace*{7mm}
\noindent {\bf\large Programa com {\em anota\c c\~oes\/}:}

\vspace*{3mm}
\begin{tabbing}
 xxx\=xxxx\=xxxx\= \kill
    \>$\{\mbox{\em true}\}$ \\
    \>{\tt x := 0;} \\
    \>$\{x=0\}$ \\
    \>{\tt y := b;} \\
    \>$\{x=0\wedge y=b\}$ \\
    \>{\tt while y <> 0 do} \\
    \> \>$\{x=(b-y)\times a\}$ \\
    \> \>{\tt begin} \\
    \> \> \>{\tt x := x + a;} \\
    \> \> \>{\tt y := y - 1} \\
    \> \>{\tt end;} \\
    \>$\{x=a\times b\}$ \\
\end{tabbing}

\vspace*{7mm}
\noindent {\bf\large Provar a corre\c c\~ao parcial:}

\vspace*{3mm}
\begin{tabbing}
 xxx\=xxxx\=xxxx\= \kill
    \>$\{a\geq 0\}$ \\
    \>{\tt x := 0; y := 1;} \\
    \>{\tt while y <= a do} \\
    \> \>{\tt begin} \\
    \> \> \>{\tt x := x + 1;} \\
    \> \> \>{\tt y := y + 2*x + 1} \\
    \> \>{\tt end} \\
    \>$\{0\leq x^2\leq a<(x+1)^2\}$ \\
\end{tabbing}


\end{document}
