[FMH11]
Ana María Fernández-Soriano, Julio Mariño, and Ángel Herranz. A tool for the integration of constraint logic programming in spreadsheets. In Purificación Arenas, Víctor M. Gulías, and Pablo Nogueira, editors, Actas XI Jornadas sobre Programación y Lenguajes, pages 243-252, A Coruña, Spain, September 2011. ISBN 978-84-9749-487-8. [ bib ]
[HM11a]
Ángel Herranz and Julio Mariño. Synthesis of logic programs from object-oriented formal specifications. In Technical Communications of the 27th International Conference on Logic Programming, volume 11 of LIPIcs, pages 95-105, Lexington, Kentucky, USA, July 2011. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN: 978-3-939897-31-6. [ bib ]
[HBMM11]
Ángel Herranz, Clara Benac, Guillem Marpons, and Julio Mariño. Mechanising the validation of ERTMS requirements and new procedures. In 9th World Congress on Railway Research, page 33, May 2011. [ bib | .pdf ]
[HM11b]
Ángel Herranz and Julio Mariño. A verified implementation of priority monitors in Java. In Bernhard Beckert, Ferruccio Damiani, and Dilian Gurov, editors, Papers presented at the 2nd. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS'11, number 26, pages 244-259, Turin, Italy, 2011. Karlsruhe Reports in Informatics. ISSN 2190-4782. [ bib ]
[Her11]
Ángel Herranz. An Object-Oriented Formal Notation: Executable Specifications in Clay. PhD thesis, Universidad Politécnica de Madrid, January 2011. [ bib ]
[HM10]
Ángel Herranz and Julio Mariño. Executable specifications in an object oriented formal notation. In 20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010, pages 144-158, Hagenberg, Austria, July 2010. Research Institute for Symbolic Computation (RISC) of the Johannes Kepler University Linz. [ bib | .pdf ]
Early validation of requirements is crucial for the rigorous development of software. Without it, even the most formal of the methodologies will produce the wrong outcome. One successful approach, popularised by some of the so-called lightweight formal methods, consists in generating (finite, small) models of the specifications. Another possibility is to build a running prototype from those specifications. In this paper we show how to obtain executable prototypes from formal specifications written in an object oriented notation by translating them into logic programs. This has a number of advantages over other lightweight methodologies. For instance, we recover the possibility of dealing with recursive data types as specifications that use them often lack finite models.

[HP10a]
Ángel Herranz and Iván Pérez. Communication models for resource mashups. Technical Report UPM-BABEL-2010-002, Babel Group, Universidad Politécnica de Madrid, March 2010. [ bib ]
[HP10b]
Ángel Herranz and Iván Pérez. Compatible communication in mashups. Technical Report UPM-BABEL-2010-001, Babel Group, Universidad Politécnica de Madrid, January 2010. [ bib ]
[MMC+09]
Guillem Marpons, Julio Mariño, Manuel Carro, Ángel Herranz, Lars-Åke Fredlund, Juan José Moreno-Navarro, and Álvaro Polo. A coding rule conformance checker integrated into GCC. ENTCS, 248:149-159, August 5 2009. [ bib | http ]
Coding rules are often used in industry to foster best practices when coding software and to avoid the many hazardous constructions present in languages such as C or C++. Predictable, reliable tools are needed to automatically measure adherence to these practices, as manually checking for compliance is cumbersome. Moreover, due to the wide range of possible coding rule sets, easy of customization is a need in order for these tools to be of practical use. With this aim in mind, we present an extension of the GNU Compiler Collection (GCC) that flags those code fragments that do not conform to coding rules belonging to a given set. These sets of coding rules can be defined using a high-level declarative language based on logic programming, thereby making it possible to easily check code for conformance with respect to rules addressing the particular needs of a project, company, or application area.

