PURe

Program Understanding and Re-engineering: Calculi and Applications

Navigation

Related

News

Sep 18 Paper Towards a Coordination Model for Interactive Systems by MarcoAntonioBarbosa, JoseCampos and LuisSoaresBarbosa has been accepted for FMIS'06 (Macau).

July 3 Paper Configurations of Web Services by MarcoAntonioBarbosa and LuisSoaresBarbosa has been accepted for FOCLASA'06 (Bonn, Germany).

July 3 Paper Strong Types for Relational Databases by Alexandra Silva and JoostVisser has been accepted for the Haskell Workshop 2006 (Portland, USA).

June 16 Paper Strongly Typed Rewriting For Coupled Software Transformation (by AlcinoCunha and JoostVisser) accepted by RULE 2006 (Seattle, USA).

May, 26 Paper Transposing Partial Coalgebras (by LuisSoaresBarbosa and JoseNunoOliveira) accepted for publication in TCS, Elsevier.

May, 11 Papers Type-safe two-level data transformation (by AlcinoCunha, JoseNunoOliveira and JoostVisser) and Pointfree factorization of operation refinement (by JoseNunoOliveira and Cesar Rodrigues) have been accepted by FM'06 (Canada).

May, 8 A paper entitled An Orchestrator for Dynamic Interconnection of Software Components, by MarcoAntonioBarbosa and LuisSoaresBarbosa, accepted at MTCoord'06 (Bologna).

More...

As of September 2006, PUReCafe has been continued with a wider scope as the Theory and Formal Methods Seminar.

PUReCafe was a weekly scientific colloquium organized by the LMF group.

Moderator: Joost Visser

Attendance open to all.

Upcoming talks

As of September 2006, PUReCafe has been continued with a wider scope as the Theory and Formal Methods Seminar.

Past talks

(reverse chronological)

Thu, 20 July, 2006 at 10:00
Combining Formal Methods and Functional Strategies Regarding the Reverse Engineering of Interactive Applications
João Carlos Silva
Graphical user interfaces (GUIs) make software easy to use by providing the user with visual controls. Therefore, correctness of GUI's code is essential to the correct execution of the overall software. Models can help in the evaluation of interactive applications by allowing designers to concentrate on its more important aspects. This paper describes our approach to reverse engineer an abstract model of a user interface directly from the GUI's legacy code. We also present results from a case study. These results are encouraging and give evidence that the goal of reverse engineering user interfaces can be met with more work on this technique.

Thu, 1 June, 2006 at 10:00
The Quality Economics of Defect-Detection Techniques
Stefan Wagner, Software & Systems Engineering, Technische Universitaet Muenchen, Institut fuer Informatik
Analytical software quality assurance (SQA) constitutes a significant part of the total development costs of a typical software system. Typical estimates say that up to 50\% of the costs can be attributed to defect detection and removal. Hence, this is a promising area for cost-optimisations. The main question in that context is then how to use those different techniques in a cost-optimal way. In detail this boils down to the questions to use (1) which techniques, (2) in which order, and (3) with what effort. This talk describes an analytical and stochastic model of the economics of analytical SQA that can be used to analyse and answer these questions. The practical application is shown on the example of a case study on model-based testing in the automotive domain.

Thu, 4 May, 2006 at 11:00
Discussion: Beyond PURe
Research.PURe team
The end of the Research.PURe project is approaching. We will be able to look back at a successful project with lots of interesting deliverables. But now it becomes urgent to reflect on what comes after Research.PURe. A deadline for new FCT proposals is July 31. We will initiate discussion about concrete ideas for such a follow-up project.

Thu, 23 March, 2006 at 10:00
Student presentations of course work
(1) Prototype Implementation of an Algebra of Components in Haskell
Jácome Cunha
The starting point to this project are state-based systems modeled as components, i.e, "black boxes" that have "buttons" or "ports" to communicate with the whole system. A list of operators to connect these components is given. A possible way to implement components as coalgebras in Haskell is shown. Finally, a tool to generate a component from a state-based system definition is implemented.
Thu, 23 March, 2006 at 10:30
(2) Camila Revival: VDM++ meets Haskell
Alexandra Silva
This communication is a follow up of [1]. We show how to model some of the key concepts of VDM++ in Haskell. Classes, objects, operations and inheritance are encoded based on the recently developed OOHaskell library.

