
\documentclass[a4paper]{article}

\setlength\textwidth{6.5in}
\setlength\oddsidemargin{0in}
\setlength\evensidemargin{0in}

%\setlength\headheight{0in}
%\setlength\headsep{0in}

%\setlength\topmargin{-0.5in}
%\addtolength{\textheight}{0.5in}


\newcommand{\SIG}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Idiom}[1]{\textsl{#1}}
\newcommand{\IF}[0]{\textbf{if}}
\newcommand{\FI}[0]{\textbf{fi}}
\newcommand{\SKIP}[0]{\textbf{skip}}
\newcommand{\DO}[0]{\textbf{do}}
\newcommand{\OD}[0]{\textbf{od}}
\newcommand{\AWAIT}[0]{\textbf{await}}

\usepackage{latexsym}
\usepackage[spanish]{babel}

\title{Programaci\'on Concurrente \\ Pr\'actico 2: Verificaci\'on de Programas Secuenciales\\Repaso}
\author{J. Blanco, N. Wolovick}


\begin{document}
\maketitle

\begin{enumerate}

	%Sch97, ej4.7
	%AO97, ej3.4
	%Apunte Javier
	\item{?`Cu\'ales de las siguientes f\'ormulas de la l\'ogica de Hoare son
		verdaderas en el sentido de la \emph{correcci\'on parcial}?
		Demostrar con la l\'ogica o dar un contraejemplo en el modelo de ejecuci\'on.
		\begin{enumerate}
			\item{$\{true\}\  x:=100\ \{true\}$}
			\item{$\{true\}\  x:=100\ \{x=100\}$}
			\item{$\{x=50\}\  x:=100\ \{x=50\}$}
			\item{$\{y=50\}\  x:=100\ \{y=50\}$}
			\item{$\{true\}\  x:=100\ \{false\}$}
			\item{$\{false\}\ x:=100\ \{x=50\}$}
			\item{$\{y=14\}\ \SKIP\ \{y=14\}$}
			\item{$\{y=12\wedge x\geq y\}\ \SKIP\ \{x>12\}$}
			\item{$\{x=X \wedge y=Y\}z:=x; x:=y; y:=z \{x=Y \wedge y=X\}$}
			\item{$\{true\}\IF\ false\rightarrow\ S\ \FI\{Q\}$}
			\item{\begin{tabbing}
				$\{true\}$   \\
           			$\IF$  \= $x\leq y \rightarrow\SKIP$ \\
           			$\Box$ \> $y\leq x \rightarrow x,y:=y,x$ \\
				$\FI$ $\{x\leq y\}$
				\end{tabbing}
			}
			\item{\begin{tabbing}
				$\{x=X\wedge y=Y\}$   \\
           			$\IF$  \= $x\leq y \rightarrow \{x\leq y\}\SKIP$ \\
           			$\Box$ \> $y\leq x \rightarrow \{x\leq y\}x,y:=y,x$  \\
				$\FI$ $\{X\leq Y\}$
				\end{tabbing}
			}
			\item{\begin{tabbing}
				$\{true\}$ \\
				$r,q:=x,0$ \\
				$\{I: x=y\times q + r\}$ \\
				$\DO$   \= $y\leq r \rightarrow$ \= $r:=r-y;$ \\
					\>			\> $q:=q+1$ \\
				$\OD\ \{x=y\times q + r \wedge r<y\}$
				\end{tabbing}
			}
			\pagebreak
			\item{\begin{tabbing}
				$\{0\leq X \wedge 0\leq Y \wedge x=X \wedge y=Y\}$ \\
				$z:=1$ \\
				$\{I: 0\leq y \wedge z\times x^y = X^Y\}$ \\
				$\DO$   \= $0<y \wedge even(y) \rightarrow$ \= $\{I \wedge 0<y \wedge even(y)\}$ \\
					\>				\> $y,x:=y\ div\ 2,x\times x$ \\
					\>				\> $\{I\}$ \\
				$\Box$   \= $0<y \wedge odd(y) \rightarrow$ \= $\{I \wedge 0<y \wedge odd(y)\}$ \\
					\>				\> $y,z:=y-1,z\times x$ \\
					\>				\> $\{I\}$ \\
				$\OD\ \{z=X^Y\}$
				\end{tabbing}
			}
		\end{enumerate}
	}

	%Apunte Javier
	\item{Demostrar que si el siguiente programa anotado es correcto
		\begin{tabbing}
			$\{P\}$	\= $\IF$  \= $B_0 \rightarrow S_0$ \\
				\> $\Box$ \> $B_1 \rightarrow S_1$ \\
				\> $\FI$ $\{Q\}$
		\end{tabbing}
		entonces el siguiente programa tambi\'en lo es:
		\begin{tabbing}
			$\{P\}$ \= $\IF$ \= $B_0 \wedge \neg B_1 \rightarrow S_0$ \\
				\> $\Box$ \> $B_1 \rightarrow S_1$ \\
				\> $\FI$ $\{Q\}$
		\end{tabbing}

		Luego, toda demostraci\'on de un programa secuencial no determin\'{\i}stico
		sirve para demostrar alguna de las variantes determin\'{\i}sticas del
		mismo.
	}

	%Sch97 ej4.32 modificado
	\item{El operador de transformaci\'on de predicados $wlp$ para correcci\'on
		parcial tambi\'en es \emph{conjuntivo}.
		\[wlp.S.(P\wedge Q) = wlp.S.P \wedge wlp.S.Q\]
		\begin{enumerate}
			\item{Demostrar que es mon\'otono 
				$(P\Rightarrow Q) \Rightarrow (wlp.S.P\Rightarrow wlp.S.Q)$
			}
			\item{?`Cu\'al de las dos implicaciones vale?
				$wlp.S.(P\vee Q) \frac{\Rightarrow}{\Leftarrow} wlp.S.P \vee wlp.S.Q$

				Demostrar o dar contraejemplo\footnote{Hint: el no-determinismo.}.
			}
		\end{enumerate}
	}

	%AO91 ej3.9
	\item{La sucesi\'on de Fibonacci est\'a dada por las siguientes ecuaciones recursivas
\[fib.0=0\ \ \ \ \ \ fib.1=1\ \ \ \ \ \ fib.n=fib.(n\!-\!1)+fib.(n\!-\!2), 2\leq n\]
		Probar la f\'ormula de correcci\'on parcial
\[\{0\leq n\} S \{x=fib.n\}\]
		donde $S$ es
		\begin{tabbing}
			$S \equiv$ \= $x:=0; y:=1; count:=n;$ \\
			\> $\DO$ $0<count \rightarrow h:=y; y:=x+y; x:=h; count:=count-1$ \\
			\> $\OD$
		\end{tabbing}
	}

	\item{Escriba el programa m\'as corto que en correcci\'on parcial establece la postcondici\'on $(N>0)$.
		\[ Q: \langle\forall i:0\leq i<N:b.i=i^2\rangle \]
	}
	
\end{enumerate}

\end{document}

