| RULE 2006 | 7th International Workshop on Rule-Based Programming Seattle, August 11, 2006 |
RULE on Friday, August 11th
Joint RULE/WRS Invited Talk (09:00‑10:00)
| 09:00‑10:00 | Claude Kirchner
(INRIA & LORIA, Nancy, France) Rewriting (your) Calculus [pdf] |
Session 1 (10:00‑10:30)
Break (10:30‑11:00)
Session 2 (11:00‑12:30)
| 11:00‑11:30 | Victor Winter
(University of Nebraska at Omaha) Model-driven Transformation-based Generation of Java Stress Tests This paper describes a practical application of transformation-based analysis and code generation. An overview is given of an approach for automatically constructing Java stress tests whose execution exercises all "interesting" class initialization sequence possibilities for a given class hierarchy. |
| 11:30‑12:00 | Alcino Cunha
(Universidade do Minho) Joost Visser (Universidade do Minho) Strongly Typed Rewriting For Coupled Software Transformation Coupled transformations occur in software evolution when multiple artifacts must be modified in such a way that they remain consistent with each other. An important example involves the coupled transformation of a data type, its instances, and the programs that consume or produce it. Previously, we have provided a formal treatment of transformation of the first two: data types and instances. The treatment involved the construction of type-safe, type-changing strategic rewrite systems. In this paper, we extend our treatment to the transformation of corresponding data processing programs. The key insight underlying the extension is that both data migration functions and data processors can be represented in a type-safe way by a generalized abstract data type (GADT). These representations can then be subjected to program calculation rules, harnessed in a type-safe, type-preserving strategic rewrite system. For ease of calculation, we use point-free representations and corresponding calculation rules. Thus, coupled transformations are carried out in two steps. First, a type-changing rewrite system is applied to a source type to obtain a target type together with (representations of) migration functions between source and target. Then, a type-preserving rewrite system is applied to the composition of a migration function and a data processor on the source (or target) type to obtain a data processor on the target (or source) type. All rewrites are type-safe. |
| 12:00‑12:30 | Emanuel Kitzelmann
(Dept. of Information Systems and Applied Computer Science, Bamberg University) Ute Schmid (Dept. of Information Systems and Applied Computer Science, Bamberg University) Inducing Constructor Systems from Example-Terms by Detecting Syntactical Regularities We present a technique for inducing functional programs from few, well chosen input/output-examples (I/O-examples). Potential applications for automatic program or algorithm induction are to enable end-users to create their own simple programs, to assist professional programmers, or to automatically invent completely new and efficient algorithms. In our approach, programs are represented as constructor term rewriting systems (CSs) containing recursive rules. I/O-examples are a set of pairs of terms \((F(i_i), o_i)\) meaning that \(F(i_i)\)---denoting application of function \(F\) to input \(i_i\)---is rewritten to \(o_i\) by the target CS. The induction is based on detecting syntactic regularities between the example-terms. In this paper we present theoretical results and describe an algorithm for inducing programs over arbitrary signatures/data-types which consist of one function, defined by an arbitrary number of rules with an arbitrary number of non-nested recursive calls in each rule. Moreover, we give empirical results based on a prototypical implementation and discuss related work. |
Lunch break (12:30‑14:00)
Joint RULE/WRS Invited Talk (14:00‑15:00)
| 14:00‑15:00 | Dick Kieburtz
(OGI School of Science and Engineering, OHSU, Portland, Oregon) Programmed Strategies for Program Verification [ppt] Plover is an automated property-verifier for Haskell programs that has been under development for the past three years as a component of the Programatica project. In Programatica, predicate definitions and property assertions written in P-logic, a programming logic for Haskell, can be embedded in the text of a Haskell program module. P-logic properties refine the type system of Haskell but cannot be verified by type-checking alone; a more powerful logical verifier is needed. Plover codes the proof rules of P-logic, and additionally, embeds strategies and decision procedures for their application and discharge. It integrates a reduction system that implements a rewriting semantics for Haskell terms with a congruence-closure algorithm that supports reasoning with equality. It can employ splitting strategies to explore alternative valuations of expressions of type Bool or other finite data types, but these strategies lead to exponential growth of terms and must be employed cautiously. Plover itself is written in Stratego, which has proven to be a powerful language in which to write a verifier. This talk will explain the design and implementation of some of the strategies that enable Plover to comprehend Haskell and to discharge some valid property assertions. |
Session 3 (15:00‑15:30)
Break (15:30‑16:00)
Session 4 (16:00‑17:00)
| 16:00‑16:30 | Peter Olveczky
(University of Oslo) Jose Meseguer Recent Advances in Real-Time Maude This paper gives an overview of recent advances in Real-Time Maude. Real-Time Maude extends the Maude rewriting logic tool to support formal specification and analysis of object-based real-time systems. It emphasizes ease and generality of specification and supports a spectrum of analysis methods, including symbolic simulation, unbounded and time-bounded reachability analysis, and LTL model checking. Real-Time Maude can be used to specify and analyze many systems that, due to their unbounded features, such as unbounded data structures or dynamic object and message creation, cannot be modeled by current timed/hybrid automaton-based tools. We illustrate this expressiveness and generality by summarizing two case studies: (i) an advanced scheduling algorithm with unbounded queues; and (ii) a state-of-the-art wireless sensor network algorithm. In this second area we show how communication in wireless sensor networks can be easily modeled in Real-Time Maude; and how this technique has been used in our specification of the advanced OGDC wireless sensor network algorithm. To the best of our knowledge, our work on OGDC represents the first formal modeling and analysis effort on advanced wireless sensor network algorithms. Finally, we give some (often easily checkable) conditions that ensure that Real-Time Maude's analysis methods are complete, also for dense time, for object-based real-time systems. In practice, our result implies that Real-Time Maude's time-bounded search and model checking of LTL time-bounded formulas are complete decision procedures for a large and useful class of non-Zeno real-time systems that fall outside the scope of systems that can be modeled in decidable fragments of hybrid automata, including the sensor network case study discussed in this paper. |
| 16:30‑17:00 | Fernando Rosa-Velardo
(Universidad Complutense de Madrid) Coding Mobile Synchronizing Petri Nets into Rewriting Logic Mobile Synchronizing Petri Nets (MSPN's) are a model for mobility and coordination based on coloured Petri Nets, in which systems are composed of a collection of (possibly mobile) hardware devices and mobile agents, both modelled homogenously. In this paper we approach their verification, for which we have chosen to code MSPN's into rewriting logic. In order to obtain a representation of MSPN systems by means of a rewrite theory, we develop a class of them, that we call nu-Abstract Petri nets (nu-APN's), which are easily representable in that framework. Moreover, the obtained representation provides a local mechanism for fresh name generation. Then we prove that, even if nu-APN's are a particular class of MSPN systems, they are strong enough to capture the behaviour of any MSPN system. We have chosen Maude to implement nu-APN's, as well as the translation from MSPN's to nu-APN's, for which we make intensive use of its reflective features. |
Session 5: Discussion: Rule-based programming -- what's next? (17:00‑17:30)
