Publications

Pinto JS, Henriques PR, Cruz D, Barros J B.  2010.  Assertion-based slicing and slice graphs. 8th IEEE International Conference on Software Engineering and Formal Methods - SEFM. Abstractsefm2010specslicing-camera-ready.pdf

This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of post conditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a slice graph, a program control flow graph extended with semantic labels. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). The paper also reviews in detail, through examples, the ideas behind the use of preconditions and post conditions for slicing programs.

Cunha A, Barros J B, Saraiva JA.  2002.  Deriving Animations from Recursive Definitions. Draft Proceedings of the 14th International Workshop on the Implementation of Functional Languages - IFL. Abstractifl02.pdf

This paper describes a generic method to derive an animation from a recursive de nition, with the objective of debugging and understanding this de nition by expliciting its control structure. This method is based on a well known algorithm of factorizing a recursive function into the composition of the producer and the consumer of its call tree. We developed a systematic method to transform both the resulting functions in order to draw the tree step by step. The theory of data types as xed points of functors, generic recursion patterns, and monads, are fundamental to our work and are brie y presented. Using polytypic implementations of monadic recursion patterns and an application to manipulate and generate graph layouts we developed a prototype that, given a recursive function written in a subset of Haskell, returns a function whose execution yields the desired animation.

Barbosa LS, Barros J B, Almeida J J.  2000.  Polytipic recursion patterns. 5º Simpósio Brasileiro de Linguagens de Programação - SBLP. Abstractbarsblp.pdf

Recursive schemes over inductive data structures have been recognized as category-theoretic universals, yielding a handful of equational laws for program construction and transformation. This paper introduces the implementation of such recursion patterns as type parametric, or polytypic, functionals in the CAMILA prototyping language. Several examples are discussed.

Barros J B, Cruz D, Henriques PR, Pinto JS.  2012.  Assertion-based slicing and slice graphs. Formal Aspects of Computing. 24:217–248. Abstractsefm2010specslicing-camera-ready.pdf

This paper revisits the idea of slicing programs based on their axiomatic semantics, rather than using criteria based on control/data dependencies. We show how the forward propagation of preconditions and the backward propagation of post conditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (i) a precise test for removable statements, and (ii) the construction of a slice graph, a program control flow graph extended with semantic labels. It improves on previous approaches in two aspects: it does not fail to identify removable commands; and it produces the smallest possible slice that can be obtained (in a sense that will be made precise). The paper also reviews in detail, through examples, the ideas behind the use of preconditions and post conditions for slicing programs.

Cunha A, Barros J B.  2003.  Towards Utility-based Programming. Abstractuspl.pdf

Many programs have an objective that can be precisely stated as the maximization of a function defined over its local variables. This is the case of utility-based software agents, which are reactive entities that try to maximize their welfare, usually accessed by an utility function. This paper introduces a programming language suitable for explicit programming with utility functions. Starting from a standard concurrent programming language, we added primitives to allow the parametrization of each process with an utility function that should be maximized. For the moment, using techniques of Markov decision problems, we can compile sequential programs, written in a restricted version of this new language, into equally behaved programs written in the original one. Major problems in developing such utility-based programming language are the need to compare the utility of infinite executions or the need to deal with uncertainty.

Barros J B, Goguen J.  1995.  Semantics of Non-terminating Rewrite Systems using Minimal Coverings. Abstractprg118.pdf

We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of this minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non-termination systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness for confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders and then instantiate these to term rewriting systems.