Loading...
Please wait, while we are loading the content...
Similar Documents
Symbolic Computation in Software Science : Foreword from the Editor
| Content Provider | Semantic Scholar |
|---|---|
| Author | Ida, Tetsuo Sato, Masahiko |
| Copyright Year | 2010 |
| Abstract | The series of workshops on Symbolic Computation in Software Science has been initiated by the research groups of Bruno Buchberger at RISC, Johannes Kepler University of Linz, Tetsuo Ida at the University of Tsukuba, and Masahiko Sato at Kyoto University. As the name suggests, the focus of the series is on applications of symbolic computation techniques in various areas of software science. The first workshop has been organized in the Castle of Hagenberg in July 2008. Following an open call afterwards, we received 15 submissions for this issue, five of which have been selected after rigorous reviewing. The accepted papers address theoretical and practical aspects of software science using symbolic computation techniques. The topics include a special technique for declarative programming, enhanced pattern matching for rule-based programming, rewritingbased approach to behavioral specification of systems, verification of safety properties for infinite-state systems, and languages with variable binding and α-equivalence. The tutorial by Sergio Antoy presents narrowing from a programmer's viewpoint. Narrowing is a symbolic computation technique, used in declarative programming, to rewrite or evaluate expressions that contain variables. It involves solving sets of equations, possibly with user-defined abstract data types. There have been many research papers that demonstrate the use of this technique. There have been surveys that discuss theoretical or implementation issues of narrowing. But there have been no tutorials so far on the use of narrowing for programming tasks. Antoy's article fills this gap. It explains, with carefully chosen examples, when, why, and how to use narrowing in programming. The presentation is largely informal and comprehensible for non-specialists. Another symbolic technique that plays an important role in programming is pattern matching. In their article, Horatiu Cirstea, Claude Kirchner, Radu Kopetz, and PierreEtienne Moreau extend patterns with complement symbols, which permits base searching criteria on both positive and negative conditions. Such extended patterns are called antipatterns. They have been used in the rule-based language Tom that is designed to add pattern matching capabilities to imperative languages like C or Java. In the paper, syntactic and AU (associative with unit) anti-pattern matching problems, algorithms to solve them, and their relationships with equational pattern matching are studied in detail. In the article by Masaki Nakamura, Kazuhiro Ogata, and Kokichi Futatsugi, the notion of reducibility of operation symbols in term rewriting systems is introduced and its application to algebraic specifications is investigated. An operation symbol is reducible if any term containing the symbol is reducible. Its restriction, which allows to reduce terms by the context-sensitive rewrite relation instead of the standard rewrite relation, is useful in behavioral specifications. In particular, the article shows that, using such a restriction, one can obtain a sufficient condition for behavioral coherence in behavioral specifications, |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.risc.jku.at/people/tkutsia/papers/foreword.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