[THM09]
Toufik Taibi, Ángel Herranz, and Juan José Moreno-Navarro. Stepwise refinement validation of design patterns formalized in tla+ using the tlc model checker. Journal of Object Technology (JOT, http://www.jot.fm/general/about/), 8(2):137-161, March 2009. [ bib | DOI | .pdf ]
Despite being around for only a little more than a decade, design patterns have proved to be successful reuse artifacts. However, the fact that they are mostly described informally gives rise to ambiguity and hinders correct usage. This paper discusses how to formally specify the "solution element" of patterns using TLA+, the formal specification language of Temporal Logic of Actions (TLA). The focus is first on formally specifying the most abstract version of a pattern before validly doing stepwise refinements by adding more details along the way until reaching a concrete implementation. Checking that the refinement properties hold was done using TLC (the TLA+ model checker).

[HMCM09]
Ángel Herranz, Julio Mariño, Manuel Carro, and Juan José Moreno-Navarro. Modeling concurrent systems with shared resources. In Formal Methods for Industrial Critical Systems, 14th International Workshop, FMICS 2009, Eindhoven, The Netherlands, November 2-3, 2009. Proceedings, volume 5825 of Lecture Notes in Computer Science, pages 102-116, 2009. [ bib | http | .pdf ]
Testing is the more widely used approach to (partial) system validation in industry. The introduction of concurrency makes exhaustive testing extremely costly or just impossible, requiring shifting to formal verification techniques. We propose a methodology to design and verify a concurrent system that splits the verification problem in two independent tasks: internal verification of shared resources, where some concurrency aspects like mutual exclusion and conditional synchronisation are isolated, and external verification of processes, where synchronisation mechanisms are not relevant. Our method is language independent, non-intrusive for the development process, and improves the portability of the resulting system. We demonstrate it by actually checking several properties of an example application using the TLC model checker.

[MMC+08b]
Guillem Marpons, Julio Mariño, Manuel Carro, Ángel Herranz, Lars-Åke Fredlund, Juan José Moreno-Navarro, and Álvaro Polo. A coding rule conformance checker integrated into GCC. In Jesús M. Almendros Jiménez and María José Suárez-Cabal, editors, VIII Jornadas sobre Programación y Lenguajes, PROLE 2008, pages 245-249, Gijón, Spain, October 7-10 2008. [ bib | .pdf ]
Coding rules are often used in industry for codifying software best practices and avoiding the many hazardous constructions present in languages such as C or C++. Predictable and customisable tools are needed to automatically measure adherence to these practices. Many of the properties about software needed for rule conformance analysis are calculated by modern compilers. We present an extension of the GNU Compiler Collection (GCC) that flags those code fragments that do not conform to a given set of rules. The user can define coding rules using a high-level declarative language based on logic programming.

[PHMM08]
Iván Pérez, Ángel Herranz, Susana Muñoz, and Juan José Moreno-Navarro. Modelling mash-up resources. In 13th Conference on Software Engineering and Databases, JISBD'08, pages 135-146, Gijón, Spain, October 7-10 2008. [ bib | .pdf ]
[MMC+08a]
Guillem Marpons, Julio Mariño-Carballo, Manuel Carro, Ángel Herranz, Juan José Moreno-Navarro, and Lars-Åke Fredlund. Automatic coding rule conformance checking using logic programming. In Paul Hudak and David Scott Warren, editors, Practical Aspects of Declarative Languages, 10th International Symposium, PADL 2008, volume 4902 of Lecture Notes in Computer Science, pages 18-34, San Francisco CA, USA, January 7-8 2008. Springer. [ bib | http ]
An extended practice in the realm of Software Engineering and programming in industry is the application of coding rules. Coding rules are customarily used to constrain the use (or abuse) of certain programming language constructions. However, these rules are usually written using natural language, which is intrinsically ambiguous and which may complicate their use and hinder their automatic enforcement. This paper presents some early work aiming at defining a framework to formalise and check for coding rule conformance using logic programming. We show how a certain class of rules - structural rules - can be reformulated as logic programs, which provides both a framework for formal specification and also for automatic conformance checking using a Prolog engine. Some examples of rules belonging to actual, third-party coding rule sets are discussed, along with the corresponding Prolog code. Experimental data regarding the practicality and impact of their application to real-life software projects is presented and discussed.

[MHF+07]
Julio Mariño, Ángel Herranz, Lars-Åke Fredlund, Manuel Carro, Víctor Pablos-Ceruelo, Guillem Marpons, and Juan José Moreno-Navarro. Study of existing coding rule formalisms and compendium of common hazards. Use of coding rules in software industry. Technical report, Facultad de Informática, Universidad Politécnica de Madrid, Boadilla del Monte, Madrid, Spain, November 2007. [ bib ]
[MMH+07b]
Guillem Marpons, Julio Mariño, Ángel Herranz, Lars-Åke Fredlund, Manuel Carro, and Juan José Moreno-Navarro. Automatic coding rule conformance checking using logic programs. CoRR, abs/0711.0344, November 2007. [ bib | http ]
Coding rules are customarily used to constrain the use (or abuse) of certain constructions in a programming language. Standard coding rule sets exist that target different languages and application domains. However, these rules are usually written using a natural language, which is intrinsically ambiguous, and which may hinder their automatic application. This short paper presents some early work aiming at defining a framework to formalise and check for coding rule conformance using logic programming. We show how a certain class of rules - structural rules - can be reformulated as logic programs. Some real examples, including Prolog code formalising them, are shown and discussed.

[MMH+07a]
Guillem Marpons, Julio Mariño, Ángel Herranz, Lars-Åke Fredlund, Manuel Carro, and Juan José Moreno-Navarro. Automatic coding rule conformance checking using logic programs. In Patricia Hill and Vim Vanhoof, editors, 17th Workshop on Logic-based methods in Programming Environments, WLPE 2007, page 47, Porto, Portugal, September 2007. [ bib | http ]
Coding rules are customarily used to constrain the use (or abuse) of certain constructions in a programming language. Standard coding rule sets exist that target different languages and application domains. However, these rules are usually written using a natural language, which is intrinsically ambiguous, and which may hinder their automatic application. This short paper presents some early work aiming at defining a framework to formalise and check for coding rule conformance using logic programming. We show how a certain class of rules - structural rules - can be reformulated as logic programs. Some real examples, including Prolog code formalising them, are shown and discussed.

[MMH+07c]
Guillem Marpons, Julio Mariño, Ángel Herranz, Lars-Åke Fredlund, Manuel Carro, and Juan José Moreno-Navarro. Towards checking coding rule conformance using logic programming, August 2007. Poster at the 14th International Static Analysis Symposium, SAS 2007. [ bib | .pdf ]
This short paper presents some early work in the context of an European project aiming at defining a framework to formalise and check for coding rule conformance using logic programming. We show how a certain class of rules - structural rules - can be reformulated as logic programs. This provides both a framework for formal specification and also for automatic conformance checking using a Prolog engine.

[HM07]
Ángel Herranz and Juan José Moreno-Navarro. Design Pattern Formalization Techniques, chapter Modeling and Reasoning about Design Patterns in SLAM-SL. IGI Publishing, March 2007. Other ISBN: 978-1-59904-221-3. [ bib | .pdf ]
The main main subject of the chapter is how design patterns can be described as class operations. Additionally, we describe two possible applications: how to reason about design patterns, and how a design can be automatically refactored using design patterns.

[MHM07]
Julio Mariño, Ángel Herranz, and Juan José Moreno-Navarro. Demandedness analysis with partial predicates. Theory and Practice of Logic Programming, 7(1-2):153-182, January 2007. [ bib ]
[HN05]
Ángel Herranz and Pablo Nogueira. More than parsing. In Francisco Javier López Fraguas, editor, Spanish Conference on Programming and Languages (CEDI-PROLE'05), pages 193-202. Thomson Paraninfo, September 2005. [ bib | .pdf ]
We introduce Generalised Object Normal Form (GONF), a syntax formalism that enables language designers to define concrete syntax in a form that also naturally defines the data structure of the abstract syntax tree. More precisely, GONF's grammatical productions specify simultaneously and without annotations (1) concrete syntax (a language and its parser) and (2) the collection of language-independent data type definitions representing the abstract syntax tree accurately and concisely. These types can be materialised in languages supporting inheritance or algebraic types, and preferably parametric polymorphism. We also describe MTP, an available GONF-based tool.

[CMHM04]
Manuel Carro, Julio Mariño, Ángel Herranz, and Juan José Moreno-Navarro. Teaching how to derive correct concurrent programs from state-based specifications. Full paper, September 2004. [ bib | .ps.gz ]
The fun of teaching and learning concurrent programming is sometimes darkened by the difficulty in getting concurrent programs to work right. In line with other programming subjects in our department, we advocate the use of formal specifications to state clearly how a concurrent program must behave, to reason about this behavior, and to be able to produce code from specifications in a semi-automatic fashion. We argue that a mild form of specification not only makes it possible to get programs running easier, but it also introduces students to a quite systematic way of approaching programming: reading and understanding specifications is seen as an unavoidable step in the programming process, as they are really the only place where the expected conduct of the system is completely described. By using formal techniques in these cases, where it is undoubtedly appropriate, we introduce formality without the need to resort to justifications with artificial or overly complicated examples.

[AHM04]
Ángel Herranz and Julio Mariño. Por otra ruta, por favor. Novática, 1(170):73-75, August 2004. Contribución a la columna "Programar es Crear". [ bib ]
[HM04]
Ángel Herranz and Julio Mariño. Por otra ruta, por favor (cupcam 2003, problema e, solución). Novatica, 1(170):73, July 2004. Sección “Programar es crear”. [ bib | .pdf ]
[LH04]
José A. Leiva and Ángel Herranz. Un refactorizador simple (cupcam 2003, problema d, solución). Novatica, 1(169):74, May 2004. Sección “Programar es crear”. [ bib | .pdf ]
[CMAHM04]
Manuel Carro, Julio Mariño, Ángel Herranz, and Juan José Moreno-Navarro. Teaching how to derive correct concurrent programs (from state-based specifications and code patterns). In C.N. Dean and R.T. Boute, editors, Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, volume 3294 of LNCS, pages 85-106. Springer, 2004. ISBN 3-540-23611-2. [ bib ]
[HM03a]
Ángel Herranz and Juan José Moreno-Navarro. Formal agility. how much of each? In Taller de Metodologías Ágiles en el Desarrollo del Software. VIII Jornadas de Ingeniería del Software y Bases de Datos, JISBD 2003, pages 47-51, Alicante, España, November 2003. Grupo ISSI. [ bib | .ps.gz ]
Agile Processes and Formal Methods (FM), water and oil, impossible mixture? Yes at first sight. Nevertheless, being formal methods weight processes and being agile processes informal approaches to software development, it is worth to study how much formal can be an agile process like Extreme Programming (XP) and how much agile can be a formal method. On our view, some XP practices are suitable for a formal approach.

[HMM03]
Ángel Herranz, Noelia Maya, and Juan José Moreno-Navarro. From executable specifications to java. In Juan José Moreno-Navarro and Manuel Palomar, editors, III Jornadas sobre Programación y Lenguajes, PROLE 2003, pages 33-44, Alicante, España, November 2003. Departamento de Lenguajes y Sistemas Informáticos, Universidad de Alicante. Depósito Legal MU-2299-2003. [ bib | .ps.gz ]
In this paper the authors study a pair of constructs in a formal specification language that can be directly translated into readable and relatively efficient code. Those constructs are algebraic types and (an extended concept of logical) quantification. The translation is guided by object oriented design patterns that makes the synthesised code easily understandable by ordinary developers. Efficiency can be achieved thanks to the effort of the user during the specification refinement process, specification transformations and implementation issues of the the design patterns.

[HM03c]
Ángel Herranz and Juan José Moreno-Navarro. Rapid prototyping and incremental evolution using SLAM. In 14th IEEE International Workshop on Rapid System Prototyping, RSP 2003), San Diego, California, USA, June 2003. [ bib | .ps.gz ]
The paper shows the outlines of the SLAM system, that allows for an effective use of Formal Methods (FM) in Rapid Application Development (RAD) and other prototyping processes. The SLAM system, includes an expressive object oriented specification language and a development environment that, among other features, is able to generate efficient and readable code in a high level object oriented language (Java, C++, ...). SLAM is able to generate prototypes that can be used to validate the requirements with the user. The additional advantage is that the prototype is not throw-away because most part of the generated code can be directly used and the other part can be optimised with the additional help of assertions automatically included.

[HM03b]
Ángel Herranz and Juan José Moreno-Navarro. Formal extreme (and extremely formal) programming. In Michele Marchesi and Giancarlo Succi, editors, 4th International Conference on Extreme Programming and Agile Processes in Software Engineering, XP 2003, number 2675 in LNCS, pages 88-96, Genova, Italy, May 2003. [ bib | .pdf ]
This paper is an exploratory work were the authors study how the technology of Formal Methods (FM) can interact with agile process in general and with Extreme Programming (XP) in particular. Our thesis is that most of XP practices (pair programming, daily build, the simplest design or the metaphor) are technology independent and therefore can be used in FM based developments. Additionally, other essential pieces like test first, incremental development and refactoring can be improved by using FM. In the paper we explore in a certain detail those pieces: when you write a formal specification you are saying what your code must do, when you write a test you are doing the same so the idea is to use formal specifications as tests. Incremental development is quite similar to the refinement process in FM: specifications evolve to code maintaining previous functionality. Finally FM can help to remove redundancy, eliminate unused functionality and transform obsolete designs into new ones, and this is refactoring.

[AHCMS03]
Ángel Herranz, Manuel Carro, Julio Mariño, and Pablo Sánchez Torralba. Almejas gigantes e interfaces de usuario. Novática, 1(161):70-73, February 2003. Contribución a la columna "Programar es Crear". [ bib ]
[HMCS03]
Ángel Herranz, Julio Mariño, Manuel Carro, and Pablo Sanchez. Almejas gigantes e interfaces de usuario (solución del programa e). Novatica, 1(161):70, January 2003. Sección “Programar es crear”. [ bib | .pdf ]
[HMM02a]
Ángel Herranz, Juan José Moreno-Navarro, and Noelia Maya. Declarative reflection and its application as a pattern language. In Marco Comini and Moreno Falaschi, editors, Electronic Notes in Theoretical Computer Science, volume 76. Elsevier Science Publishers, November 2002. [ bib | .pdf | .ps.gz ]
The paper presents the reflection facilities of the specification language Slam-sl. Slam-sl is an object oriented specification language where class methods are specified by pre and postconditions. The reflection capabilities allow managing these pre and postconditions in specifications what means that semantic reflection is possible. The range of interesting applications is very wide: formal specification of interfaces and abstract classes, specification of component based software, formalization of design pattern, using Slam-sl as a pattern language, etc. The paper discusses the last two advantages in some detail.

[AHCMS02]
Ángel Herranz, Manuel Carro, Julio Mariño, and Pablo Sánchez Torralba. No taléis el bosque por culpa de los árboles. Novática, 1(159):74-77, October 2002. Contribución a la columna "Programar es Crear". [ bib ]
[HMCS02]
Ángel Herranz, Julio Mariño, Manuel Carro, and Pablo Sanchez. No taléis el bosque por culpa de los árboles: solución. Novatica, 1(159):74, September 2002. Sección “Programar es crear”. [ bib | .pdf ]
[HMM02b]
Ángel Herranz, Juan José Moreno-Navarro, and Noelia Maya. Declarative reflection and its application as a pattern language. In Marco Comini and Moreno Falaschi, editors, 11th. International Workshop on Functional and Logic Programming (WFLP'02), Grado, Italy, June 2002. University of Udine. [ bib | .ps.gz ]
The paper presents the reflection facilities of the specification language Slam-sl. Slam-sl is an object oriented specification language where class methods are specified by pre and postconditions. The reflection capabilities allow managing these pre and postconditions in specifications what means that semantic reflection is possible. The range of interesting applications is very wide: formal specification of interfaces and abstract classes, specification of component based software, formalization of design pattern, using Slam-sl as a pattern language, etc. The paper discusses the last two advantages in some detail.

[HM02b]
Ángel Herranz and Juan José Moreno-Navarro. Specifying in the large: Object-oriented specifications in the software development process. In B. J. Krämer H. Ehrig and A. Ertas, editors, The Sixth Biennial World Conference on Integrated Design and Process Technology (IDPT'02), volume 1, Pasadena, California, June 2002. Society for Design and Process Science. ISSN 1090-9389. [ bib | .ps.gz ]
The paper discusses how formal methods, and, in particular, object oriented specification languages can be integrated in the software development process in an effective way. We depart from an object specification language in the SLAM system that combines characteristics of algebraic languages as well as pre and postconditions for class methods specification. We study how to specify classes as well as the formal relations that class relationships must hold (in particular, inheritance). One of the main features of the specification language is that it is supported by an integrated environment that, among other facilities, includes the generation of readable and (enough) efficient imperative code. We also address how this translation can be done and the extra capabilities of the environment regarding the use of formal method in the development process, for instance program validation.

[GHM02]
Carlos Gregorio, Ángel Herranz, and Raquel Martinez. Computing curricula 2001. Novática, 1(157):47-54, May 2002. In Spanish. [ bib | .ps.gz | .pdf ]
En diciembre de 2001 se publicó el informe final del volumen Computer Science del Computing Curricula 2001. Las recomendaciones desarrolladas por ACM y IEEE de forma individual, tanto como las recomendaciones elaboradas de forma conjunta, han sido y siguen siendo un punto de referencia para todos los que nos dedicamos a la enseñanza universitaria de la informática. El objetivo de este artículo es dar a conocer las líneas maestras del informe, los principios del mismo, las nuevas áreas de conocimientos y las diferentes estrategias de implementación sugeridas, el objetivo final es que un lector interesado pueda hacerse una idea clara de las propuestas fundamentales del informe.

[CHMS02]
Manuel Carro, Ángel Herranz, Julio Mariño, and Pablo Sánchez. Configuración de un aeropuerto: solución. Novatica, 1(156):72, March 2002. Sección “Programar es crear”. [ bib | .pdf ]
[HM02a]
Ángel Herranz and Juan José Moreno-Navarro. On the design of an object-oriented formal notation. In Fourth Workshop on Rigorous Object Oriented Methods, ROOM 4. King's College, London, March 2002. [ bib | .ps.gz ]
We consider that the application of formal methods in the software development process is essential to obtain high integrity products. Despite the fact that arguments for using formal methods, in practice it is clear that its use is not widespread. Slam is a software construction system based on formal specifications. In this paper some features of the formal specification language embedded in the Slam system are presented: algebraic types, safe inheritance, generic polymorphism and collection traversals. These features have in common that that they rely on static information, they are well known techniques, they are practical and relatively popular and not all of them are usual in formal notations.

[HM01b]
Ángel Herranz and Juan José Moreno-Navarro. Design patterns as class operators. Workshop on High Integrity Software Development at V Spanish Conference on Software Engineering, JISBD'01, November 2001. [ bib | .ps.gz ]
The paper presents a formalization of (some) design patterns as operators between classes. A concrete design pattern is understood as an operator that modifies certain classes into the design proposed by the pattern. In such this way, we present a way to understand design patterns in a formal context, what aims for formal reasoning about them. Furthermore, the view of design patterns as class operators proposes a method to incorporate design patterns into object oriented development tools. It also can give some hints to easily compose patterns , and to identify design patterns in a given specification.

[HM01a]
Ángel Herranz and Juan José Moreno-Navarro. Declarative reflection and its application as a pattern language. In Fernando Orejas, Fernando Cuartero, and Diego Cazorla, editors, I Jornadas sobre Programación y Lenguajes, PROLE 2001, pages 179-197, Almagro, Spain, November 2001. [ bib | .ps.gz ]
The paper presents the reflection facilities of the specification language Slam-sl. Slam-sl is an object oriented specification language where class methods are specified by pre and postconditions. The reflection capabilities permit managing these pre and postconditions in specifications what means that semantic reflection is possible. The range of interesting applications is very wide: formal specification of interfaces and abstract classes, specification of component based software, formalization of design pattern, using Slam-sl as a pattern language, etc. The paper discusses the last two advantages in some detail.

[MH01]
Juan José Moreno-Navarro and Ángel Herranz. Declarative reflection and its application as a pattern language. Invited Session on “Formalization of Object-Oriented Methods, Patterns, and Frameworks”, The Fifth Multi-Conference on Systemics, Cybernetics and Informatics (SCI'2001), July 2001. [ bib | .ps.gz ]
The paper presents the reflection facilities of the specification language Slam-sl. Slam-sl is an object oriented specification language where class methods are specified by pre and postconditions. The reflection capabilities permit managing these pre and postconditions in specifications what means that semantic reflection is possible. The range of interesting applications is very wide: formal specification of interfaces and abstract classes, specification of component based software, formalization of design pattern, using Slam-sl as a pattern language, etc. The paper discusses the last two advantages in some detail.

[HM01c]
Ángel Herranz and Juan José Moreno-Navarro. Slam-sl Tutorial. Grupo Babel, Facultad de Informática, Universidad Politécnica de Madrid, Campus de Montegancedo s/n, 28660, Boadilla del Monte, Madrid, Spain, 2001. Draft based on Ángel Herranz's PhD. Thesis. [ bib | .ps.gz ]
This paper shows the debugging facilities provided by the Slam system. The Slam system includes i) a specification language that integrates algebraic specifications and model-based specifications using the object oriented model. Class operations are defined by using rules each of them with logical pre and postconditions but with a functional flavour. ii) A development environment that, among other features, is able to generate readable code in a high level object oriented language. iii) The generated code includes (part of) the pre and postconditions as assertions, that can be automatically checked in the debug mode execution of programs. We focus on this last aspect. The Slam language is expressive enough to describe many useful properties and these properties are translated into a Prolog program that is linked (via an adequate interface) with the user program. The debugging execution of the program interacts with the Prolog engine which is responsible for checking properties.

[HM00c]
Ángel Herranz and Juan José Moreno-Navarro. Towards automating the iterative rapid prototyping process with the SLAM system. In V Spanish Conference on Software Engineering, pages 217-228, November 2000. [ bib | .ps.gz ]
This paper shows the outlines of the Slam project, designed for automating the Iterative Rapid Prototyping Process. The Slam project system includes a very expressive object oriented specification language that integrates algebraic specifications and model-based specifications. Class operations are defined by using rules each of them with logical pre- and post-conditions but with a functional flavour. The main novel feature of the system is that contains a development environment that, among other features, is able to generate (reasonable) efficient and readable code in another high level object oriented language (C++, Java, etc.). The generated code includes (part of) the pre- and post-conditions as assertions, that can be automatically checked in the debug mode execution of programs. Slam can be used to generate prototypes that can be used to validate the requirements with the user. The additional advantage is that the prototype is not throw-away because most part of the generated code can be used at it is and the other part can be optimized with the additional help of the declarative debugging of the modified code.

[HMM00]
Ángel Herranz, Juan José Moreno-Navarro, and Julio Mariño. Demand analysis with partial predicates. In 9th International Workshop on Functional and Logic Programming (WFLP 2000), Benicassim, Spain, September 2000. Universidad Politécnica de Valencia. [ bib ]
[HM00b]
Ángel Herranz and Juan José Moreno-Navarro. On the role of functional-logic languages for the debugging of imperative programs. In 9th International Workshop on Functional and Logic Programming (WFLP 2000), Benicassim, Spain, September 2000. Universidad Politécnica de Valencia. [ bib | .ps.gz ]
The paper presents some aspects of the debugging subsystem of the ongoing project Slam where the language Curry plays a significant role. The Slam project is an attempt to amalgamate most of the best facilities of declarative languages to the development of imperative programs. The Slam system is composed by i) an object oriented specification language. (Functional style) Rules are used to define class operations each of them with logical pre and post-conditions. ii) A development environment that, among other features, is able to generate readable code in a high level object oriented (imperative) language. iii) The generated code includes (part of) the pre and post-conditions as assertions, that can be automatically checked in the debug mode execution of programs. We concentrate on the latter aspect. Many useful properties can be expressed in the Slam language and these properties are translated into a Curry program that is linked (via an adequate interface) with the generated program. The Curry execution is responsible for checking properties, interacting with the debugging execution of the program.

