\documentclass[12pt,spanish,a4]{article} \usepackage{babel} \usepackage{zed-csp} \usepackage{enumerate} \usepackage{fullpage} \begin{document} % % EJERCICIO 1 % \begin{syntax} [METHOD,ID,STATE] \\ \end{syntax} \begin{axdef} CALL : \power METHOD \\ RETURN : \power METHOD \\ nullmethod : METHOD \where nullmethod \in RETURN \\ nullmethod \in CALL \\ CALL \bigcup RETURN = METHOD \\ CALL \bigcap RETURN = \{ nullmethod \} \\ \#CALL = \# RETURN \\ \end{axdef} \begin{syntax} PORT ::= send | receive | returned | return \\ CONTROL ::= ready | receive\_callin | running\_callin | \\ make\_callout | taked\_callout | receive\_return\_callout | \\ taked\_return\_callout | send\_return\_callin \end{syntax} \begin{schema}{Layer} id : ID \\ export : CALL \\ import : ID \cross CALL \\ states : \power STATE \\ start : STATE \\ compute : STATE \rel ID \cross STATE \cross METHOD \\ runmethod : ID \cross STATE \cross CALL \rel STATE \\ nextreturn : ID \cross STATE \cross RETURN \rel STATE \\ \where start \in states \also \forall m:CALL, \; i:ID \; s_1,s_2:STATE | (s_1, (i,s_2,m)) \in compute @ \\ \t1 \{s_1, s_2\} \subset states \land \exists i:ID (i,m) \in import \also \forall i:ID, \; s_1,s_2:STATE, \; c:CALL | ((i,s_1,c),s_2) \in runmethod @ \\ \t1 \{s_1, s_2\} \subset states \land \exists i:ID @ (i,c) \in import \\ \also \forall i:ID, \; s_1,s_2:STATE, \; r:RETURN | ((i,s_1,r),s_2) \in nextreturn @ \\ \t1 \{s_1, s_2\} \subset states \land \exists i:ID @ (c,returnby? \, r) \in import \\ \end{schema} \begin{schema}{Layer\_State} l : Layer \\ current : STATE \\ in : ID \\ out : ID \\ port : PORT \cross ID \pfun METHOD \\ ctrl : CONTROL \\ \where current \in l.states \also out \in \{i:ID | \exists c:CALL @ (i,c) \in l.import \} \\ \also \forall p:PORT, i:ID | p \in \{send,receive\} \land (p,i) \in domain \, port @ \\ \t1 port \, p \, i \; \in CALL \\ \forall p:PORT, i:ID | p \in \{return,returned\} \land (p,i) \in domain \, port @ \\ \t1 port \, p \, i \; \in RETURN \\ \also \{i:ID | (send,i) \in domain \, port\} = \{i:ID | (returned,i) \in domain \, port\} \\ \{i:ID | (receive,i) \in domain \, port\} = \{i:ID | (return,i) \in domain \, port\} \\ \also FALTA PONER COSAS VER DESPUES!! \end{schema} \begin{schema}{Layer\_InternalCompute} \Delta Layer\_State \where ctrl \in \{ready, running\_callin, taked\_return\_callout\} \\ \also l' = l \\ in' = in \\ out' = out \\ port' = port \\ ctrl' = ctrl \\ \also \exists s_1,s_2 : STATE, i:ID | (s_1, (i,s_2,nullmethod)) \in compute @ \\ \t1 current = s_1 \land current' = s_2 \\ \end{schema} \begin{schema}{Layer\_MakeCallOut} \Delta Layer\_State \where ctrl \in \{ running\_callin, taked\_return\_callout \} \\ \also l' = l \\ in' = in \\ \also \exists s_1,s_2 : STATE, i:ID, m:CALL | (s_1, (i,s_2,m)) \in compute @ \\ \t1 m \neq nullmethod \\ \t1 \land current = s_1 \\ \t1 \land current' = s_2 \land \\ \t1 \land out' = i \land \\ \t1 \land ctrl' = make\_callout \land \\ \t1 \land port' \ndres \{(send,i)\} = port \ndres \{(send,i)\} \land \\ \t1 \land port' \, send \, i = m \\ \end{schema} \begin{schema}{Layer\_TakeReturnCallOut} \Delta Layer\_State \where ctrl \in \{ receive\_return\_callout \} \\ \also l' = l \\ in' = in \\ out' = out \\ port' = port \\ \also \exists r:RETURN, \; s_1,s_2:STATE | ( (out,s_1,r), s_2) \in nextreturn @ \\ \t1 current = s1 \\ \t1 \land returnby? \, r = port \, send \, out \\ \t1 \land current' = s_2 \\ \t1 \land ctrl' = taked\_return\_callout \end{schema} \begin{schema}{Layer\_RunCallIn} \Delta Layer\_State \where ctrl \in \{ receive\_callin \} \also l' = l \\ in' = in \\ out' = out \\ port' = port \\ \also \exists s_2:STATE | ( ( in, current , port \, receive \, in ),s_2) \in runmethod @ \\ \t1 current' = s_2 \\ \t1 \land ctrl' = running\_callin \end{schema} \begin{schema}{Layer\_SendReturnCallIn} \Delta Layer\_State \where ctrl \in \{ running\_callin \} \also l' = l \\ in' = in \\ out' = out \\ \also \exists s_1,s_2 : STATE, r:RETURN | (s_1, (in,s_2,r)) \in compute @ \\ \t1 current = s_1 \\ \t1 \land r \neq nullmethod \\ \t1 \land returnby? \, r = port \, receive \, in \\ \t1 \land current' = s\_2 \\ \t1 \land port' \ndres \{(return,in)\} = port \ndres \{(return,in)\} \\ \t1 \land port' \, return \, in = r \\ \t1 \land ctrl' = send\_return\_callin \\ \end{schema} \begin{syntax} Layer\_Compute \defs \\ \t1 Layer\_InternalCompute \\ \t1 \lor Layer\_MakeCallOut \\ \t1 \lor Layer\_TakeReturnCallOut \\ \t1 \lor Layer\_RunCallIn \\ \t1 \lor Layer\_SendReturnCallIn \\ \end{syntax} \begin{schema}{Connector} Source,Sink : Layer \where Source.id \neq Sink.id \\ Source.import \subset Sink.export \\ \end{schema} \begin{axdef} layername : \power ID \\ connectorname : \power ID \\ \where layername \bigcap connectorname = \emptyset \\ \end{axdef} \begin{schema}{System} syslayer : layername \fun Layer \\ sysconnector : layername \cross layername \fun Connector \\ \where \forall c:connectorname \exists ln_1,ln_2:layername @ \\ \t1 sysconnector \, c .Source = syslayer \, ln_1 \land \\ \t1 sysconnector \, c .Sink = syslayer \, ln_2 \\ \also \forall ln_1, ln_2:layername @ \#\{c:connectorname | \\ \t1 sysconnector \, c.Source = syslayer \, ln_1 \land \\ \t1 sysconnector \, c.Sink = syslayer \, ln_2 \} \leq 1 \\ \also \forall ln_1:layername @ syslayer \, ln_1.id = ln_1 \end{schema} \begin{schema}{System\_State} sys : System \\ syslayer\_state : layername \fun Layer\_State \where \forall ln:layername @ syslayer\_state \, ln.l = sys.syslayer \, l \end{schema} \begin{schema}{System\_State\Phi Layer\_State} \Delta System\_State \\ \Delta Layer\_State \\ layer? : layername \where sys ' = sys \\ syslayer\_state' \ndres \{ layer? \} = syslayer\_state \ndres \{ layer? \} \\ \theta Layer\_State = syslayer\_state \; layer? \\ \theta Layer\_State' = syslayer\_state' \; layer? \end{schema} \begin{schema}{System\_Layer\_Compute} System\_State \Phi Layer\_State \\ Layer\_Compute \\ \where \exists ln:layername @ layer? = ln \end{schema} \begin{schema}{System \Phi 2Layer\_State} \Delta System\_State \Delta Layer\_State_1 \\ \Delta Layer\_State_2 \\ ln_1?,ln_2? : layername \where sys ' = sys \\ \also syslayer\_state' \ndres \{ ln_1?, ln_2? \} = syslayer\_state \ndres \{ ln_1?, ln_2? \} \\ \also \theta Layer\_State_1 = syslayer\_state \; ln_1? \\ \theta Layer\_State_2 = syslayer\_state \; ln_2? \\ \theta Layer\_State_1' = syslayer\_state' \; ln_1? \\ \theta Layer\_State_2' = syslayer\_state' \; ln_2? \\ \end{schema} \begin{schema}{System\_DeliverCallIn} System \Phi 2Layer\_State \\ \where \exists l_1,l_2:layername @ ln_1? = l_1 \land ln_2? = l_2 \\ \also ctrl_1 = makecallout \\ % Listos para mandar! ctrl_2 = ready \also out_1 = l_2.l.id \\ % Se lo esta mandando a ese! \also port_1 \; send \; out_1 \in l_2.l.export \also \exists c:connectorname @ \\ \t1 \land sys.sysconnector \; c.Source.id = l_1.id \\ \t1 \land sys.sysconnector \; c.Sink = l_2.id \\ \also l_1' = l_1 \\ current_1' = current_1 \\ in_1' = in_1 \\ out_1' = out_1 \\ port_1' = port_1 \\ ctrl_1' = taked\_callout \\ \also l_2' = l_2 \\ current_2' = current_2 \\ in_2' = l_1.id \\ out_2' = out_2 \\ port_2' \ndres \{ (receive,l_1.id) \} = port_2 \ndres \{ (receive,l_1.id) \} \\ port_2' \; receive \; l_1.id = port_1 \; send \; out_1 \\ ctrl_2' = receive\_callin \\ \end{schema} \begin{schema}{System\_DeliverReturn} System \Phi 2Layer\_State \\ \where \exists l_1,l_2:layername @ ln_1? = l_1 \land ln_2? = l_2 \\ \also ctrl_1 = send\_return\_callout \\ % Estados correctos ctrl_2 = taked\_callout \\ \also in_1 = l_2.id \\ % Devuelvo al a quien lo puso! out_2 = l_1.id \\ % Devuelvo al a quien lo puso! \also % (l_1.id, returnby? (port_1 \; return \; in_1) \in l_2.import \\ port_2 \; send \; out_1 = returnby? (port_1 \; return \; in_1) \\ \also \exists c:connectorname @ \\ \t1 \land sys.sysconnector \; c.Source.id = l_1.id \\ \t1 \land sys.sysconnector \; c.Sink = l_2.id \\ \also l_1' = l_1 \\ current_1' = current_1 \\ in_1' = in_1 \\ out_1' = out_1 \\ port_1' = port_1 \\ ctrl_1' = ready \\ \also l_2' = l_2 \\ current_2' = current_2 \\ in_2' = in_2 \\ out_2' = out_2 \\ port_2' \ndres \{ (returned, out_2) \} = port_2 \ndres \{ (returned,out_2) \} \\ port_2' \; returned \; out_2 = port_1 \; return \; in_1 \\ ctrl_2' = receive\_return\_callout \\ \end{schema} \begin{syntax} Total\_System\_Compute \defs \\ \t1 System\_Layer\_Compute \\ \t1 \lor System\_DeliverCallIn \\ \t1 \lor System\_DeliverReturn \\ \end{syntax} Nota: Faltaria armar lo de la traza, pero ya estoy hecho mierda! :), despues debo explicar todas las ideas de aca puse...por que de lo contrario despues se me escapan de la cabeza! ZZZZZZZZZZZZZZZZZ \end{document} % % EJERCICIO 4 % \section{Pilas} Es una especificaci\'on de un dominio ``bien comprendido''. \begin{schema}{Pila[X]} stack : \seq X \end{schema} \begin{schema}{Push[X]} \Delta Pila[X] elem? : X \where stack' = \cat stack \end{schema} \begin{schema}{Top[X]} \Xi Pila[X] elem! : X \where elem! = head~ stack \end{schema} \begin{schema}{Retract[X]} \Delta Pila[X] \where stack' = tail~ stack \end{schema} \begin{schema}{Empty[X]} Pila[X] \where stack = <> \end{schema} \begin{schema}{InitPila[X]} Pila[X] \where stack = <> \end{schema} \begin{syntax} T\_Retract[X] = ( \lnot Empty[X] \land Restract[X] ) \lor (Empty[X] \land \Xi Pila) \\ T\_Top[X] = ( \lnot Empty[X] \land Top[X] ) \lor (Empty[X] \land \Xi Pila) \also Stack[X] \defs InitPila[X] \lor Push[X] \lor T\_Retract[X] \lor T\_Top[X] \lor \Xi Pila[X] \end{syntax} \begin{itemize} \item ({\bf Maxi}) ?`Esta bien usado los {\it schemas} parametricos?. \end{itemize} % % EJERCICIO 5 % \section{Base de datos cinematografica} Voy a especificar a la base de datos, o mejor dicho el estado de la base de datos, como varias tablas separadas como se modela en los sistemas de base de datos reales.?`Que gano? , poder concentrarme en las diferentes subpartes de la base de datos, modelar su estados respectivos, y luego unir todo. Empezamos con la tabla de directores, solo se presentara la operaci\'on de altas ya que el problema no exije ninguna otra. \begin{syntax} CODIGO == \nat \also TITULO == TEXT \also DIRECTOR == TEXT \also GUIONISTA == TEXT \also DIRECTORES == \power DIRECTOR \also GUIONISTAS == \power GUIONISTA \also TITULOS == \power TITULO \end{syntax} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DIRECTORES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{schema}{InDirector} direc? : DIRECTOR \where \#direc? > 0 \end{schema} \begin{schema}{Directores} directores : DIRECTORES \where \forall d:directores @ d \neq <> \end{schema} \begin{schema}{InitDirectores} Directores \where directores = \varnothing \end{schema} \begin{schema}{AddDirector} \Delta Directores \\ InDirector \where directores' = directores \bigcup \{direc?\} \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% GUIONISTA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modelamos la tabla de guionistas. \begin{syntax} InGuionista \defs InDirector [guion?/direc?, GUIONISTA/DIRECTOR] \end{syntax} \begin{schema}{Guionistas} guionistas : GUIONISTAS \where \forall g:guionistas @ g \neq <> \end{schema} \begin{schema}{AddGuionista} \Delta Guionistas InGuionista \where guionistas' = guionistas \bigcup \{guion?\} \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TITULOS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Vamos a especificar la base de datos de los titulos de la pelicula. \begin{schema}{InTitulo} tit? : TITULO \where \#tit? > 0 \end{schema} \begin{schema}{Titulos} titulos : TITULOS \where \forall t:titulos @ t \neq <> \end{schema} \begin{schema}{InitTitulos} Titulos \where titulos = \varnothing \end{schema} \begin{schema}{AddTitulo} \Delta Titulos InTitulo \where titulos' = titulos \bigcup \{tit?\} \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% RELACIONES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Vamos a especificar la relaci\'on entre guionistas y titulos de peliculas. \begin{schema}{GuionTit} guion\_tit : GUIONISTA \rel TITULO \\ Titulos \\ Guionistas \where \forall g\_t : guion\_tit @ \exists g:guionistas @ \exists t:titulos @ g\_t = (g, t) \end{schema} \begin{schema}{AddGuionTit} \Delta GuionTit \\ InTitulo \\ InGuionista \where tit? \in titulos \\ guion? \in guionistas \also guion\_tit' = guion\_tit \bigcup \{guion?, tit?\} \\ \theta Guionistas' = \theta Guionistas \\ \theta Titulos' = \theta Titulos \end{schema} \begin{schema}{InitGuionTit} GuionTit \where guion\_tit = \varnothing \end{schema} Vamos a especificar la relaci\'on entre directores y titulos de peliculas. \begin{schema}{DirecTit} direc\_tit : DIRECTOR \rel TITULO \\ Titulos \\ Directores \where \forall d\_t : direc\_tit @ \exists d:directores @ \exists t:titulos @ d\_t = (d, t) \end{schema} \begin{schema}{AddDirecTit} \Delta DirecTit \\ InTitulo \\ InDirector \where tit? \in titulos \\ direc? \in directores \also direc\_tit' = direc\_tit \bigcup \{direc?, tit?\} \\ \theta Drectores' = \theta Directores \\ \theta Titulos' = \theta Titulos \end{schema} \begin{schema}{InitDirecTit} DirecTit \where direc\_tit = \varnothing \end{schema} Terminado ya de especificar las diferentes tablas necesarias de mi base de datos las voy a juntar para formar la misma. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BASE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{schema}{Peliculas} GuionTit \\ DirecTit \end{schema} \begin{schema}{InitPeliculas} GuionTit \\ DirecTit \where InitTitulos \\ InitDirectores \\ InitGuionistas \\ InitDirecTit \\ InitGuionTit \end{schema} \begin{schema}{AddPeliculaPel} \Delta Peliculas \\ InTitulo \\ InDirector \\ InGuionista \where AddGuionTit \\ AddDirecTit \end{schema} Ahora tengo que hacer la ``promoci\'on de operadores'' de mis componentes, como debido a que tengo una sola de cada una puede prescindir de las funciones que operan sobre nombres (NAME). \begin{schema}{AddDirectorPel} \Delta Peliculas \\ \Xi GuionTit \\ AddDirector \where direc\_tit' = direc\_tit \end{schema} \begin{schema}{AddGuionistaPel} \Delta Peliculas \\ \Xi DirecTit \\ AddGuionista \where guion\_tit' = guion\_tit \end{schema} \begin{schema}{AddTituloPel} \Delta Peliculas \\ \Xi Directores \\ \Xi Guionistas \\ AddTitulo \where direc\_tit' = direc\_tit \\ guion\_tit' = guion\_tit \end{schema} Consultas sobre la base de datos. \begin{schema}{ConsultaGuionista} \Xi Peliculas \\ InGuionista \\ titulos! : TITULOS \where titulos! = guion\_tit \limg \{guion?\} \rimg \end{schema} \begin{schema}{ConsultaDirector} \Xi Peliculas \\ InDirector \\ titulos! : TITULOS \where titulos! = direc\_tit \limg \{direc?\} \rimg \end{schema} \begin{schema}{ModDirectorPel} \Delta Peliculas \\ InDirec_o \\ InDirec_n \where direc?_o \in directores \\ \exists t: titulos @ (direc?_o, t) \in direc\_pel \also directores' = directores \setminus \{direc?_o\} \bigcup \{direc?_n\} \\ direc\_tit' = \{direc?_o\} \ndres direc\_tit \\ \t3 \bigcup \{ t : titulos | t \in direc\_tit \limg \{direc?_o\} \rimg @ \\ \t3 direc?_n \mapsto t \} \\ \Xi GuionTit \end{schema} \begin{schema}{InitPeliculas} InitTitulos \\ InitDirectores \\ InitGuionistas \\ InitDirecTit \\ InitGuionTit \\ InitPeliculas \\ \end{schema} \begin{syntax} Base \defs AddPeliculaPel \lor AddTituloPel \lor AddDirectorPel \lor AddGuionistaPel \\ \t1 \lor AddDirecTit \lor AddGuionTit \lor ConsultaGionista \lor ConsultaDirector \\ \t1 \lor ModDirectorPel \lor InitPeliculas \lor \Xi Peliculas \end{syntax} \begin{itemize} \item ({\bf Maxi}) Aca hice un {\it schema} por cada entrada de datos validandolo, de esta manera la validacion la escribo una sola vez pudiendolo usar varias veces. Ademas puedo llegar a escribir propiedades como $\forall \, InDirector \, \dots$. ?`Esta bien?. \item ({\bf Maxi}) Al principio habia pensado en una especie de c\'odigo de director, c\'odigo de guionista, etc; debido a que este es un mecanismo para evitar repeticiones en una base de datos. Pero yo aca en $Z$ lo hice mediante conjuntos, los cuales netamente no repiten datos.?`Esta bien este nivel de abstracci\'on?. \item ({\bf Maxi}) La semantica del sistema que yo le di con respecto al hacer alguna operacion que recibe datos de entradas es: lee los datos de entrada y si estos son correctos realizo la operaci\'on correspondiente, de lo contrario no cambio la base de datos. Para lograr esto solo arme {\it schemas} que funcionan sobre ciertas precondiciones, no arme {\it schemas} que me digan que pasa si estas no se cumplen ?`por qu\'e?, para eso agrego al final de la especificacion del sistema el $\Xi$. ?`Es correcto?. En el caso de que al no cumplirse las precondiciones se comportara de otra manera, emitiendo alguna alarma, si deberia especificarlo ?`Es asi?. \item ({\bf Maxi}) Aca la semantica de ingresar algun dato repetido en no cambiar el estado de la base. ?`Esta bien?, ?`Es una opcion de especificacion a seguir?. \end{itemize} % % EJERCICIO 6 % \section{Editor y otras cositas} \begin{enumerate}[a)] \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{axdef} left\_arrow : CHAR \where left\_arrow \nin printing \end{axdef} \begin{schema}{LeftArrow} ch?: CHAR \where ch? = left\_arrow \end{schema} \begin{schema}{Backward} \Delta Editor \\ LeftArrow \where left' = left \cat \\ right' = right \end{schema} \begin{schema}{BOF} Editor \where left = <> \end{schema} \begin{syntax} T\_Backward \defs (\lnot BOF \land Backward) \lor (BOF \land LeftArrow \land \Xi Editor) \end{syntax} \begin{axdef} del\_key : CHAR \where del\_key \nin printing \end{axdef} \begin{schema}{DelKey} ch? : CHAR \where ch? = del\_key \end{schema} \begin{schema}{Delete} \Delta Editor DelKey \where left' = left right' = tail right \end{schema} \begin{syntax} T\_Delete \defs (\lnot EOF \land Delete) \lor (EOF \land DelKey \land \Xi Editor) \end{syntax} \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{syntax} NoOpKey \defs [ch?:CHAR | ch? \notin printing] \land \\ \t2 \lnot DelKey \land \lnot LeftArrow \land \lnot RightArrow \land \Xi Editor \\ \end{syntax} \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{itemize} \item ({\bf Maxi}): No especifico que el archivo pertenezca al {\it filesystem} ya que al mismo lo voy a denotar por su contenido que es lo que me interesa.?`Esta bien? \item Ademas no todo archivo (flujo de datos) esta dentro del {\it filesystem}, recordar los {\it pipes} del {\it Kernel} de Linux. \end{itemize} \begin{syntax} FILE == TEXT \end{syntax} \begin{schema}{LoadFile} \Delta Editor file? : FILE \where left' = <> right' = file? \end{schema} \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Estados del esquema $EOF$. \begin{syntax} right = <> \\ left = < \mbox{todos las posibles {\it strings}, sean o no caracteres ``imprimibles''} > \end{syntax} No voy a sacar exactamente la cantidad de estado, ya que eso no me aporta mucha informaci\'on en este nivel de abstraccion, sino que calculare el orden de los mismos. (Ver hoja anexa escrita a mano). \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{verbatim} data Editor = Edit String String insert:: Char -> Editor -> Editor printing :: Char -> Bool insert ch (Edit left right) | printing ch = Edit (ch:left) right | otherwise = Edit left right \end{verbatim} \begin{itemize} \item Notaremos que en los esquemas {\it Insert, Delete, Fordward, Backward} siempre se agrega algo al final de {\it left}. \item Representaremos nuestro editor mediante el constructor {\texttt{Editor left right}}, donde el primer elemento de {\it left} es el ultimo caracter en la variable {\it left} de los {\it schemas}. \item el string {\texttt{right}} tiene la misma semantica que la variable {\it right} que aparece en los {\it schemas}. \item Viendo todo lo anterior vemos que se realizan $O(1)$ operaciones $(:)$. \item ({\bf Maxi}) ?`Era esto lo que habia que hacer? \end{itemize} \item %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{syntax} \forall Editor | Init @ EOF \equiv \\ \forall left, right : TEXT | left = <> \land right = <> @ right = <> \end{syntax} \end{enumerate} % % EJERCICIO 7 % \section{Contestador} Vamos a tratar de definir cintas de contestador, esto se realizo as\'i despues de ver varias formas diferentes de especificar este ejercicio llegando a esta version mucho mas simplificada y clara. \begin{syntax} [MSG] \end{syntax} \begin{schema}{Cinta} msgs : \seq MSG \end{schema} \begin{schema}{InitCinta} Cinta \where msgs = <> \end{schema} \begin{schema}{AddCinta} \Delta Cinta \\ msg? : MSG \where msgs' = msgs \cat \end{schema} \begin{schema}{RemoveCinta} \Delta Cinta \\ msg! : MSG \where msgs \neq <> \also msg! = head~ msgs \\ msgs' = tail~ msgs \end{schema} Vamos ahora a especificar el contestador. \begin{axdef} play, save : NAME \\ cintas : \power NAME max : \nat \where play \in cintas \\ save \in cintas \also max > 0 \end{axdef} \begin{syntax} LIGHT & ::= on | off \also BOTON & :: = play | save | any \end{syntax} \begin{schema}{Contestador} cinta : cintas \fun Cinta \\ full : LIGHT \\ btn : BOTON \\ speaker : MSG \where btn \in \{any,save\} \Rightarrow \#( (cinta~play).msgs \cat (cinta~save).msgs ) \leq max \\ btn \in \{play\} \Rightarrow \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 \leq max \also btn \in \{any, save\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) = max \\ \t1 \Rightarrow full = on \\ btn \in \{play\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 = max \\ \t1 \Rightarrow full = on \also btn \in \{any, save\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) < max \\ \t1 \Rightarrow full = off \\ btn \in \{play\} \land \#( (cinta~play).msgs \cat (cinta~save).msgs ) + 1 < max \\ \t1 \Rightarrow full = off \end{schema} Vamos a promover el {\it schema} Cinta al nivel del contestador. \begin{schema}{Contestador \Phi Cinta} \Delta Contestador \\ \Delta Cinta \\ ct? : NAME \where \{ct?\} \ndres cinta = \{ct?\} \ndres cinta \\ \theta Cinta = cinta \{ct?\} \\ \theta Cinta' = cinta' \{ct?\} \end{schema} \begin{axdef} null : MSG \end{axdef} \begin{schema}{InitContestador} Contestador \where btn = any \\ speaker = null \also \forall c:cintas @ cinta~ c = \theta InitCinta \end{schema} \begin{schema}{Play} Contestador \Phi Cinta \\ RemoveCinta \where ct?=play \iff \#(cinta~ play).msgs \neq <> \\ ct?=save \iff \#(cinta~ play).msgs = <> \also speaker' = msg! \\ btn' = play \end{schema} \begin{schema}{Save} Contestador \Phi Cinta \\ AddCinta \where btn = play \also ct?=save \\ msg? = speaker \also btn' = save \\ speaker' = speaker \end{schema} \begin{schema}{Call} Contestador \Phi Cinta \\ AddCinta \\ msg\_callin? : MSG \where full = off \also ct? = play \\ msg? = msg\_callin? \\ \also btn' = any \\ speaker' = speaker \end{schema} \begin{syntax} T\_Contestador \defs InitContestador \lor Play \lor Save \lor \Xi Contestador \end{syntax} \begin{itemize} \item ({\bf Maxi}) Cuando defino el conjunto de nombres que representan a los componentes o subsistemas generalmente se hace $x \in C$, pero no se aclara nada de si en $C$ hay mas cosas o no se dice $\{x\}=C$ (Jacky lo hace asi!). ?` Qu\'e estilo opto?, como esta hecho el contestador o como trabaja Jacky es m\'as abstracto ya que yo pienso en la especificaci\'on no por el contenido exacto de $C$. \item ({\bf Maxi}) ?`Es valido poner un valor nulo de un tipo de datos como para inicializar con ese valor alguna variable de un {\it schema}? (ver el {\it schema} de inicializaci\'on del contestador). \item ({\bf Maxi}) Aca cuando ninguna precondici\'on se cumpla en el contestador va a quedar inmutable es su estado ($\Xi$). Por lo cual solo me intereso en especificar las operaciones exijiendo las precondiciones sobre las cuales son validas solamente.?`Esta bien?. \item ({\bf Maxi}) Ver la especificaci\'on del contestador que hice en papel, comentar que a esta version llegue luego de varias especificaciones. ?`Esta mal?. \end{itemize} % % EJERCICIO 8 % \section{Pipes} Primero voy a definir un {\it stream}, el cual, es la modelizaci\'on y la unidad de redireccionamiento en Unix. \begin{schema}{Stream} stream : TEXT \end{schema} Una vez hecho esto, modelo la tabla de descriptores de archivos de un proceso mediante una funci\'on. Todo proceso debe tener almenos dos {\it streams} asociados a el, los cuales son entrada y salida estandar. \begin{syntax} PID == \nat \also STDIN == 0 \\ STDOUT == 1 \also SOURCE == 0 \\ DEST == 1 \\ \also ROLL\_PROC == \{0,1\} \end{syntax} \begin{schema}{Proceso} pid : PID \\ descrip : \nat \pfun Stream \where \exists i,o:Stream @ descrip~ STDIN = i \land descrip~ STDOUT = o \end{schema} Modelamos ahora un {\it pipe} como un vinculo entre dos procesos, ese vinculo es justamente la redireccion de la entrada/salida estandar. \begin{schema}{Pipe} proceso: ROLL\_PROC \fun Proceso \where (proceso~ SOURCE).descrip~ STDOUT = (proceso~ DEST).descrip~ STDIN \\ (proceso~ SOURCE).descrip~ STDIN = (proceso~ DEST).descrip~ STDOUT \\ \end{schema} % % EJERCICIO 9 % \section{Despachante} Aca voy a armar es despachante apartir de sus componentes o subsistemas. Al armar una especificaci\'on siguiendo este estilo es importante tener en cuenta la promoci\'on de operadores, los cuales me permiten ``realizar'' operaciones sobre un subsistema desde el nivel del sistema. Primero voy a especificar el buffer, junto con sus operaciones ofrecidas. %%%%%%%%%%%%%%%%%%%%%%%%%%% BUFFER %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{syntax} YESNO & ::= yes | no \also MSG == TEXT \end{syntax} \begin{axdef} max\_buff: \nat \\ \where max\_buff > 0 \end{axdef} \begin{schema}{Buff} buffer: \seq MSG \\ isfull: YESNO isempty : YESNO \where \#buffer <= max\_buff \\ isfull = yes \iff \#buffer = max\_buff \also \#buffer > 0 \iff isempty = no \\ \end{schema} \begin{axdef} parity: MSG \fun YESNO \end{axdef} \begin{schema}{PutBuff} \Delta Buff \\ msg?: MSG \where isfull = no \also parity~ msg? = yes \implies buffer' = buffer \cat \\ parity~ msg? = no \implies buffer' = buffer \end{schema} \begin{schema}{GetBuff} \Delta Buff \\ msg! : MSG \where isempty = no \also msg! = head~ buffer \\ buffer' = tail~ buffer \end{schema} \begin{schema}{FullBuff} Buffer \where isfull = yes \end{schema} \begin{schema}{EmptyBuff} Buffer \where isempty = yes \end{schema} \begin{syntax} Buffer \defs ( PutBuff \lor (FullBuff \land \Xi Buff) ) \lor \\ \t2 ( GetBuff \lor (EmptyBuff \land \Xi Buff) ) \end{syntax} %%%%%%%%%%%%%%%%%%%%%%%%%%% CANALES %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Vamos a especificar ahora los canales junto con las operaciones sobre el mismo. \begin{axdef} null : MSG \end{axdef} \begin{schema}{Ch} ch\_dato: MSG \\ error!: YESNO \where error! = parity~ ch\_dato \end{schema} \begin{schema}{ReadCh} \Delta Ch \\ in?: MSG \where ch\_dato' = in? \end{schema} \begin{schema}{PutCh} \Delta Ch \\ out? : MSG \where ch\_dato' = out? \end{schema} \begin{schema}{InitCh} Ch \where ch\_dato = null \\ error! = no \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%% DESPACHANTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Vamos a componer los subsistemas especificados mediante las tecnicas de asignarle a cada componente un nombre. \begin{axdef} in1, in2, out1 : NAME \\ ChEntradas, ChSalidas : \power NAME \\ canales : \power NAME \\ \where \{in1, in2\} \in ChEntradas \\ \{out1\} \in ChSalidas \\ canales = ChEntradas \bigcap ChSalidas \\ \end{axdef} \begin{schema}{Despachante} canal: canales \fun Ch \\ Buffer vaciando : YESNO \where \#canal = 3 \also FullBuff \implies vaciando = yes EmptyBuff \implies vaciando = no \end{schema} Voy a promover el {\it schema} canal al nivel del despachante para luego poder aplicar las operaciones del buffer al nivel del sistema. \begin{schema}{Despachante \Phi Ch} \Delta Despachante \\ \Delta Ch \\ ch?: canales \where \{ch?\} \ndres canal' = \{ch?\} \ndres canal \\ \theta Ch = canal~ ch? \\ \theta Ch' = canal'~ ch? \end{schema} Modelamos cuando llega un dato por un canal. \begin{schema}{ComeInCh} \Delta Despachante \Phi Ch \\ ReadCh \\ PutBuff \where ch? \in ChEntradas \also msg? = in? \end{schema} \begin{schema}{ComeOutCh} \Delta Despachante \Phi Ch \\ PutCh \\ GetBuff \where \lnot(EmptyBuff) \\ ch? \in ChSalidas \also out? = msg! \end{schema} \begin{schema}{InitDespachante} Despachante \where \forall c:canales @ canal~ c = \theta InitCh \\ InitBuff \end{schema} \begin{schema}{Vaciando} Despachante \where vaciando = yes \end{schema} \begin{syntax} T\_Despachante \defs InitDespachante \lor (Vaciando \land ComeOutCh) \lor \\ \t4 (\lnot Vaciando \land ComeInCh) \lor \Xi Despachante \end{syntax} \begin{itemize} \item ({\bf Maxi}) Aca el problema del despachante fue modelar la salida, ya que esto se puede pensar como un conjunto de instrucciones secuenciales de sacar de a un elemento el buffer, por otro lado yo antes la especificacion la habia hecho de tal manera que cuando se llenaba el buffer se devolvia, mediante una variable de salida del mismo tipo del buffer, todos los mensajes. ?`Que es mejor?, la que hice aca es mas larga pero no deja de espresar que hay UN canal de salida, mientras que pensandolo de la otra manera no se sabe. \item ({\bf Maxi}) Al poner el $\Xi$ al final siempre cuando defino un sistema es debido a que hay estados que si me interesan a la hora de tomar las decisiones sobre las operaciones brindadas (precondiciones) pero cuando estas no se cumplen el sistema no tiene que hacer nada. ?`Es por eso?. \item ({\bf Maxi}) Cuando poseo por ejemplo tres {\it schemas} $A,B,C$ y sus tres precondiciones se cumplen ?` Es valido?, con eso estoy denotando que me da lo mismo realizar cualquiera de las tres operaciones o que estan las tres disponibles al mismo tiempo.?`Esta bien?. \end{itemize} % % EJERCICIO 10 % \section{Guardia de Hospital} Aca nuevamente vamos a especificar las componentes del sistema junto con las operaciones que ellas ofrecen pero luego integrar todo en el sistema. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DISPOSITIVO %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Empezamos modelando un dispositivo. \begin{syntax} LECTURA == \num \also STATUS ::= ok | fault \also ALARMA ::= falla\_disp | fuera\_rango | nada \end{syntax} \begin{schema}{Rango} minimo, maximo : LECTURA \where minimo \leq maximo \end{schema} \begin{schema}{Dispositivo} Rango \\ lectura : LECTURA \\ func : STATUS \\ alarma : ALARMA \\ \where func = fault \iff alarma = falla\_disp \\ func = ok \iff alarma = nada \\ \lnot(minimo \leq lectura \leq maximo) \iff alarma = fuera\_rango \end{schema} \begin{axdef} check : Dispositivo \fun STATUS \end{axdef} \begin{schema}{Lectura} \Delta Dispositivo \\ \Xi Rango \\ lectura? : LECTURA \where check~ \theta Dispositivo = ok \also lectura' = lectura? \\ func' = ok \end{schema} \begin{schema}{ErrorDisp} \Delta Dispositivo \\ \Xi Rango \where check~ \theta Dispositivo = fault \also func' = fault \\ lectura' = lectura \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BOX %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modelas el {\it box} de enfermeria donde van los mensajes de alarma. \begin{syntax} [NAME] \end{syntax} \begin{axdef} pacientes, dispositivos : \power NAME \where pacientes \bigcap dispositivos = \varnothing \end{axdef} \begin{schema}{Box} monitor: \seq pacientes \cross dispositivos \cross ALARMA \end{schema} \begin{schema}{PutBox} \Delta Box \\ msg\_box? : pacientes \cross dispositivos \cross ALARMA \where monitor' = monitor \cat \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% PACIENTE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modelamos a los pacientes. \begin{syntax} FREC == \num \end{syntax} \begin{schema}{Paciente} frec : FREC \\ disp\_adosados : \power Dispositivo \where frec >= 0 \\ \#disp\_adosados > 0 \end{schema} \begin{schema}{InitPaciente} Paciente \where \exists frec\_seteo : FREC @ frec = frec\_seteo \\ \exists disp\_inicial : dispositivos @ disp\_inicial \in disp\_adosados \end{schema} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% BASE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Modelamos la base de datos que almacena las lecturas. \begin{schema}{Base} base : \seq pacientes \cross dispositivos \cross LECTURA \\ \end{schema} \begin{schema}{PutBase} \Delta Base reg?: pacientes \cross dispositivos \cross LECTURA \where base' = base \cat \end{schema} \begin{schema}{InitBase} Base \where base = <> \end{schema} Ahora juntamos todo en el sistema. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% GUARDIA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{schema}{Guardia} dispositivo : dispositivos \fun Dispositivo \\ paciente : pacientes \fun Paciente \\ Base \\ Box \where \forall p_1,p_2:pacientes | p_1 \neq p_2 @ \\ \t1 (paciente p_1).disp\_adosados \bigcap (paciente p_2).disp\_adosados = \varnothing \end{schema} Vamos a promover el {\it schema} dispositivo al nivel del sistema. \begin{schema}{Guardia \Phi Dispositivo} \Delta Guardia \\ \Delta Dispositivo \\ disp? : dispositivos \where \{disp?\} \ndres dispositivo = \{disp?\} \ndres dispositivo' \\ \theta Dispositivo = dispositivo~ disp? \theta Dispositivo' = dispositivo'~ disp? \end{schema} \begin{schema}{LecturaDisp} Guardia \Phi Dispositivo \\ Lectura \\ PutBase \where \exists p:pacientes @ disp? \in (paciente p).disp\_adosados \land \\ \t2 reg? = (p, disp?, lectura?) \end{schema} \begin{schema}{FalloDisp} Guardia \Phi Dispositivo \\ ErrorDisp \\ PutBox \\ \Xi Base \where \exists p:pacientes @ disp? \in (paciente p).disp\_adosados \land \\ \t1 msg\_box? = (p, disp?, alarma') \end{schema} \begin{schema}{InitGuardia} Guardia \where \forall d:dispositivos @ dispositivo~ d = \theta InitDispositivo \\ \forall p:pacientes @ paciente~ p = \theta InitPaciente \\ \also InitBox \\ InitBase \end{schema} \begin{syntax} GuardiaHospital \defs InitGuardia \lor LecturaDisp \lor FalloDisp \lor \Xi Guardia \end{syntax} \begin{itemize} \item ({\bf Maxi}) Existe una variable de {\it Dispositivo} llamada alarma, que su funci\'on es comunicar al exterior un estado del dispositivo. Si hubiese puesto como variable de estado {\it alarma!} en vez de {\it alarma}, ?` Hay alguna contradicci\'on con la convenci\'on de nombres de variables? \item ({\bf Maxi}) Para chequear que un dispositivo ande utilizo una funci\'on externa que no la descripvo como funciona sino lo que hace. ?`Esta bien? \item ({\bf Maxi}) Cuando hago la lectura del dispositivo use una variable para representar un valor proveniente de ``afuera'', pero mi pregunta es: ?` Se entiende que es una lectura de ese dispositivo?. ?`Tengo que especificar m\'as?. (por ejemplo una funcion que dado un dispositivo o alguna clase de id me devuelva la lectura). Es mas que nada por un tema de semantica. \item ({\bf Maxi}) Ver el {\it schema} paciente, ?`Cuando quiero decir algo que desconozco uso un existencial?. Ver tambi\'en {\it LecturaOk}. \end{itemize} \end{document}