Tapsoft '93: Theory and Practice of Software Development: 4th International Joint Conference Caap/Fase, Orsay, France, April 13-17, 1993. Proceedings (Springer Series in Solid-State Sciences)

"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."--PUBLISHER'S WEBSITE 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

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.