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

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.

Theoretical Computer Science and software science: The past, the present and the future (position paper).- Future trends of TAPSOFT.- New challenges for theoretical computer science.- What does the future hold for theoretical computer science?.- Automata theory on trees and partial orders.- A theory of testing for timed automata.- Conservative extensions, interpretations between theories and all that!.- Specification and proof in membership equational logic.- Formalism and method.- CoFI: The common framework initiative for algebraic specification and development.- Logicality of conditional rewrite systems.- Simulating forward-branching systems with constructor systems.- Reliable generalized and context dependent commutation relations.- Word-into-Trees Transducers with bounded difference.- Generalized quantitative temporal reasoning: An automata-theoretic approach.- The Railroad Crossing Problem: Towards semantics of timed algorithms and their model checking in high level languages.- Model checking through symbolic reachability graph.- Optimal implementation of wait-free binary relations.- Relative undecidability in the termination hierarchy of single rewrite rules.- Termination proofs using gpo ordering constraints.- Automatically proving termination where simplification orderings fail.- Generating efficient, terminating logic programs.- Modal characterization of weak bisimulation for higher-order processes.- Formats of ordered SOS rules with silent actions.- A uniform syntactical method for proving coinduction principles in ?-calculi.- A labelled transition system for ??-calculus.- Set operations for recurrent term schematizations.- Inclusion constraints over non-empty sets of trees.- Grid structures and undecidable constraint theories.- Predicative functional recurrence and poly-space.- On the complexity of function pointer may-alias analysis.- Maximum packing for biconnected outerplanar graphs.- Synchronization of a line of identical processors at a given time.- An algorithm for the solution of tree equations.- E-unification by means of tree tuple synchronized grammars.- Linear interpolation for the higher-order matching problem.- A semantic framework for functional logic programming with algebraic polymorphic types.- Subtyping constraints for incomplete objects.- Partializing stone spaces using SFP domains.- Let-polymorphism and eager type schemes.- Semantics of architectural connectors.- Protective interface specifications.- Specifying complex and structured systems with Evolving Algebras.- A comparison of modular verification techniques.- A compositional proof of a real-time mutual exclusion protocol.- Traces of I/O-automata in Isabelle/HOLCF.- Reactive types.- A type-based approach to program security.- An applicative module calculus.- Compositional specification of embedded systems with Statecharts.- Verification of message sequence charts via template matching.- Probabilistic lossy channel systems.- A logic of object-oriented programs.- Auxiliary variables and recursive procedures.- Locality based Linda: Programming with explicit localities.- A syntactic theory of dynamic binding.- A unified framework for binding-time analysis.- A typed intermediate language for flow-directed compilation.- Action refinement as an implementation relation.- Behaviour-refinement of coalgebraic specifications with coinductive correctness proofs.- COMPASS: A comprehensible assertion method.- Using LOTOS patterns to characterize architectural styles.- Automating formal specification-based testing.- TYPELAB: An environment for modular program development.- TAS and IsaWin: Generic interfaces for transformational program development and theorem proving.- Proving system correctness with KIV.- A new proof-manager and graphic interface for the Larch Prover.- A web-based animator for object specifications in a persistent environment.- Publishing formal specifications in Z notation on world wide web.- DOSFOP — A documentation tool for the algebraic programming language Opal.- AG: A set of maple packages for symbolic computing of automata and semigroups.