Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Publicações

Publicações por Jorge Sousa Pinto

2007

A Higher-Order Calculus for Graph Transformation

Autores
Fernandez, M; Mackie, I; Pinto, JS;

Publicação
Electronic Notes in Theoretical Computer Science

Abstract
This paper presents a formalism for defining higher-order systems based on the notion of graph transformation (by rewriting or interaction). The syntax is inspired by the Combinatory Reduction Systems of Klop. The rewrite rules can be used to define first-order systems, such as graph or term-graph rewriting systems, Lafont's interaction nets, the interaction systems of Asperti and Laneve, the non-deterministic nets of Alexiev, or a process calculus. They can also be used to specify higher-order systems such as hierarchical graphs and proof nets of Linear Logic, or to specify the operational semantics of graph-based languages.

2012

Assertion-based slicing and slice graphs

Autores
Barros, JB; da Cruz, D; Henriques, PR; Pinto, JS;

Publicação
FORMAL ASPECTS OF COMPUTING

Abstract
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 postconditions can be combined in a new slicing algorithm that is more precise than the existing specification-based algorithms. The algorithm is based on (a) a precise test for removable statements, and (b) the construction of a slice graph, a program control flow graph extended with semantic labels and additional edges that "short-circuit" removable commands. 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). Iteration is handled through the use of loop invariants and variants to ensure termination. The paper also discusses in detail applications of these forms of slicing, including the elimination of (conditionally) unreachable and dead code, and compares them to other related notions.

2010

Assertion-based slicing and slice graphs

Autores
Barros, JB; Da Cruz, D; Henriques, PR; Pinto, JS;

Publicação
Proceedings - Software Engineering and Formal Methods, SEFM 2010

Abstract
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. © 2010 IEEE.

1996

Using Internet technology for course support

Autores
Miranda, JEP; Pinto, JS;

Publicação
SIGCSE Bulletin (Association for Computing Machinery, Special Interest Group on Computer Science Education)

Abstract
This paper has two purposes: first, to describe an experiment made in an undergraduate course, using Internet services to improve the speed and ease of communication between students and teaching team. We claim that the very positive results we obtained may very easily be reproduced in any course, with undergraduate students from the first year on. The second purpose is to discuss some possible directions the authors are planning to follow, in what concerns the utilization of Internet in education. Virtual environments such as MUDs and the automatic marking-up of problems submitted through WWW forms are steps towards what might end up as a full-blown Distance Education Environment.

2001

Parallel evaluation of Interaction Nets with MPINE

Autores
Pinto, JS;

Publicação
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Abstract
We describe the MPINE tool, a multi-threaded evaluator for Interaction Nets. The evaluator is an implementation of the present author's Abstract Machine for Interaction Nets [5] and uses POSIX threads to achieve concurrent execution. When running on a multi-processor machine (say an SMP architecture), parallel execution is achieved effortlessly, allowing for desktop parallelism on commonly available machines. © Springer-Verlag Berlin Heidelberg 2001.

2011

GammaPolarSlicer

Autores
Areias, S; da Cruz, D; Henriques, PR; Pinto, JS;

Publicação
COMPUTER SCIENCE AND INFORMATION SYSTEMS

Abstract
In software development, it is often desirable to reuse existing software components. This has been recognized since 1968, when Douglas Mcllroy of Bell Laboratories proposed basing the software industry on reuse. Despite the failures in practice, many efforts have been made to make this idea successful. In this context, we address the problem of reusing annotated components as a rigorous way of assuring the quality of the application under construction. We introduce the concept of caller-based slicing as a way to certify that the integration of an annotated component with a contract into a legacy system will preserve the behavior of the former. To complement the efforts done and the benefits of the slicing techniques, there is also a need to find an efficient way to visualize the annotated components and their slices. To take full profit of visualization, it is crucial to combine the visualization of the control/ data flow with the textual representation of source code. To attain this objective, we extend the notion of System Dependence Graph and slicing criterion.

  • 8
  • 12