Algo1_TP1/espec/drone.tex

\begin{problema}{crearD}{i: \ent, ps: [Producto]}{Drone}
	\asegura {id(res)==i} 
	\asegura {mismos(productosDisponibles(res),pd)}
	\asegura {bateria(res)==100}
	\asegura {enVuelo==False}
	\asegura {|vuelosRealizados(res)|==0}
\end{problema}

\begin{problema}{idD}{d: Drone}{\ent}
	\asegura {res==id(d)}
\end{problema}

\begin{problema}{bateriaD}{d: Drone}{\ent}
	\asegura {res==bateria(d)}
\end{problema}

\begin{problema}{enVueloD}{d: Drone}{\bool}
	\asegura{res==enVuelo(d)} 
\end{problema}
	
\begin{problema}{vueloRealizadoD}{d: Drone}{[(\ent, \ent)]}
	\asegura{res==vueloRealizado(d)}
\end{problema}

\begin{problema}{posicionActualD}{d: Drone}{(\ent, \ent)}
	\asegura{res==posicionAltual(d)}
\end{problema}

\begin{problema}{productosDisponiblesD}{d: Drone}{[Producto]}
	\asegura{mismos(res,productosDisponobles(d))}
\end{problema}

\begin{problema}{vueloEscaleradoD}{d: Drone}{\bool}
	\asegura{res==\ escalera1(d) \vee escalera2(d)\vee escalera3(d) \vee escalera4(d)}
\end{problema}

\begin{problema}{vuelosCruzadosD}{ds: [Drone]}{[$((\ent, \ent), \ent)]$}
	\requiere{|ds| > 0 }
	\requiere{(\forall d \leftarrow ds)\mid VueloRealizado(d) \mid == \mid VueloRealizado(d)_{0} \mid}
	\asegura{\mid res \mid == \mid quitarRepetidos(parcelasConChoques(ds)) \mid}
	\asegura{estaOrdenadoPorLaSugundaCoordenada(res)}
	\asegura{(\forall e \leftarrow parcelasConChoques(ds))e \in res } 
\end{problema}