Perspectives Of System Informatics: 4th International Andrei Ershov Memorial Conference, Psi 2001, Akademgorodok, Novosibirsk, Russia, July 2-6, 2001 : Revised Papers Psi 2001

This Book Constitutes The Thoroughly Refereed Post-proceedings Of The 4th International Andrei Ershov Memorial Conference, Psi 2001, Held In Akademgorodok, Novosibirsk, Russia, In July 2001. The 50 Revised Papers Presented Together With 2 Invited Memorial Papers Devoted To The Work Of Andrei Ershov Were Carefully Selected During 2 Rounds Of Reviewing And Improvement. The Book Offers Topical Sections On Computing And Algorithms, Logical Methods, Verification, Program Transformation And Synthesis, Semantics And Types, Processes And Concurrency, Uml Specification, Petri Nets, Testing, Software Construction, Data And Knowledge Bases, Logic Programming, Constraint Programming, Program Analysis, And Language Implementation. [pt. 1] Memorial Session -- A.p. Ershov: A Pioneer And A Leader Of National Programming -- A.a. Lyapunov And A.p. Ershov In The Theory Of Program Schemes And The Development Of Its Logic Concepts -- [pt. 2] Computing And Algorithms -- The Abstract State Machine Paradigm: What Is In And What Is Out -- On Algorithmic Unsolvability -- [pt. 3] Logic Methods -- Resolution And Binary Decision Diagrams Cannot Simulate Each Other Polynomially -- On Expressive And Model Checking Power Of Propositional Program Logics -- An Extension Of Dynamic Logic For Modelling Ocl's @pre Operator -- Optimal Algorithms Of Event-driven Re-evaluation Of Boolean Functions -- [pt. 4] Verification -- A Transformation Of Sdl Specifications: A Step Towards The Verification -- Accurate Widenings And Boundedness Properties Of Timed Systems -- Adaptive Saturation-based Reasoning -- A Verification Approach For Distributed Abstract State Machines -- [pt. 5] Program Transformation And Synthesis --^ Transformational Construction Of Correct Pointer Algorithms -- A Theoretical Foundation Of Program Synthesis By Equivalent Transformation -- Equivalent Transformation By Safe Extension Of Data Structures -- Semantics And Transformations In Formal Synthesis At System Level -- Automated Program Synthesis For Java Programming Language -- [pt. 6] Semantics & Types -- The Varieties Of Programming Language Semantics (and Their Uses) -- Binding-time Analysis For Polymorphic Types -- An Investigation Of Compact And Efficient Number Representations In The Pure Lambda Calculus -- [pt. 7] Processes And Concurrency -- Observational Semantics For Timed Event Structures -- The Impact Of Synchronisation On Secure Information Flow In Concurrent Programs -- Dynamical Priorities Without Time Measurement And Modification Of The Tcp -- [pt. 8] Uml Specification -- From Adt To Uml-like Modelling -- Transformation Of Uml Specification To Xtg -- [pt. 9] Petri Nets --^ A Systematic Approach Towards Object-based Petri Net Formalisms -- Unfoldings Of Coloured Petri Nets -- A Net-based Multi-tier Behavior Inheritance Modelling Method -- [pt. 10] Testing -- Specification Based Testing: Towards Practice -- Java Specification Extension For Automated Test Development -- Specification-based Testing Of Firewalls -- [pt. 11] Software Construction -- Academic Vs. Industrial Software Engineering: Closing The Gap -- A Method For Recovery And Maintenance Of Software Architecture -- An Empirical Study Of Retargetable Compilers -- [pt. 12] Data & Knowledge Bases -- Conceptual Data Modeling: An Algebraic Viewpoint -- Integrating And Managing Conflicting Data -- A Knowledge Engineering Approach To Deal With 'narrative' Multimedia Documents -- Using Agents For Concurrent Querying Of Web-like Databases Via A Hyper-set Theoretic Approach -- [pt. 13] Logic Programming -- Reexecution-based Analysis Of Logic Programs With Delay Declarations --^ Pos(t): Analyzing Dependencies In Typed Logic Programs -- A Prolog Tailoring Technique On An Epilog Tailored Procedure -- [pt. 14] Constraint Programming -- Hierarchical Constraint Satisfaction Based On Subdefinite Models -- Using Constraint Solvers In Cad/cam Systems -- A Graphical Interface For Solver Cooperations -- [pt. 15] Program Analysis -- Abstract Computability Of Non-deterministic Programs Over Various Data Structures -- On Lexicographic Termination Ordering With Space Bound Certifications -- Generalised Computability And Applications To Hybrid Systems -- [pt. 16] Language Implementation -- Exploring Template Template Parameters -- Compiler-cooperative Memory Management In Java -- A Software Composition Language And Its Implementation -- Editor Definition Language And Its Implementation -- Oberon-2 As Successor Of Modula-2 In Simulation. Dines Bjørner, Manfred Broy, Alexandre V. Zamulin (eds.) Includes Bibliographical References And Index. A.P. Ershov— A Pioneer and a Leader of National Programming....Pages 1-7 A.A. Lyapunov and A.P. Ershov in the Theory of Program Schemes and the Development of Its Logic Concepts....Pages 8-23 The Abstract State Machine Paradigm: What Is in and What Is out....Pages 24-24 On Algorithmic Unsolvability....Pages 25-32 Resolution and Binary Decision Diagrams Cannot Simulate Each Other Polynomially....Pages 33-38 On Expressive and Model Checking Power of Propositional Program Logics....Pages 39-46 An Extension of Dynamic Logic for Modelling OCL’s @ pre Operator....Pages 47-54 Optimal Algorithms of Event-Driven Re-evaluation of Boolean Functions....Pages 55-63 A Transformation of SDL Specifications— A Step towards the Verification....Pages 64-78 Accurate Widenings and Boundedness Properties of Timed Systems....Pages 79-94 Adaptive Saturation-Based Reasoning....Pages 95-108 A Verification Approach for Distributed Abstract State Machines....Pages 109-115 Transformational Construction of Correct Pointer Algorithms....Pages 116-130 A Theoretical Foundation of Program Synthesis by Equivalent Transformation....Pages 131-139 Equivalent Transformation by Safe Extension of Data Structures....Pages 140-148 Semantics and Transformations in Formal Synthesis at System Level....Pages 149-156 Automated Program Synthesis for Java Programming Language....Pages 157-164 The Varieties of Programming Language Semantics And Their Uses....Pages 165-190 Binding-Time Analysis for Polymorphic Types....Pages 191-204 An Investigation of Compact and Efficient Number Representations in the Pure Lambda Calculus....Pages 205-213 Observational Semantics for Timed Event Structures....Pages 214-224 The Impact of Synchronisation on Secure Information Flow in Concurrent Programs....Pages 225-239 Dynamical Priorities without Time Measurement and Modification of the TCP....Pages 240-245 From ADT to UML-Like Modelling....Pages 246-246 Transformation of UML Specification to XTG....Pages 247-254 A Systematic Approach towards Object-Based Petri Net Formalisms....Pages 255-267 Unfoldings of Coloured Petri Nets....Pages 268-278 A Net-Based Multi-tier Behavior Inheritance Modelling Method....Pages 279-286 Specification Based Testing: Towards Practice....Pages 287-300 Java Specification Extension for Automated Test Development....Pages 301-307 Specification-Based Testing of Firewalls....Pages 308-316 Academic vs. Industrial Software Engineering: Closing the Gap....Pages 317-323 A Method for Recovery and Maintenance of Software Architecture....Pages 324-327 An Empirical Study of Retargetable Compilers....Pages 328-335 Conceptual Data Modeling: An Algebraic Viewpoint....Pages 336-348 Integrating and Managing Conflicting Data....Pages 349-362 A Knowledge Engineering Approach to Deal with ‘Narrative’ Multimedia Documents....Pages 363-377 Using Agents for Concurrent Querying of Web-Like Databases via a Hyper-Set-Theoretic Approach....Pages 378-394 Reexecution-Based Analysis of Logic Programs with Delay Declarations....Pages 395-405 Pos(T ) : Analyzing Dependencies in Typed Logic Programs....Pages 406-420 A Prolog Tailoring Technique on an Epilog Tailored Procedure....Pages 421-433 Hierarchical Constraint Satisfaction Based on Subdefinite Models....Pages 434-445 Using Constraint Solvers in CAD/CAM Systems....Pages 446-456 A Graphical Interface for Solver Cooperations....Pages 457-467 Abstract Computability of Non-deterministic Programs over Various Data Structures....Pages 468-481 On Lexicographic Termination Ordering with Space Bound Certifications....Pages 482-493 Generalised Computability and Applications to Hybrid Systems....Pages 494-499 Exploring Template Template Parameters....Pages 500-510 Compiler-Cooperative Memory Management in Java....Pages 511-518 A Software Composition Language and Its Implementation....Pages 519-529 Editor Definition Language and Its Implementation....Pages 530-537 Oberon-2 as Successor of Modula-2 in Simulation....Pages 538-545