[1] Camila Revival: VDM meets Haskell, Joost Visser, J.N. Oliveira, L.S. Barbosa, J.F. Ferreira, and A. Mendes. Overture Workshop, colocated with Formal Methods 2005.

Thu, 16 March, 2006 at 10:00
A calculational account of lambda-coinduction
Alexandra Silva
This communication is an attempt to apply the calculational style underlying the so-called Bird-Meertens formalism to generalised coinduction, as defined in F. Bartels' thesis. In particular, equational properties of such generic recursion scheme are given, relying on its universal characterisation. We also show how corresponding calculational kits for particular instances of the general coinduction are derived by specialisation.

Thu, 9 March, 2006 at 10:00
A Local Graph-rewriting System for Deciding Equality in Sum-product Theories
José Bacelar Almeida
We present a local graph-rewriting system capable of deciding equality on a fragment of the language of point-free expressions. The fragment under consideration is quite limited since it does not includes exponentials. Nevertheless, it constitutes a non-trivial exercise due to interactions between additive and multiplicative laws.

Tue, 24 January, 2006 at 11:00
The essence of dataflow programming
Tarmo Uustalu, Inst. of Cybernetics, Tallinn
We propose a novel, comonadic approach to dataflow (stream-based) computation. This is based on the observation that both general and causal stream functions can be characterized as coKleisli arrows of comonads and on the intuition that comonads in general must be a good means to structure context-dependent computation. In particular, we develop a generic comonadic interpreter of languages for context-dependent computation and instantiate it for stream-based computation. We also discuss distributive laws of a comonad over a monad as a means to structure combinations of effectful and context-dependent computation. We apply the latter to analyse clocked dataflow (partial streams based) computation.
Joint work with Varmo Vene, University of Tartu. Appeared in Proc of APLAS 2005.

Mon, 19 December, 2005 at 14:30
Strong Types for Relational Databases
Alexandra Silva
We define a strongly-typed model of relational databases and operations on them. In this model, table meta-data is represented by type-level entities that guard the semantic correctness of all database operations at compile time. The model relies on type-class bounded and parametric polymorphism and we demonstrate its encoding in the functional programming language Haskell. Apart from the standard relational database operations, such as selection and joins, we formalize functional dependencies and normalization. We show how functional dependency information can be represented at the type level, and can be transported through operations from argument types to result types. The model can be used for static query checking, but also as the basis for a formal, calculational approach to database design, programming, and migration. The model is available as sub-library of the UMinho Haskell Libraries, and goes under the name of CoddFish.

Wed, 30 November, 2005 at 12:30
Circularization of Strict Multiple Traversal Programs
João Paulo Fernandes
Functional programming provides different programming styles for programmers to write their programs in. The differences are even more explicit under a lazy evaluation model, under which a computation of a value is only triggered upon its need. When facing the challenge of implementing solutions for multiple traversals algorithm problems, the functional programmer often tends to assume himself as the decision maker of all the implementation details: how many traversals to define, in which order to schedule them, which intermediate structures to define and traverse, just to name some. Another sub-paradigm is available, though. Given the proper will and sufficient practice, multiple traversal algorithms are possible to be implemented as lazy circular programs, where some of the programming work is handed to the lazy machinery.In this talk I will present a calculational rule to convert multiple traversal programs into single-pass circular ones. Feedback is more than expected, it is wanted!

Tue, 12 July, 2005 at 10:30
Interactive point-free proof editing
Zé Pedro Correia
A BIC was recently assigned to Zé Pedro Correia. Its subject is to develop a tool to manipulate point-free expressions, according to transformation laws, in order to construct a point-free proof. This talk will serve to introduce this project to the Research.PURe group, presenting the work done so far and the work to do. We also expect to collect some opinions on the general expected "behaviour" of the tool.
Tue, 12 July, 2005 at 11:30
Calculating Circular Programs
Joao Fernandes
Abstract to be announced

