(** %{\sc Segunda parte de la primera pr\'actica}% *) (** %Fecha de entrega: 22 de Diciembre 2006% *) (** %\section{Introducci\'on} Una {\em especificaci\'on} es una descripci\'on precisa de las requerimientos del cliente escrita en una determinada notaci\'on (lenguaje). Se dice que la notaci\'on es formal cuando posee una sint\'axis {\em formal} as\'{\i} como una sem\'antica formal (e.g. Coq). Si tiene una sint\'axis formal s\'olamente, se dice que es un lenguaje {\em semi--formal} (e.g. UML). Los requerimientos pueden ser funcionales, de eficiencia o de implementaci\'on. En este ejemplo sencillo solo trataremos con requerimientos funcionales. Una especificaci\'on viene a ser una suerte de {\em contrato} entre el cliente y el especificador. Por lo tanto el cliente debe ser capaz de entender la especificaci\'on en orden a {\em validarla} pero normalmente los clientes no estar\'an versados en lenguajes especializados para entender la especificaci\'on. Existen varios m\'etodos para salvar esta dificultad: trasladarla, con las m\'{\i}nimas imprecisiones posibles, al lenguaje natural del cliente o, si es ejecutable probarla en varios escenarios con el cliente. El uso de ejemplos y contraejemplos es una buena t\'ecnica para asegurar que el cliente y el especificador se entienden el uno al otro. En la medida que la especificaci\'on es tambi\'en un contrato entre el especificador y el implementador, se supone que \'este comprende bien el lenguaje especializado de la especificaci\'on. Tambi\'en resulta esencial, que el implementador disponga de la descripci\'on en lenguaje natural porque ello le ayudar\'a a trasladar las distintas ideas a conceptos propios del dominio de la aplicaci\'on. Asegurar al m\'aximo que la especificaci\'on coincide con las necesidades del cliente es un aspecto fundamental. Claro que esta coincidencia no se puede demostrar completamente y por eso este proceso, llamado validaci\'on, consiste precisamente en probar {\em propiedades} sobre la especificaci\'on que responden, casi siempre, a precisiones o demandas del cliente. Cuantas m\'as propiedades solicitadas podamos probar a partir de la especificaci\'on m\'as confianza tendremos en la coincidencia de la misma con los requerimientos expuestos. Finalmente, debe ser posible probar que la implementaci\'on satisface la especificaci\'on. En este sentido conviene utilizar m\'etodos que permitan, como hace Coq, bien extraer autom\'aticamente el c\'odigo directamente de la especificaci\'on o bien demostrar un teorema que pruebe dicha satisfacci\'on. Desafortunadamente no siempre es posible demostrar que un sistema completo satisface su especificaci\'on y para ello en algunos casos se recurre a otros m\'etodos semiformales como el {\em testing}, no para probar pero s\'{\i} para ganar confianza en que la implementaci\'on se adec\'ua bastante a la especificaci\'on. \section{Gu\'{\i}a de tel\'efonos electr\'onica} Supongamos que deseamos construir una especificaci\'on formal en Coq de una gu\'{\i}a de tel\'efonos electr\'onica descrita por el cliente, en un primer momento, por los siguientes requerimientos informales\footnote{Ejemplo sacado de {\em A Tutorial Introduction to PVS} de Hudy Crow y otros}: \begin{itemize} \item la gu\'{\i}a debe almacenar los n\'umeros de tel\'efono de una ciudad \item Dado un nombre, debe ser posible encontrar un n\'umero de tel\'efono asociado \item Debe ser posible a\~nadir y borrar entradas en la gu\'{\i}a \end{itemize} Vemos que hay tres tipos de entidades que se mencionan: gu\'{\i}as, n\'umeros de tel\'efonos y nombres; una gu\'{\i}a define una asociaci\'on entre nombres y n\'umeros de tel\'efono. Se necesitan tres operaciones, que podemos llamar {\tt EncTel} (encontrar tel\'efono), {\tt AddTel} (a\~nadir tel\'efono) y {\tt BorrTel} (borrar tel\'efono). {\tt EncTel} toma una gu\'{\i}a y un nombre y devuelve el n\'umero de tel\'efono asociado a ese nombre en esa gu\'{\i}a. La funcionalidad exacta de las otras dos es menos clara, por lo tanto debemos tomar algunas decisiones de dise\~no. El cliente decide que {\tt AddTel} tomar\'a una gu\'{\i}a, un nombre y un n\'umero de tel\'efono y a\~nadir\'a la asociaci\'on de ese nombre y n\'umero a dicha gu\'{\i}a. Y {\tt BorrTel} deber\'{\i}a tomar una gu\'{\i}a y un nombre y borrar la asociaci\'on de ese nombre y su tel\'efono de esa gu\'{\i}a (si tal asociaci\'on existe) El siguiente paso es decidir c\'omo representar estas entidades y operaciones en Coq. Si estuvieramos pogramando tendr\'{\i}amos que escoger alguna representaci\'on espec\'{\i}fica para los n\'umeros de tel\'efono y para los nombres (e.g. cadenas ascci o otras m\'as estructuradas como registros conteniendo el c\'odigo de \'area etc.) y tendr\'{\i}amos que tomar algunas decisiones de dise\~no en este momento. Pero para crear la especificaci\'on, todo lo que necesitamos es que n\'umeros de tel\'efono y nombres sean tipos distinguibles y saber que la igualdad entre sus elementos es decidible:% *) Section guia1. Require Export ite. Variable N:Set. Variable T:Set. Axiom eq_dec_N : forall(x1 x2:N),{x1=x2}+{~x1=x2}. Axiom eq_dec_T:forall(t1 t2:T),{t1=t2}+{~t1=t2}. (** %A continuaci\'on hay que decidir c\'omo vamos a representar las gu\'{\i}as. Hay varias posibilidades. La primera podr\'{\i}a ser que {\bf una gu\'{\i}a es simplemente una funci\'on entre nombres y tel\'efonos}:% *) Definition G:=N -> T. (** %Esto tiene ya una consecuencia: como una gu\'{\i}a solo registra los nombres que tienen tel\'efono, debemos representar, por ejemplo, mediante la asociaci\'on con un tel\'efono ficticio los nombres que no lo tienen:% *) Variable tf0:T. (** %y as\'{\i} podemos definir la gu\'{\i}a vac\'{\i}a:% *) Definition guiavacia:=fun(nm:N) => tf0. (** %Podemos definir ya la primera funcionalidad:% *) Definition EncTel:=fun(g:G) (nm:N) => (g nm). (** %Vamos a definir \verb"AddTel0" como una primera aproximaci\'on a \verb"AddTel" veamos como podemos a\~nadir a una gu\'{\i}a un nombre y un tel\'efono. Despu\'es trataremos de comprobar que representa realmente esta idea mediante una serie de lemas:% *) Definition AddTel0:=fun(g:G)(nm:N)(tf:T)(a:N) => if (eq_dec_N a nm) then tf else (g a). Lemma proba:forall(g:G)(nm:N)(tf:T),(AddTel0 g nm tf nm)=tf. Proof. intros g nm tf. unfold AddTel0. case (eq_dec_N nm nm); auto. intros. elim n;auto. Qed. Lemma proba1:forall(g:G)(nm a:N)(tf:T),(a=nm) -> (AddTel0 g nm tf a)=tf. Proof. intros g nm a tf H. rewrite H; apply proba. Qed. Lemma proba2:forall(g:G)(nm a:N)(tf:T),(~a=nm) -> (AddTel0 g nm tf a)=(g a). Proof. Admitted. Hint Resolve proba proba1 proba2. (** %El cliente demanda ahora: Si a\~nadimos un nombre {\tt nm} con un tel\'efono {\tt tfp} a una gu\'{\i}a y despu\'es buscamos ese nombre en dicha gu\'{\i}a deber\'{\i}amos de obtener {\tt tp}:% *) Lemma EncAdd0:forall(g:G)(nm:N)(tfp:T), (EncTel (AddTel0 g nm tfp) nm)= tfp. Proof. intros. unfold EncTel. unfold AddTel0. case (eq_dec_N nm nm). auto. intros. elim n;auto. Qed. (** %y, efectivamente se cumple. % *) (** %Definamos ahora la funcionalidad de borrar una entrada en la gu\'{\i}a:% *) (* Definition BorrTel:G -> N -> G:= fun(g:G)(nm:N) => (AddTel0 g nm tf0). *) Definition BorrTel:G -> N -> G:= fun (g:G) (nm:N)(x:N)=>if (eq_dec_N nm x) then tf0 else (g x). Lemma BorrTel1:forall (g:G) (nm:N),(BorrTel g nm nm)=tf0. intros. unfold BorrTel. rewrite ite_l;auto. Qed. Lemma BorrTel2:forall (g:G)(nm x:N),~x=nm -> (BorrTel g nm x)=g x. intros. unfold BorrTel. rewrite ite_r;auto. Qed. (** %Podemos ahora comprobar nuestro entendimiento de esta especificaci\'on chequeando la intuici\'on de que a\~nadiendo un nombre y tel\'efono a una gu\'{\i}a y despu\'es borrarla debe dejar la gu\'{\i}a como estaba. {\it Lemma BorAdd0:forall(g:G)(nm:N)(tfp:T)(x:N), (BorrTel (AddTel0 g nm tfp) nm x)= (g x).} \noindent pero esto no es cierto como se ve en el contraejemplo siguiente:% *) Section contraejemplo1. Variable nombre:N. Variable tel1:T. Variable nig:~(tel1=tf0). Let g:=(AddTel0 guiavacia nombre tel1). Lemma no: ~(BorrTel (AddTel0 g nombre tel1) nombre) nombre=(g nombre). rewrite BorrTel1. unfold g. rewrite proba1;auto. Qed. End contraejemplo1. (** %As\'{\i} pues tenemos un fallo en la especificaci\'on. Podemos modificar esta exigencia y, llamando:% *) Definition Desconocido:=fun(g:G)(nm:N) => (g nm)=tf0. (** %planteamos el siguiente lema (interpretar y probar):% *) Lemma BorAdd0:forall(g:G)(nm:N)(tfp:T)(x:N), (Desconocido g nm) -> (BorrTel (AddTel0 g nm tfp) nm x)=(g x). intros. unfold BorrTel. unfold Desconocido in H. Admitted. (** %Compruebe si es cierta la siguiente propiedad que nos pide el cliente: a\~nadir un nombre y despu\'es borrarlo es lo mismo que simplemente borrarlo.% *) Lemma BorAddBor:forall(g:G)(nm:N)(tfp:T)(x:N), (BorrTel (AddTel0 g nm tfp) nm x)=(BorrTel g nm x). intros. unfold BorrTel. Admitted. (** %Compruebe si es cierto lo siguiente: despu\'es de a\~nadir un nombre a una gu\'{\i}a ese nombre ya no es desconocido.% *) (** %\section{Mejorando la especificaci\'on} Tratemos de mejorar nuestra especificaci\'on para superar los dos problemas que hemos detectado. En primer lugar {\tt AddTel} tiene el efecto no deseado de cambiar el tel\'efono de un nombre cuando se a\~nade \'este nombre a gu\'{\i}a donde ya figuraba. Y segundo, no evita que podamos a\~nadir un nombre con el tel\'efono falso {\tt tf0}. Podemos evitar el segundo problema representando los tel\'efonos normales (distintos del {\tt tf0} con el tipo :% *) Definition TN:={tf:T | ~(tf=tf0)}. (** %al que a\~nadimos las dos conocidas proyecciones:%*) Definition p1:=fun(tfp:TN)=>let (tf,_):=tfp in tf. Definition p2:=fun(tfp:TN)=> let (_,p) return (~((p1 tfp)=tf0)) :=tfp in p. (** %y definimos la funcionalidad de a\~nadir tel\'efono s\'olamente para los normales y evitamos cambiar el tel\'efono permitiendo s\'olamente a\~nadir nombres que no figuraran ya con uno real:% *) Definition AddTel:G->N->TN->N->T := fun(g:G)(nm:N)(tfp:TN) => if (eq_dec_T (g nm) tf0) then (AddTel0 g nm (p1 tfp)) else g. (** %Interpretar y completar las pruebas de las siguientes propiedades:% *) Lemma proban:forall(g:G)(nm:N)(tf:TN),(Desconocido g nm) -> (AddTel g nm tf nm)=(p1 tf). Admitted. Lemma proban_con:forall(g:G)(nm:N)(tf:TN),~(Desconocido g nm) -> (AddTel g nm tf nm)=g nm. Proof. intros. unfold AddTel. case (eq_dec_T (g nm) tf0); intros; auto. Qed. Lemma proba1n:forall(g:G)(nm a:N)(tf:TN),(Desconocido g nm) -> (a=nm) -> (AddTel g nm tf a)=(p1 tf). Proof. intros g nm a tf d H. rewrite H; apply proban;auto. Qed. Lemma proba2n:forall(g:G)(nm a:N)(tf:TN), (~a=nm)->(AddTel g nm tf a)=(g a). Proof. intros. unfold AddTel. case (eq_dec_T (g nm) tf0); intros; auto. Qed. (** %y construimos una nueva funcionalidad que hace precisamente el cambio del tel\'efono de un nombre s\'olamente si ese nombre tiene ya un n\'umero normal. Interpretar y probar:% *) Definition CambiarTel:G -> N -> TN -> N -> T := fun(g:G)(nm:N)(tfp:TN) => if (eq_dec_T (g nm) tf0) then g else (AddTel0 g nm (p1 tfp)). Lemma EncAdd:forall(g:G)(nm:N)(tfp:TN),(Desconocido g nm) -> (EncTel (AddTel g nm tfp) nm)= (p1 tfp). Proof. intros. simpl. unfold EncTel. unfold AddTel. Admitted. Lemma BorAdd:forall(g:G)(nm:N)(tfp:TN)(x:N),(Desconocido g nm) -> (BorrTel (AddTel g nm tfp) nm x)=(g x). intros. case (eq_dec_N nm x). intro e. rewrite <- e. rewrite BorrTel1. auto. Admitted. Lemma camtelx:forall(g:G)(nm:N)(tfp:TN)(x:N),(~x=nm) -> (CambiarTel g nm tfp x)=(g x). Proof. intros. unfold CambiarTel. case (eq_dec_T (g nm) tf0); intros; auto. Qed. Lemma EncCam:forall(g:G)(nm:N)(tfp:TN),~(Desconocido g nm) -> (EncTel (CambiarTel g nm tfp) nm)= (p1 tfp). Admitted. Lemma MiCam1:forall(g:G)(nm:N)(tfp:TN),~(g nm)=tf0 -> ( CambiarTel g nm tfp nm)= (p1 tfp). Proof. intros. unfold CambiarTel. case (eq_dec_T (g nm) tf0); intros; auto. elim (H e). Qed. Lemma MiCam2:forall(g:G)(nm:N)(tfp:TN),(g nm)=tf0 -> ( CambiarTel g nm tfp nm)= tf0. Proof. intros. unfold CambiarTel. case (eq_dec_T (g nm) tf0); intros; auto. elim (n H). Qed. Lemma ConAdd:forall(g:G)(nm:N)(tfp:TN)(x:N), ~(Desconocido (AddTel g nm tfp) nm). Proof. intros. unfold Desconocido. unfold AddTel. case (eq_dec_T (g nm) tf0). intros. unfold AddTel0. case (eq_dec_N nm nm). intros. exact (p2 tfp). destruct 1;auto. auto. Qed. Lemma adtelcon:forall(g:G)(nm:N)(tfp1:TN),~(AddTel g nm tfp1 nm)=tf0. Proof. (red; intros). (apply (ConAdd g nm tfp1 nm); auto). Qed. Lemma AddCam: forall(g:G)(nm:N)(tfp1 tfp2:TN)(x:N), (CambiarTel (AddTel g nm tfp1) nm tfp2 x)= (AddTel (CambiarTel g nm tfp2) nm tfp2 x). Admitted. End guia1. (** %\section{Nueva representaci\'on} Se trata ahora de seguir un nuevo requisito pedido por el cliente que nos dice que deber\'{\i}amos de contemplar la posibilidad de que un nombre tuviera varios tel\'efonos. Ello nos lleva a representar una gu\'{\i}a como una funci\'on de nombres en listas de tel\'efonos. Esto tiene adem\'as la ventaja de que nos permite prescindir del tel\'efono virtual. Desarrollar una especificaci\'on en la misma l\'{i}nea que la anterior.% *) (** %\section{Representaci\'on con un tipo inductivo} Finalmente, tratar de definir el tipo gu\'{\i}a como un tipo inductivo y definir funcionalidades y expresar y probar propiedades an\'alogas a las anteriores.% *)