TAPSOFT ’97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14–18, 1997 Proceedings

Corrado Böhm (auth.), Michel Bidoit, Max Dauchet (eds.)3540627812, 9783540627814

This book constitutes the refereed proceedings of the 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development (TAPSOFT’97), held in Lille, France, in April 1997.
The volume is organized in three parts: The first presents invited contributions, the second is devoted to trees in algebra in programming (CAAP) and the third to formal approaches in software engineering (FASE). The 30 revised full papers presented in the CAAP section were selected from 77 submissions; the 23 revised full papers presented in the FASE section were selected from 79 submissions.

---

Table of contents :
Theoretical Computer Science and software science: The past, the present and the future (position paper)….Pages 1-5
Future trends of TAPSOFT….Pages 6-10
New challenges for theoretical computer science….Pages 11-14
What does the future hold for theoretical computer science?….Pages 15-19
Automata theory on trees and partial orders….Pages 20-38
A theory of testing for timed automata….Pages 39-39
Conservative extensions, interpretations between theories and all that!….Pages 40-66
Specification and proof in membership equational logic….Pages 67-92
Formalism and method….Pages 93-114
CoFI: The common framework initiative for algebraic specification and development….Pages 115-137
Logicality of conditional rewrite systems….Pages 139-152
Simulating forward-branching systems with constructor systems….Pages 153-164
Reliable generalized and context dependent commutation relations….Pages 165-176
Word-into-Trees Transducers with bounded difference….Pages 177-188
Generalized quantitative temporal reasoning: An automata-theoretic approach….Pages 189-200
The Railroad Crossing Problem: Towards semantics of timed algorithms and their model checking in high level languages….Pages 201-212
Model checking through symbolic reachability graph….Pages 213-224
Optimal implementation of wait-free binary relations….Pages 225-236
Relative undecidability in the termination hierarchy of single rewrite rules….Pages 237-248
Termination proofs using gpo ordering constraints….Pages 249-260
Automatically proving termination where simplification orderings fail….Pages 261-272
Generating efficient, terminating logic programs….Pages 273-284
Modal characterization of weak bisimulation for higher-order processes….Pages 285-296
Formats of ordered SOS rules with silent actions….Pages 297-308
A uniform syntactical method for proving coinduction principles in λ-calculi….Pages 309-320
A labelled transition system for π ε -calculus….Pages 321-332
Set operations for recurrent term schematizations….Pages 333-344
Inclusion constraints over non-empty sets of trees….Pages 345-356
Grid structures and undecidable constraint theories….Pages 357-368
Predicative functional recurrence and poly-space….Pages 369-380
On the complexity of function pointer may-alias analysis….Pages 381-392
Maximum packing for biconnected outerplanar graphs….Pages 393-404
Synchronization of a line of identical processors at a given time….Pages 405-416
An algorithm for the solution of tree equations….Pages 417-428
E -unification by means of tree tuple synchronized grammars….Pages 429-440
Linear interpolation for the higher-order matching problem….Pages 441-452
A semantic framework for functional logic programming with algebraic polymorphic types….Pages 453-464
Subtyping constraints for incomplete objects….Pages 465-477
Partializing stone spaces using SFP domains….Pages 478-489
Let-polymorphism and eager type schemes….Pages 490-501
Semantics of architectural connectors….Pages 503-519
Protective interface specifications….Pages 520-534
Specifying complex and structured systems with Evolving Algebras….Pages 535-549
A comparison of modular verification techniques….Pages 550-564
A compositional proof of a real-time mutual exclusion protocol….Pages 565-579
Traces of I/O-automata in Isabelle/HOLCF….Pages 580-594
Reactive types….Pages 595-606
A type-based approach to program security….Pages 607-621
An applicative module calculus….Pages 622-636
Compositional specification of embedded systems with Statecharts….Pages 637-651
Verification of message sequence charts via template matching….Pages 652-666
Probabilistic lossy channel systems….Pages 667-681
A logic of object-oriented programs….Pages 682-696
Auxiliary variables and recursive procedures….Pages 697-711
Locality based Linda: Programming with explicit localities….Pages 712-726
A syntactic theory of dynamic binding….Pages 727-741
A unified framework for binding-time analysis….Pages 742-756
A typed intermediate language for flow-directed compilation….Pages 757-771
Action refinement as an implementation relation….Pages 772-786
Behaviour-refinement of coalgebraic specifications with coinductive correctness proofs….Pages 787-802
COMPASS: A comprehensible assertion method….Pages 803-817
Using LOTOS patterns to characterize architectural styles….Pages 818-832
Automating formal specification-based testing….Pages 833-847
TYPELAB: An environment for modular program development….Pages 849-854
TAS and IsaWin: Generic interfaces for transformational program development and theorem proving….Pages 855-858
Proving system correctness with KIV….Pages 859-862
A new proof-manager and graphic interface for the Larch Prover….Pages 863-866
A web-based animator for object specifications in a persistent environment….Pages 867-870
Publishing formal specifications in Z notation on world wide web….Pages 871-874
DOSFOP — A documentation tool for the algebraic programming language Opal….Pages 875-878
AG: A set of maple packages for symbolic computing of automata and semigroups….Pages 879-882