Tue, 28 June, 2005
Strategic Term Rewriting and Its Application to a VDM-SL to SQL Conversion
Paulo Silva
We constructed a tool, called VooDooM, which converts datatypes in VDM-SL into SQL relational data models. The conversion involves transformation of algebraic types to maps and products, and pointer introduction. The conversion is specified as a theory of refinement by calculation. The implementation technology is strategic term rewriting in Haskell, as supported by the Strafunski bundle. Due to these choices of theory and technology, the road from theory to practise is straightforward.

Tue, March 22, 2005
Transformações Pointwise - Pointfree
JoseProenca
Na programação funcional existem vários estilos de programação, não havendo consenso quanto a qual será o melhor. Dois estilos opostos são, por exemplo, pointfree e pointwise, que se distinguem principalmente por no primeiro serem utilizadas variáveis e no segundo não. No trabalho foi introduzida uma possível descrição de expressões em pointfree e em pointwise, de tal forma que estas fossem o mais simples possível. Depois foi introduzido um processo que permite converter expressões entre estes dois tipos. Foram também consideradas outras linguagens pointwise que podem ser convertidas para o tipo pointwise originalmente criado. O principal objectivo foi tornar possível a transição de código pointwise para pointfree, utilizando bases teóricas e com a garantia de que não sejam introduzidos erros no processo de conversão.

Tue, March 15, 2005
PURe CAMILA: A System for Software Development using Formal Methods
João F. Ferreira
This work consists in the first steps for the re-implementation of CAMILA, which is a software development environment intended to promote the use of formal methods in industrial software environments. The new CAMILA, also called Research.PURe CAMILA, is written in Haskell and makes use of monadic programming. A small prototype interpreter was created, but the purpose of this work is to study the concepts behind such a tool, such as datatype invariants and partial functions.

Tue, March 8, 2005
Towards a Catalog of Aspect-Oriented Refactorings
Miguel Monteiro
In this paper, we present a collection of aspect-oriented refactorings covering both the extraction of aspects from object-oriented legacy code and the subsequent tidying up of the resulting aspects. In some cases, this tidying up entails the replacement of the original implementation with a different, centralized design, made possible by modularization. The collection of refactorings includes the extraction of common code in various aspects into abstract superaspects. We review the traditional object-oriented code smells in the light of aspect-orientation and propose some new smells for the detection of crosscutting concerns. In addition, we propose a new code smell that is specific to aspects.

Tue, February 1, 2005up
Visual Language for Pointfree Programming
José Miguel Vilaça
Miguel Vilaça will introduce the topic of designing a visual language for pointfree programming. After this, we will exchange ideas about how to approach this problem.

Tue, January 18, 2005
Functional dependency theory made 'simpler' (pdf)
JoseNunoOliveira
In the context of Joost Visser's Spreadsheets under Scrutiny talk, I have been looking at refinement laws for spreadsheet normalization. Back to good-old `functional dependency theory', D. Maier's book etc, I ended up by rephrasing of the standard theory using the binary relation pointfree calculus. It turns out that the theory becomes simpler and more general, thanks to the calculus of 'simplicity' and coreflexivity. This research also shows the effectiveness of the binary relation calculus in «explaining» and reasoning about the n-ary relation calculus «à la Codd».

Tue, December 21, 2004
Extreme Grammaring (presentation slides)
TiagoAlves
Grammars are to parser generators what programming languages are to compilers. Although parsing is a subset of a well studied area like compilers, grammars were always looked upon as "the ugly duckling". In this presentation I will propose a methodology for developing grammars using the SDF (Syntax Definition Formalism) inspired in Extreme Programming. This methodology was used to develop a grammar for ISO VDM-SL, one of the most common languages used for formal specification. The grammar is available from: VooDooMFront.

Tue, December 14, 2004
title to be completed
Damijan Rebernak
Damijan Rebernak from Maribor University, Slovenia, will present a talk on grammar-based tools. NOTE: The talk will start at 12:00, instead of the usual hour of 11:00.

