Towards a Maude Formal Environment

Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in the development of formal analysis tools for checking specific properties of Ma...

Full description

Autores:
Durán, Francisco
Rocha, Camilo
Álvarez, José María
Tipo de recurso:
Part of book
Fecha de publicación:
2011
Institución:
Escuela Colombiana de Ingeniería Julio Garavito
Repositorio:
Repositorio Institucional ECI
Idioma:
eng
OAI Identifier:
oai:repositorio.escuelaing.edu.co:001/1890
Acceso en línea:
https://repositorio.escuelaing.edu.co/handle/001/1890
Palabra clave:
MAUDE
Obligación de prueba
Objeto controlador
Objeto de herramienta
MFE
Critical Pair
Proof Obligation
Tool Object
Active Tool
Controller Object
Rights
closedAccess
License
© Springer-Verlag Berlin Heidelberg 2011
id ESCUELAIG2_ff1e81a3dd8b7a9eb960bb976bb706ad
oai_identifier_str oai:repositorio.escuelaing.edu.co:001/1890
network_acronym_str ESCUELAIG2
network_name_str Repositorio Institucional ECI
repository_id_str
dc.title.eng.fl_str_mv Towards a Maude Formal Environment
title Towards a Maude Formal Environment
spellingShingle Towards a Maude Formal Environment
MAUDE
Obligación de prueba
Objeto controlador
Objeto de herramienta
MFE
Critical Pair
Proof Obligation
Tool Object
Active Tool
Controller Object
title_short Towards a Maude Formal Environment
title_full Towards a Maude Formal Environment
title_fullStr Towards a Maude Formal Environment
title_full_unstemmed Towards a Maude Formal Environment
title_sort Towards a Maude Formal Environment
dc.creator.fl_str_mv Durán, Francisco
Rocha, Camilo
Álvarez, José María
dc.contributor.author.none.fl_str_mv Durán, Francisco
Rocha, Camilo
Álvarez, José María
dc.contributor.researchgroup.spa.fl_str_mv Informática
dc.subject.armarc.eng.fl_str_mv MAUDE
topic MAUDE
Obligación de prueba
Objeto controlador
Objeto de herramienta
MFE
Critical Pair
Proof Obligation
Tool Object
Active Tool
Controller Object
dc.subject.armarc.spa.fl_str_mv Obligación de prueba
Objeto controlador
Objeto de herramienta
dc.subject.armarc.ENG.fl_str_mv MFE
dc.subject.proposal.eng.fl_str_mv Critical Pair
Proof Obligation
Tool Object
Active Tool
Controller Object
description Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in the development of formal analysis tools for checking specific properties of Maude specifications. This includes tools for checking termination, confluence, and inductive properties of rewrite theories. Nevertheless, most of these tools have been designed to work in isolation, making it difficult, for instance, to exchange data between them and inconvenient to switch between their environments. This paper presents the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can interact with tools to mechanically verify properties of Maude specifications. One important aspect of this work is that the MFE has been designed to be easily extended with tools having highly heterogeneous designs whilst creating synergy among them. As a proof of concept, we report on the integration of five commonly used formal analysis tools for Maude specifications into MFE and illustrate their interoperability with an example.
publishDate 2011
dc.date.issued.none.fl_str_mv 2011
dc.date.accessioned.none.fl_str_mv 2021-12-03T16:17:47Z
dc.date.available.none.fl_str_mv 2021-12-03T16:17:47Z
dc.type.spa.fl_str_mv Capítulo - Parte de Libro
dc.type.coar.fl_str_mv http://purl.org/coar/resource_type/c_2df8fbb1
dc.type.coarversion.fl_str_mv http://purl.org/coar/version/c_970fb48d4fbd8a85
dc.type.version.spa.fl_str_mv info:eu-repo/semantics/publishedVersion
dc.type.coar.spa.fl_str_mv http://purl.org/coar/resource_type/c_3248
dc.type.content.spa.fl_str_mv Text
dc.type.driver.spa.fl_str_mv info:eu-repo/semantics/bookPart
dc.type.redcol.spa.fl_str_mv http://purl.org/redcol/resource_type/ART
format http://purl.org/coar/resource_type/c_3248
status_str publishedVersion
dc.identifier.isbn.none.fl_str_mv 9783642249334
9783642249327
dc.identifier.uri.none.fl_str_mv https://repositorio.escuelaing.edu.co/handle/001/1890
identifier_str_mv 9783642249334
9783642249327
url https://repositorio.escuelaing.edu.co/handle/001/1890
dc.language.iso.spa.fl_str_mv eng
language eng
dc.relation.ispartofseries.none.fl_str_mv Lecture Notes in Computer Science;7000
dc.relation.citationendpage.spa.fl_str_mv 351
dc.relation.citationstartpage.spa.fl_str_mv 329
dc.relation.indexed.spa.fl_str_mv N/A
dc.relation.ispartofbook.eng.fl_str_mv Formal Modeling: Actors, Open Systems, Biological Systems
dc.relation.references.spa.fl_str_mv User interfaces for theorem provers, http://www.informatik.uni-bremen.de/uitp/
Aspinall, D., Lüth, C.: Special issue on user interfaces in theorem proving. Journal of Automated Reasoning 39(2) (2007) Google Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002) Google Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)
Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)
Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 173–178. Springer, Heidelberg (2007)
Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006)
Durán, F., Lucas, S., Bevilacqua, V.: MTT: The Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313–319. Springer, Heidelberg (2008)
Durán, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electronic Notes in Theoretical Computer Science 248, 93–113 (2009)
Durán, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246–262. Springer, Heidelberg (2009)
Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications. In: Ölveczky, P. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)
Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)
Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (2007)
Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming (submitted for publication, 2011)
Durán, F., Ölveczky, P.C.: A guide to extending Full Maude illustrated with the implementation of Real-Time Maude. Electronic Notes in Theoretical Computer Science 238(3), 83–102 (2009)
Franssen, M., van den Brand, M.: Design of a proof repository architecture. In: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009), pp. 19–23. ACM (2009)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Hemer, D., Long, G., Strooper, P.: Plug-in proof support for formal development environments. In: Proceedings of the 2005 Australasian Symposium on Theory of Computing (CATS 2005), pp. 69–79. Australian Computer Society, Inc. (2005)
Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, University of Illinois at Urbana-Champaign (2008)
Hendrix, J., Clavel, M., Bevilacqua, V.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)
Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)
Lucas, S.: MU-TERM: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200–209. Springer, Heidelberg (2004)
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)
Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of rewrite theories. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 594–609. Springer, Heidelberg (2010)
dc.rights.eng.fl_str_mv © Springer-Verlag Berlin Heidelberg 2011
dc.rights.coar.fl_str_mv http://purl.org/coar/access_right/c_14cb
dc.rights.uri.spa.fl_str_mv https://creativecommons.org/licenses/by/4.0/
dc.rights.accessrights.spa.fl_str_mv info:eu-repo/semantics/closedAccess
dc.rights.creativecommons.spa.fl_str_mv Atribución 4.0 Internacional (CC BY 4.0)
rights_invalid_str_mv © Springer-Verlag Berlin Heidelberg 2011
https://creativecommons.org/licenses/by/4.0/
Atribución 4.0 Internacional (CC BY 4.0)
http://purl.org/coar/access_right/c_14cb
eu_rights_str_mv closedAccess
dc.format.extent.spa.fl_str_mv 22 páginas.
dc.format.mimetype.spa.fl_str_mv application/pdf
dc.publisher.spa.fl_str_mv Springer
dc.publisher.place.spa.fl_str_mv Berlín
institution Escuela Colombiana de Ingeniería Julio Garavito
bitstream.url.fl_str_mv https://repositorio.escuelaing.edu.co/bitstream/001/1890/6/Towards%20a%20Maude%20Formal%20Environment.png
https://repositorio.escuelaing.edu.co/bitstream/001/1890/7/Towards%20a%20Maude%20Formal%20Environment.pdf.jpg
https://repositorio.escuelaing.edu.co/bitstream/001/1890/1/Towards%20a%20Maude%20Formal%20Environment.pdf
https://repositorio.escuelaing.edu.co/bitstream/001/1890/2/license.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1890/3/springer.pdf.txt
https://repositorio.escuelaing.edu.co/bitstream/001/1890/5/Towards%20a%20Maude%20Formal%20Environment.pdf.txt
bitstream.checksum.fl_str_mv 635bdf114d96ef098f67eb5c5c5d5eb4
0dd3bc5e98e3ae5c1d80fa57d6ab0bae
be9b098bc4d1ddfff3bec8d431433234
5a7ca94c2e5326ee169f979d71d0f06e
d784fa8b6d98d27699781bd9a7cf19f0
d784fa8b6d98d27699781bd9a7cf19f0
bitstream.checksumAlgorithm.fl_str_mv MD5
MD5
MD5
MD5
MD5
MD5
repository.name.fl_str_mv Repositorio Escuela Colombiana de Ingeniería Julio Garavito
repository.mail.fl_str_mv repositorio.eci@escuelaing.edu.co
_version_ 1814355595668488192
spelling Durán, Francisco5002c334b7fc9f7b4b49cbacec064e0c600Rocha, Camilo649eba80a4c919beefa7d19955bc2950600Álvarez, José Maríae51cc31bf714c23f2b7ffa8c350b6d00600Informática2021-12-03T16:17:47Z2021-12-03T16:17:47Z201197836422493349783642249327https://repositorio.escuelaing.edu.co/handle/001/1890Maude is a declarative and reflective language based on rewriting logic in which computation corresponds to efficient deduction by rewriting. Because of its reflective capabilities, Maude has been useful as a metatool in the development of formal analysis tools for checking specific properties of Maude specifications. This includes tools for checking termination, confluence, and inductive properties of rewrite theories. Nevertheless, most of these tools have been designed to work in isolation, making it difficult, for instance, to exchange data between them and inconvenient to switch between their environments. This paper presents the Maude Formal Environment (MFE), an executable formal specification in Maude within which a user can interact with tools to mechanically verify properties of Maude specifications. One important aspect of this work is that the MFE has been designed to be easily extended with tools having highly heterogeneous designs whilst creating synergy among them. As a proof of concept, we report on the integration of five commonly used formal analysis tools for Maude specifications into MFE and illustrate their interoperability with an example.Maude es un lenguaje declarativo y reflexivo basado en una lógica de reescritura en la que el cómputo corresponde a una deducción eficiente por reescritura. Debido a sus capacidades reflexivas, Maude ha resultado útil como metaherramienta en el desarrollo de herramientas de análisis formal para verificar propiedades específicas de las especificaciones de Maude. Esto incluye herramientas para verificar la terminación, la confluencia y las propiedades inductivas de las teorías de reescritura. Sin embargo, la mayoría de estas herramientas han sido diseñadas para funcionar de forma aislada, lo que dificulta, por ejemplo, el intercambio de datos entre ellas y dificulta el cambio entre sus entornos. Este documento presenta Maude Formal Environment (MFE), una especificación formal ejecutable en Maude dentro de la cual un usuario puede interactuar con herramientas para verificar mecánicamente las propiedades de las especificaciones de Maude. Un aspecto importante de este trabajo es que el MFE ha sido diseñado para ser ampliado fácilmente con herramientas que tienen diseños muy heterogéneos, creando sinergia entre ellos. Como prueba de concepto, informamos sobre la integración de cinco herramientas de análisis formales de uso común para las especificaciones de Maude en MFE e ilustramos su interoperabilidad con un ejemplo.22 páginas.application/pdfengSpringerBerlínLecture Notes in Computer Science;7000351329N/AFormal Modeling: Actors, Open Systems, Biological SystemsUser interfaces for theorem provers, http://www.informatik.uni-bremen.de/uitp/Aspinall, D., Lüth, C.: Special issue on user interfaces in theorem proving. Journal of Automated Reasoning 39(2) (2007) Google ScholarClavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: Specification and programming in rewriting logic. Theoretical Computer Science 285, 187–243 (2002) Google ScholarClavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework: How to Specify, Program, and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)Clavel, M., Durán, F., Eker, S., Meseguer, J., Stehr, M.O.: Maude as a formal meta-tool. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1684–1703. Springer, Heidelberg (1999)Clavel, M., Durán, F., Hendrix, J., Lucas, S., Meseguer, J., Ölveczky, P.: The Maude formal tool environment. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 173–178. Springer, Heidelberg (2007)Clavel, M., Palomino, M., Riesco, A.: Introducing the ITP tool: a tutorial. Journal of Universal Computer Science 12(11), 1618–1650 (2006)Durán, F., Lucas, S., Bevilacqua, V.: MTT: The Maude termination tool (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 313–319. Springer, Heidelberg (2008)Durán, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electronic Notes in Theoretical Computer Science 248, 93–113 (2009)Durán, F., Lucas, S., Meseguer, J.: Termination modulo combinations of equational theories. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 246–262. Springer, Heidelberg (2009)Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational Maude specifications. In: Ölveczky, P. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)Durán, F., Meseguer, J.: A Maude coherence checker tool for conditional order-sorted rewrite theories. In: Ölveczky, P. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 86–103. Springer, Heidelberg (2010)Durán, F., Meseguer, J.: Maude’s module algebra. Science of Computer Programming 66(2), 125–153 (2007)Durán, F., Meseguer, J.: On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories. Journal of Logic and Algebraic Programming (submitted for publication, 2011)Durán, F., Ölveczky, P.C.: A guide to extending Full Maude illustrated with the implementation of Real-Time Maude. Electronic Notes in Theoretical Computer Science 238(3), 83–102 (2009)Franssen, M., van den Brand, M.: Design of a proof repository architecture. In: Proceedings of the 1st Workshop on Modules and Libraries for Proof Assistants (MLPA 2009), pp. 19–23. ACM (2009)Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)Hemer, D., Long, G., Strooper, P.: Plug-in proof support for formal development environments. In: Proceedings of the 2005 Australasian Symposium on Theory of Computing (CATS 2005), pp. 69–79. Australian Computer Society, Inc. (2005)Hendrix, J.: Decision Procedures for Equationally Based Reasoning. Ph.D. thesis, University of Illinois at Urbana-Champaign (2008)Hendrix, J., Clavel, M., Bevilacqua, V.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165–174. Springer, Heidelberg (2005)Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151–155. Springer, Heidelberg (2006)Lucas, S.: MU-TERM: A tool for proving termination of context-sensitive rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 200–209. Springer, Heidelberg (2004)Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007)Rocha, C., Meseguer, J.: Constructors, sufficient completeness and deadlock freedom of rewrite theories. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 594–609. Springer, Heidelberg (2010)© Springer-Verlag Berlin Heidelberg 2011https://creativecommons.org/licenses/by/4.0/info:eu-repo/semantics/closedAccessAtribución 4.0 Internacional (CC BY 4.0)http://purl.org/coar/access_right/c_14cbTowards a Maude Formal EnvironmentCapítulo - Parte de Libroinfo:eu-repo/semantics/publishedVersionhttp://purl.org/coar/resource_type/c_3248http://purl.org/coar/resource_type/c_2df8fbb1Textinfo:eu-repo/semantics/bookParthttp://purl.org/redcol/resource_type/ARThttp://purl.org/coar/version/c_970fb48d4fbd8a85MAUDEObligación de pruebaObjeto controladorObjeto de herramientaMFECritical PairProof ObligationTool ObjectActive ToolController ObjectTHUMBNAILTowards a Maude Formal Environment.pngTowards a Maude Formal Environment.pngimage/png140872https://repositorio.escuelaing.edu.co/bitstream/001/1890/6/Towards%20a%20Maude%20Formal%20Environment.png635bdf114d96ef098f67eb5c5c5d5eb4MD56open accessTowards a Maude Formal Environment.pdf.jpgTowards a Maude Formal Environment.pdf.jpgGenerated Thumbnailimage/jpeg3473https://repositorio.escuelaing.edu.co/bitstream/001/1890/7/Towards%20a%20Maude%20Formal%20Environment.pdf.jpg0dd3bc5e98e3ae5c1d80fa57d6ab0baeMD57open accessORIGINALTowards a Maude Formal Environment.pdfTowards a Maude Formal Environment.pdfapplication/pdf189531https://repositorio.escuelaing.edu.co/bitstream/001/1890/1/Towards%20a%20Maude%20Formal%20Environment.pdfbe9b098bc4d1ddfff3bec8d431433234MD51open accessLICENSElicense.txtlicense.txttext/plain; charset=utf-81881https://repositorio.escuelaing.edu.co/bitstream/001/1890/2/license.txt5a7ca94c2e5326ee169f979d71d0f06eMD52open accessTEXTspringer.pdf.txtspringer.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1890/3/springer.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD53open accessTowards a Maude Formal Environment.pdf.txtTowards a Maude Formal Environment.pdf.txtExtracted texttext/plain2https://repositorio.escuelaing.edu.co/bitstream/001/1890/5/Towards%20a%20Maude%20Formal%20Environment.pdf.txtd784fa8b6d98d27699781bd9a7cf19f0MD55metadata only access001/1890oai:repositorio.escuelaing.edu.co:001/18902022-11-22 03:00:37.963open accessRepositorio Escuela Colombiana de Ingeniería Julio Garavitorepositorio.eci@escuelaing.edu.coU0kgVVNURUQgSEFDRSBQQVJURSBERUwgR1JVUE8gREUgUEFSRVMgRVZBTFVBRE9SRVMgREUgTEEgQ09MRUNDScOTTiAiUEVFUiBSRVZJRVciLCBPTUlUQSBFU1RBIExJQ0VOQ0lBLgoKQXV0b3Jpem8gYSBsYSBFc2N1ZWxhIENvbG9tYmlhbmEgZGUgSW5nZW5pZXLDrWEgSnVsaW8gR2FyYXZpdG8gcGFyYSBwdWJsaWNhciBlbCB0cmFiYWpvIGRlIGdyYWRvLCBhcnTDrWN1bG8sIHZpZGVvLCAKY29uZmVyZW5jaWEsIGxpYnJvLCBpbWFnZW4sIGZvdG9ncmFmw61hLCBhdWRpbywgcHJlc2VudGFjacOzbiB1IG90cm8gKGVuICAgIGFkZWxhbnRlIGRvY3VtZW50bykgcXVlIGVuIGxhIGZlY2hhIAplbnRyZWdvIGVuIGZvcm1hdG8gZGlnaXRhbCwgeSBsZSBwZXJtaXRvIGRlIGZvcm1hIGluZGVmaW5pZGEgcXVlIGxvIHB1YmxpcXVlIGVuIGVsIHJlcG9zaXRvcmlvIGluc3RpdHVjaW9uYWwsIAplbiBsb3MgdMOpcm1pbm9zIGVzdGFibGVjaWRvcyBlbiBsYSBMZXkgMjMgZGUgMTk4MiwgbGEgTGV5IDQ0IGRlIDE5OTMsIHkgZGVtw6FzIGxleWVzIHkganVyaXNwcnVkZW5jaWEgdmlnZW50ZQphbCByZXNwZWN0bywgcGFyYSBmaW5lcyBlZHVjYXRpdm9zIHkgbm8gbHVjcmF0aXZvcy4gRXN0YSBhdXRvcml6YWNpw7NuIGVzIHbDoWxpZGEgcGFyYSBsYXMgZmFjdWx0YWRlcyB5IGRlcmVjaG9zIGRlIAp1c28gc29icmUgbGEgb2JyYSBlbiBmb3JtYXRvIGRpZ2l0YWwsIGVsZWN0csOzbmljbywgdmlydHVhbDsgeSBwYXJhIHVzb3MgZW4gcmVkZXMsIGludGVybmV0LCBleHRyYW5ldCwgeSBjdWFscXVpZXIgCmZvcm1hdG8gbyBtZWRpbyBjb25vY2lkbyBvIHBvciBjb25vY2VyLgpFbiBtaSBjYWxpZGFkIGRlIGF1dG9yLCBleHByZXNvIHF1ZSBlbCBkb2N1bWVudG8gb2JqZXRvIGRlIGxhIHByZXNlbnRlIGF1dG9yaXphY2nDs24gZXMgb3JpZ2luYWwgeSBsbyBlbGFib3LDqSBzaW4gCnF1ZWJyYW50YXIgbmkgc3VwbGFudGFyIGxvcyBkZXJlY2hvcyBkZSBhdXRvciBkZSB0ZXJjZXJvcy4gUG9yIGxvIHRhbnRvLCBlcyBkZSBtaSBleGNsdXNpdmEgYXV0b3LDrWEgeSwgZW4gY29uc2VjdWVuY2lhLCAKdGVuZ28gbGEgdGl0dWxhcmlkYWQgc29icmUgw6lsLiBFbiBjYXNvIGRlIHF1ZWphIG8gYWNjacOzbiBwb3IgcGFydGUgZGUgdW4gdGVyY2VybyByZWZlcmVudGUgYSBsb3MgZGVyZWNob3MgZGUgYXV0b3Igc29icmUgCmVsIGRvY3VtZW50byBlbiBjdWVzdGnDs24sIGFzdW1pcsOpIGxhIHJlc3BvbnNhYmlsaWRhZCB0b3RhbCB5IHNhbGRyw6kgZW4gZGVmZW5zYSBkZSBsb3MgZGVyZWNob3MgYXF1w60gYXV0b3JpemFkb3MuIEVzdG8gCnNpZ25pZmljYSBxdWUsIHBhcmEgdG9kb3MgbG9zIGVmZWN0b3MsIGxhIEVzY3VlbGEgYWN0w7phIGNvbW8gdW4gdGVyY2VybyBkZSBidWVuYSBmZS4KVG9kYSBwZXJzb25hIHF1ZSBjb25zdWx0ZSBlbCBSZXBvc2l0b3JpbyBJbnN0aXR1Y2lvbmFsIGRlIGxhIEVzY3VlbGEsIGVsIENhdMOhbG9nbyBlbiBsw61uZWEgdSBvdHJvIG1lZGlvIGVsZWN0csOzbmljbywgCnBvZHLDoSBjb3BpYXIgYXBhcnRlcyBkZWwgdGV4dG8sIGNvbiBlbCBjb21wcm9taXNvIGRlIGNpdGFyIHNpZW1wcmUgbGEgZnVlbnRlLCBsYSBjdWFsIGluY2x1eWUgZWwgdMOtdHVsbyBkZWwgdHJhYmFqbyB5IGVsIAphdXRvci5Fc3RhIGF1dG9yaXphY2nDs24gbm8gaW1wbGljYSByZW51bmNpYSBhIGxhIGZhY3VsdGFkIHF1ZSB0ZW5nbyBkZSBwdWJsaWNhciB0b3RhbCBvIHBhcmNpYWxtZW50ZSBsYSBvYnJhIGVuIG90cm9zIAptZWRpb3MuRXN0YSBhdXRvcml6YWNpw7NuIGVzdMOhIHJlc3BhbGRhZGEgcG9yIGxhcyBmaXJtYXMgZGVsIChsb3MpIGF1dG9yKGVzKSBkZWwgZG9jdW1lbnRvLiAKU8OtIGF1dG9yaXpvIChhbWJvcykK

Publicaciones similares