Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA compositional Semantics for CHR
182
0
0.0
(
0
)
Added by
Maria Chiara Meo
Publication date
2006
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached. CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far. In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.
rate research
Read More
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption, and more generally to optimize a given program. Essentially, it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. Unfolding is one of the basic operations which is used by most program transformation systems and which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. This paper defines an unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning. We also prove that, under some suitable conditions, confluence and termination are preserved by the above transformation. To appear in Theory and Practice of Logic Programming (TPLP)
Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no other has considered unfolding of CHR programs. This paper defines a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning. We prove that confluence and termination properties are preserved by the above transformations.
It is well-known that big-step semantics is not able to distinguish stuck and non-terminating computations. This is a strong limitation as it makes very difficult to reason about properties involving infinite computations, such as type soundness, which cannot even be expressed. We show that this issue is only apparent: the distinction between stuck and diverging computations is implicit in any big-step semantics and it just needs to be uncovered. To achieve this goal, we develop a systematic study of big-step semantics: we introduce an abstract definition of what a big-step semantics is, we define a notion of computation by formalising the evaluation algorithm implicitly associated with any big-step semantics, and we show how to canonically extend a big-step semantics to characterise stuck and diverging computations. Building on these notions, we describe a general proof technique to show that a predicate is sound, that is, it prevents stuck computation, with respect to a big-step semantics. One needs to check three properties relating the predicate and the semantics and, if they hold, the predicate is sound. The extended semantics are essential to establish this meta-logical result, but are of no concerns to the user, who only needs to prove the three properties of the initial big-step semantics. Finally, we illustrate the technique by several examples, showing that it is applicable also in cases where subject reduction does not hold, hence the standard technique for small-step semantics cannot be used.
It has been an open question as to whether the Modular Structural Operational Semantics framework can express the dynamic semantics of call/cc. This paper shows that it can, and furthermore, demonstrates that it can express the more general delimited control operators control and shift.
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes. In this paper, we introduce a bottom-up, fixpoint semantics that aims to model the behavior of PROMELA programs. This work is the first step towards a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