Tue, December 7, 2004
Generalizing the Hylo-shift law
JorgeSousaPinto
In the Pure Workhsop last Sptember a limitation of the Hylo-shift law for program calculation was identified, and a possible way of solving it was then discussed. In this talk I will present my current understanding of how a generalized version of the law can be formalized.

Thu, Oct 26, 2004
Spreadsheets under Scrutiny
JoostVisser
In this talk we will show how Haskell can be used to process spreadsheets. We will demonstrate a prototype that takes an excell workbook as input, converts it to gnumeric's xml representation of spreadsheets with formulas, reads and parses the xml representation into a strongly type set of haskell datatypes, and finally computes and visualizes the spreadsheet data flow graph. The audience will be invited to suggest interesting spreadsheet analyses and transformations that might be implemented with this infrastructure.

Wed, 20 Oct, 2004
A Survey of Slicing Techniques
NunoRodrigues
Abstract not yet available

Thu, 22 July, 2004
Generalised LR Parsing in Haskell
Joao Fernandes
This is a sneak preview of the student presentation João will give at the Summer School on Advanced Functional Programming (Tartu, 21 august, 2004). GLR parsing is a generalization of LR parsing where ambiguous grammars do not lead to parse errors, but to several parsers working in parallel. We have implemented GLR in Haskell relying on lazy evaluation and incremental computation to improve its performance and approach closer to the original imperative formulation of the algorithm.

Thu, 3 June, 2004
Data Model Reverse Engineering from Legacy Source Code
JoostVisser
The data models of most legacy software systems are not explicitly defined. Instead, they are encoded in the program source code. Using a mixture of program understanding techniques it is possible to (partly) reconstruct these models. In this talk we provide details of a reverse engineering project carried out at the Software Improvement Group. In this project, the software portfolio of a large multinational bank, consisting of many million lines of Cobol code, was analyzed. Both hierarchical databases (IMS) and relational ones (DB2) are used in this portfolio. We will survey the program understanding techniques used, and detail the particular challenges posed by the size and heterogeneity of the analyzed portfolio.

Thu, 20 may, 2004
Constrained datatypes and datatype invariants: a relational approach (slides)
JoseNunoOliveira
Datatype invariants are a significant part of the business logic which is at the heart of any commercial software application. However, invariants are hard to maintain consistent and their formal verification requires costly «invent and verify» procedures, most often neglected throughout the development life-cycle. We sketch a basis for a calculational approach to maintaining invariants based on a «correct by construction» development principle. We propose that invariants take the place of data-types in the diagrams that describe computations and use weakest liberal preconditions to type the arrows in such diagrams. All our reasoning is carried out in the relational calculus structured by Galois connections.

Thu, 13 may, 2004
Complexity Inference
ManuelBernardoBarbosa
Abstract not available

Thu, 6 may, 2004
Incremental and Lazy Generalised LR Parsing
JoaoSaraiva
Parser combinators elegantly and concisely model generalised LL parsers in a purely functional language. They nicely illustrate the concepts of higher-order functions, polymorphic functions and lazy evaluation. Indeed, parser combinators are often presented as "the" motivating example for functional programming. Generalised LL, however, has an important drawback: it does not handle (direct nor indirect) left recursive context-free grammars.
In a different context, the (non-functional) parsing community has been doing a considerable amount of work on generalised LR parsing. Such parsers handle virtually any context-free grammar. Surprisingly, no work has been done on generalised LR by the functional prog. community. In this talk, I will present a concise (100 lines!), elegant and efficient implementation of an incremental generalised LR parser generator/interpreter in Haskell. Such parsers rely heavily on lazy evaluation. Incremental evaluation is obtained via function memoisation. I will present the HaGlr tool: a prototype implementation of our generalised LR parser generator. The profiling of some (toy) examples will be discussed.

Thu, 29 april, 2004
Lightweight Structural Invariants
JoseBacelarAlmeida
We present some ideias of how structural invariants can be attached to types.

Thu, 1 apr, 2004
Connectors as relations
MarcoAntonioBarbosa
The basic motivation of component based development is to replace conventional programming by the composition and configuration of reusable off-the-shelf units externally coordinated, through a network of connecting devices, to achieve a common goal. This work introduces a new relational model for connectors of software components. The proposed model adopts a coordination point of view in order to deal with components temporal and spatial decoupling and, therefore, to provide support for looser levels of inter-component dependency and effective external control.

