TAPSOFT’93: Theory and Practice of Software Development: 4th International Joint Conference CAAP/FASE Orsay, France, April 13–17, 1993 Proceedings

John V. Guttag (auth.), M. -C. Gaudel, J. -P. Jouannaud (eds.)3540566104, 9783540566106

This volume contains the proceedings of the fourth International Joint Conference on the Theory and Practice of Software Development, TAPSOFT ’93. Since the first in 1985, the aim of these conferences has been to bring together theoretical computer scientists and researchers in software engineering with a view to discussing how formal methods can usefully be applied in software development. TAPSOFT ’93 consists ofthree parts: an advanced seminar, the Colloquium on Trees in Algebra and Programming (CAAP), and the Colloquium on Formal Approaches of Software Engineering (FASE). The advanced seminar includes four invited surveys and four invited conferences. The selected papers for CAAP are organized in seven sessions: specifications and proofs, concurrency, automata and counting, constraints solving, rewriting, logic and trees, analysis of algorithms, and a common session with FASE on type inference. The selected papers for FASE are presented in eight sessions: case studies in formal design and development, compositionality modules and development, formal development, foundations and analysis of formal specifications, verification of concurrent systems, model checking, parallel calculus, and a common session with CAAP on type inference.

---

Table of contents :
Goldilocks and the three specifications….Pages 1-14
On relating some models for concurrency….Pages 15-30
Compositionality results for different types of parameterization and parameter passing in specification languages….Pages 31-45
Proving ground confluence and inductive validity in constructor based equational specifications….Pages 46-60
Associative-commutative discrimination nets….Pages 61-74
Algebraic specification and development in geometric modeling….Pages 75-89
A case study in transformational design of concurrent systems….Pages 90-104
Yeast: A case study for a practical use of formal methods….Pages 105-120
Verification and comparison of transition systems….Pages 121-135
Constraining interference in an object-based design method….Pages 136-150
From π-calculus to higher-order π-calculus — and back….Pages 151-166
Hyperedge replacement with rendezvous….Pages 167-181
True concurrency semantics for a linear logic programming language with broadcast communication….Pages 182-198
A general framework for modular implementations of modular system specifications….Pages 199-214
Specifications can make programs run faster….Pages 215-229
Application of the composition principle to unity-like specifications….Pages 230-242
Trees, ordinals and termination….Pages 243-250
When is a functional tree transduction deterministic?….Pages 251-265
Automata on infinite trees with counting constraints….Pages 266-281
Directed column-convex polyominoes by recurrence relations….Pages 282-298
Object organisation in software environments for formal methods….Pages 299-313
Monads, indexes and transformations….Pages 314-327
A technique for specifying and refining TCSP processes by using guards and liveness conditions….Pages 328-342
Applications of type theory….Pages 343-355
Feature automata and recognizable sets of feature trees….Pages 356-375
About the theory of tree embedding….Pages 376-390
Linear unification of higher-order patterns….Pages 391-405
A theory of requirements capture and its applications….Pages 406-420
Exception handling and term labelling….Pages 421-436
Gate splitting in LOTOS specifications using abstract interpretation….Pages 437-452
Constructing systems as object communities….Pages 453-467
Term rewriting in CTΣ ….Pages 468-484
Optimal reductions in interaction systems….Pages 485-500
Optimal solutions to pattern matching problems….Pages 501-518
Testing for a conformance relation based on acceptance….Pages 519-528
Testability of a communicating system through an environment….Pages 529-543
Automating (specification = implementation) using equational reasoning and LOTOS….Pages 544-558
On the Ehrenfeucht-Fraïssé game in theoretical computer science….Pages 559-568
On asymptotic probabilities in logics that capture DSPACE(log n ) in presence of ordering….Pages 569-583
A propositional dense time logic….Pages 584-598
La Vraie Forme d’un Arbre….Pages 599-612
Model checking using net unfoldings….Pages 613-628
Reachability analysis on distributed executions….Pages 629-643
Property preserving abstractions under parallel composition….Pages 644-657
Types as parameters….Pages 658-670
Polymorphic type inference with overloading and subtyping….Pages 671-685
Type reconstruction with recursive types and atomic subtyping….Pages 686-701
(Un)expected path lengths of asymmetric binary search trees….Pages 702-716
Trie size in a dynamic list structure….Pages 717-731
A fully parallel calculus of synchronizing processes….Pages 732-745
Generic systolic arrays: A methodology for systolic design….Pages 746-761