[HM00a]
Ángel Herranz and Juan José Moreno-Navarro. Generation of and debugging with logical pre and post conditions. In M. Ducasse, editor, Automated and Algorithmic Debugging 2000. TU Munich, August 2000. [ bib | .ps.gz ]
This paper shows the debugging facilities provided by the SLAM system. The SLAM system includes i) a specification language that integrates algebraic specifications and model-based specifications using the object oriented model. Class operations are defined by using rules each of them with logical pre and postconditions but with a functional flavour. ii) A development environment that, among other features, is able to generate readable code in a high level object oriented language. iii) The generated code includes (part of) the pre and postconditions as assertions, that can be automatically checked in the debug mode execution of programs. We focus on this last aspect. The SLAM language is expressive enough to describe many useful properties and these properties are translated into a Prolog program that is linked (via an adequate interface) with the user program. The debugging execution of the program interacts with the Prolog engine which is responsible for checking properties.

[MMM+96]
J.J. Moreno-Navarro, J. Mariño, J. García Martín, Ángel Herranz, and A. del Pozo. Adding type-classes to functional-logic languages. In M. Martelli and M. Navarro, editors, APPIA-GULP-PRODE'96, pages 427-438. Universidad del País Vasco, Summer Courses, Basque Country University, 1996. [ bib ]
[Her93]
Ángel Herranz. Interpretación abstracta de lenguajes lógico funcionales. Master's thesis, Facultad de Informática, Universidad Politécnica de Madrid, Campus de Montegancedo s/n, 28660, Boadilla del Monte, Madrid, Spain, October 1993. In Spanish. [ bib | .ps.gz ]
The aim of this work is to formulate a framework for the abstract interpretation of functional logic languages based on its operational semantics that allows for the most usual analyses needed in declarative programming: mode inference, optimal garbage collection, detection of parallel computations etc. Besides, it should allow for analyses of particular features of a lazy language.

[MHM93]
Julio Mariño, Ángel Herranz, and Juan José Moreno-Navarro. Demandedness analysis with dependence information for lazy narrowing. In W. Winsborough and S. Michaylov, editors, Workshop on Global Compilation, International Logic Programming Symposium October 26-30, 1993, Vancouver, BC, Canada, pages 99-114. Association for Logic Programming and Simon Fraser University, October 1993. Penn State University Technical Report. [ bib ]
[MH93]
Julio Mariño and Ángel Herranz. Specialized compilation of lazy functional logic programs. In Segundo Congreso Nacional de Programación Declarativa - 2nd Spanish Conference on Declarative Programming (ProDe'93), pages 39-55. Instituto de Investigación en Inteligencia Artificial, CSIC, 1993. [ bib ]

This file was generated by bibtex2html 1.94.