Thu, 25 mar, 2004
A Unified Approach for the Integration of Distributed Heterogeneous Software Components
Barrett Bryant
A framework is proposed for assembling software systems from distributed heterogeneous components. For the successful deployment of such a software system, it is necessary that its realization not only meets the functional requirements but also non-functional requirements such as Quality of Service (QoS) criteria. The approach described is based on the notions of a meta-component model called the Unified Meta Model (UMM), a generative domain model, and specification of appropriate QoS parameters. A formal specification based on Two-Level Grammar is used to represent these notions in a tightly integrated way so that QoS becomes a part of the generative domain model. A simple case study is described in the context of this framework.

Thu, 18 mar, 2004
Gilles Barthe
Type Isomorphisms and Proof Reuse in Dependent Type Theory

Thu, 11 mar, 2004
Generic Sorting by Insertion
JorgeSousaPinto
We show that three popular functional sorting algorithms can be seen as having a common structure derived from insertion sort. Slides available here.

Thu, 4 mar, 2004
Developing Haskell Software
Joost Visser
In this talk, I will give a brief overview of Haskell software development around the world and I will present a light-weight infrastructure to support such development by us. Among other things, I will talk about development tools such as Haddock, QuickCheck, HUnit, and GHood. I will point out some nice development projects that seem relevant to the Research.PURe project, such as the refactoring project in Kent.

Thu, 26 feb, 2004
Advanced Functional Programming Project Presentations
Students
The students in the course on Advanced Functional Programming will present their project work:
  • Football Robots in HASKELL
  • Software Evaluation as a Web service
  • Querying and Transforming XML in HASKELL

Thu, 19 feb, 2004
Point-free Program Transformation
AlcinoCunha, JorgeSousaPinto
Functional programs are particularly well suited to formal manipulation by equational reasoning. In this setting, it is straightforward to use calculational methods for program transformation. Well-known transformation techniques, like tupling or the introduction of accumulating parameters, can be implemented using calculation through the use of the fusion (or promotion) strategy. In this paper we revisit this transformation method, but, unlike most of the previous work on this subject, we adhere to a pure point-free calculus that emphasizes the advantages of equational reasoning. We focus on the accumulation strategy initially proposed by Bird, where the transformed programs are seen as higher-order folds calculated systematically from a specification. The machinery of the calculus is expanded with higher-order point-free operators that simplify the calculations. A substantial number of examples (both classic and new) are fully developed, and we introduce several shortcut optimization rules that capture typical transformation patterns.

Thu, 12 feb, 2004
Transposing Relations: from Maybe-functions to Hash-Tables
JoseNunoOliveira
Functional transposition is a technique for converting relations into functions aimed at developing the relational algebra via the algebra of functions. This talk attempts to develop a basis for generic transposition. Two well-known instances of the construction are considered, one applicable to any relation and the other applicable to simple relations only. Our illustration of the usefulness of the generic transpose takes advantage of the free theorem of a polymorphic function. We show how to derive laws of relational combinators as free theorems of their transposes. Finally, we relate the topic of functional transposition with the hash-table technique for data representation.

Thu, 5 feb, 2004
Revisiting Sorting Morphisms
JoseBarros, JorgeSousaPinto, ManuelBernardoBarbosa
Members of the Research.PURe team seem to see in sorting algorithms a never-ending source of inspiration. In this session JoseBarros and ManuelBernardoBarbosa will explain why they think program-understanding can help optimize sorting algorithms, and JorgeSousaPinto will discuss how all major functional sorting algorithms can be derived from insertion sort.

Thu, 29 jan, 2004
Invitation to Wiki
AlcinoCunha, JoostVisser
We will explain the basics of collaborative web editing with Wiki. We will discuss the way we have organized our local Wiki and invite you to contribute to it. Finally we will exchange ideas about how to use the Wiki for our research and education.

r82 - 28 Jun 2007 - 11:45:16 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM