Search

The paper aims at presenting and analyzing the implementation of a Participatory Design Methodology within the large multidisciplinary European Project PALETTE. This methodology successfully enabled and supported the development and implementation of a "palette" of interoperable services dedicated to Communities of Practice in order to manage their knowledge asset, support collaboration, communication and decision making, and help to better animate the community life. Finally, it presents some lessons learnt that could be of interest for other multidisciplinary project in the Technology Enhanced Learning community.

This paper presents a research realised in the framework of the PALETTE project (FP6-TEL) which aimed at observing and analysing the design in use of web services and tools in the context of Communities of Practice (CoPs). Design in use consists in trialling the prototypes and their scenarios of uses and to observe the instrumental genesis carried out by the CoPs services. We first present our conceptual framework based on the instrumental genesis theory. We then present our methodology for the generation of data and the analysis. Results of a cross-case analysis done on seven cases of design in use of PALETTE services and scenarios by CoPs are then described and analysed. The discussion provides reflection that may inform the use of PALETTE services by other CoPs in other contexts. Finally, in the conclusion, we reflect on our methodological approach and results, and provide guidelines for further research.

In this paper we propose a new data model for imperfect geographic information: a twofold fuzzy region model; which is an extension of both the fuzzy region model and the egg/yolk model. We show how it is meaningful and practically useful in representing the knowledge that results from classified pixel data. By defining different operators on the model we are able to develop an imprecise quality report for geographic databases that actually uses the imperfect classification data as a reference. This allows us, despite the large amount of imperfection in geographic classifications, to use them for rather accurate error detection on geographic databases.

We present an imperative program verification system that exploits many powerful aspects of Oz. Our verification system supports an expressive assertion language for writing specifications and loop invariants. It is able to prove the correctness of elaborated imperative programs consisting of several subproblems that are checked independently. We illustrate the functionalities of our system on a few non trivial examples. Then, we explain that, using Oz constraint programming and other convenient programming mechanisms of Oz, the implementation of the system is straightforward. We also provide information about the efficiency of our implementation.

Declarative methodologies for logic program construction have been proposed for Prolog. They roughly consist of 1) building a purely logical version of the program based on a clear declarative semantics and 2) performing a number of checks about modes, types, termination and multiplicity. We plan to define a similar methodology for Mercury. This choice is motivated by the fact that type, mode, and multiplicity must be explicitly specified in Mercury, allowing the compiler to perform the second step above. In order to propose a methodology to perform the first step, we need a declarative semantics for Mercury, which has not yet been explicitly defined. The goal of the paper is to propose such a semantics pursuing simplicity and naturalness. We chose to define the semantics with respect to a unique interpretation domain, called the "universe", which is a kind of higher-order version of the Herbrand universe. Based on this simple domain, the denotation of terms and goals is naturally defined as well as the models of programs. Although the declarative semantics is primarily introduced to improve "manual" program construction by programmers, it could be used in a synthesis context.

The paper presents an analyzer for verifying the correctness of a Prolog program relative to a specification which provides a list of input/output annotations for the arguments and parameters that can be used to establish program termination. The work stems from Deville's methodology to derive Prolog programs that correctly implement their declarative meaning. In this context, we propose an algorithm that combines, adapts, and sometimes improves various existing static analyses in order to verify total correctness of Prolog programs with respect to formal specifications. Using the information computed during the verification process, an automatic complexity analysis can be also performed.

Program verification is a crucial issue in the field of program development, compilation and debugging. In this paper, we present an analyser for Prolog which aims at verifying whether the execution of a program behaves according to a given specification (behavioural assumptions). The analyser is based on the methodology of abstract interpretation. A novel notion of abstract sequence is introduced, that includes an over- approximatimation of successful inputs (this is useful to detect mutual exclusion of clauses, and expresses size relation information between successful inputs and the corresponding outputs, together with cardinality information in terms of input argument sizes.

interpretation of Prolog has received much attention in recent years leading to the development of many frameworks and algorithms. One reason for this proliferation comes from the fact that program analyses can be defined at various granularities, achieving a different trade-off between efficiency and precision. The purpose of this paper is to study this tradeoff experimentally. We review the most frequently proposed granularities which can be expressed as a two dimensional space parametrized by the form of the inputs and outputs. The resulting algorithms are evaluated on three abstract domains with very different functionalities, Mode, Prop, and Pattern to assess the impact of granularity on efficiency and accuracy. This is, to our knowledge, the first study of granularity at the algorithm level and some of the results are particularly surprising.

Fixpoint computation is a major issue in abstract interpretation. However, little attention has been devoted to the design and implementation of efficient general purpose fixpoint algorithms. This paper provides an experimental evaluation of several general-purpose optimization techniques: stabilization detection, manipulation of the sets of call patterns, and caching of abstract operations. All techniques can be included in a general fixpoint algorithm which can then be proven correct once for all and instantiated to a large variety of abstract semantics. For the sake of the experiments, we focus on a single abstract semantics for Prolog and shows the instantiations of the general-purpose algorithms to this semantics. The experiments are done on two abstract domains and a significant set of benchmarks programs. They seem to demonstrate the practical value of the approach.

The subject of this paper is Abstract Interpretation of logic programs, based on Constraint Solving over Finite Domains. More specifically, we use Toupie, a Constraint language based on the μ-calculus. Fixpoint computation is the basic execution mechanism of this language. Therefore it is very convenient and efficient for Abstract Interpretation of logic programs. The following topics are covered in this paper. 1) The semantics and implementation of Toupie are described. 2) A class of abstract domains for logic programs is defined. This class can be viewed as an extension of the domain Prop ([9]) to a limited class of first order formulas with equality. It happens that the elements of this domain coincide with the objects manipulated by Toupie, i.e. 0+ formulas. 3) Transformation rules which allow the transformation of flat logic programs into Toupie programs are given. Execution of the Toupie programs on this abstract domains provides a correct bottom-up abstract interpretation of the corresponding logic programs, i.e. a complete description of the success patterns for the program. 4) An experimental evaluation of the resulting analysis tool was performed and is thoroughly described. The system was used to analyse the benchmark programs used for the same purpose in [13, 14]. Four different instances of the generic domain were evaluated: two variants of Prop and two domains for simple (but useful) type analyses. The results show that the system is very efficient and accurate on the benchmark programs. This seems to demonstrate that the proposed approach to abstract interpretation provides a versatile alternative to previous proposals for a significant class of analyses.

Although very attractive from a theoretical standpoint, the “Program = Logic + Control” equation of logic programming is sometimes considered too idealistic by “real life” programmers. The lack of adequate tools to practically support a rigorous approach based on logic is advocated here to be a main cause of this discrepancy. An implemented environment based on a precise methodology is presented. It provides for the handling of specifications, the computer-aided construction and the prototyping of (pure) logic descriptions, and the derivation and optimization of Prolog procedures from those descriptions. The system and the methodology are outlined jointly. The system-aided construction of a complete example is presented afterwards.

The efficient implementation of generic abstract interpretation algorithms for Prolog is reconsidered. Two new optimization techniques are proposed and applied to the original algorithm of [15]: dependency on clause prefixes and caching of operations. The first improvement avoids reevaluating a clause prefix when no abstract value which it depends on has been updated. The second improvement consists of caching all operations on substitutions and reusing the results whenever possible. The algorithm together with the two optimization techniques have been implemented in $C$ (about 8000 lines of code each), tested on a large number of Prolog programs, and compared with the original implementation on an abstract domain containing modes, types, and sharing. In conjuction with refinements of the domain algorithms, they produce an average reduction of more than 58\ Extensive experimental results on the programs are given, including computation times, memory consumption, hit ratios for the caches, the number of operations performed, and the time distribution. As a main result, the improved algorithms exhibit the same efficiency as the specific tools of [29, 10], despite the fact that our abstract domain is more sophisticated and accurate. The abstract operations also take 90\ that the room left for improvement is very limited. Results on a simpler domain are also given and show that even extremely basic domains can benefit from the optimizations. The general-purpose character of the optimizations is also discussed.

A method for deducing type properties at each execution point of a Prolog procedure is proposed. Such properties allow to detect at compile-time inconsistent calls, i.e. whose arguments don't respect some type preconditions.