Programming Language Theory and Formal Methods

In this book - we present topics from: formal grammars in programming, programming languages semantics, finite automata, and formal methods and semantics in distributed software. Section 1 focuses on formal methods in programming, describing integrating formal methods in XP (extreme programming) - a conceptual solution, formal methods for commercial, applications issues vs. solutions, why formal methods are considered for safety critical systems, and integration of UML sequence diagram with formal specification methods-a formal solution based on Z. Section 2 focuses on programming languages semantics, describing declarative programming with temporal constraints, in the language CG, Lolisa: formal syntax and semantics for a subset of the solidity programming language in mathematical tool coq, ontology of domains. ontological description software engineering domain - the standard life cycle, guidelines based software engineering for developing software components, intelligent agent based mapping of software requirement specification to design model. Section 3 focuses on finite automata, describing the equivalent conversion between regular grammar and finite automata, controllability, reachability, and stabilizability of finite automata: a controllability matrix method, bounded model checking of ETL cooperating with finite and looping automata connectives, an automata-based approach to pattern matching, tree automata for extracting consensus from partial replicas of a structured document. Section 4 focuses on formal methods and semantics in distributed software, describing building requirements semantics for networked software interoperability, formal semantics of OWL-s with rewrite logic, web semantic and ontology, web services conversation adaptation using conditional substitution semantics of application domain concepts. Cover Title Page Copyright DECLARATION ABOUT THE EDITOR TABLE OF CONTENTS List of Contributors List of Abbreviations Preface Section 1: Formal Methods in Programming Chapter 1 Integrating Formal Methods in XP—A Conceptual Solution Abstract Introduction Formal Methods in Practice Extreme Programming an Agile Approach Agile Approaches towards Formal Methods Formal Methods in XP: A Conceptual Solution Evaluation of Proposed Solution Discussion and Conclusions Limitations and Future Work References Chapter 2 Formal Methods for Commercial Applications Issues vs. Solutions Abstract Introduction Formal Methods: Issues vs. Solutions Formal Methods: Motivations for Commercial Applications Conclusion References Chapter 3 Why Formal Methods Are Considered for Safety Critical Systems? Abstract Introduction Proposed Approach & Methodology Formalization of Use Case Diagram Using Z/EVES Result Analysis Conclusion Acknowledgements References Chapter 4 An Integration of UML Sequence Diagram with Formal Specification Methods- A Formal Solution Based on Z Abstract Introduction Related Work Expectations from System Specifications Proposed Solution Formalization of Flight Reservation System Testing and Verification Limitations and Future Work Conclusions Appendix References Section 2: Programming Languages Semantics Chapter 5 Declarative Programming with Temporal Constraints, in the Language CG Abstract Introduction Modeling Evolving Applications Asking Temporal Questions: Queries Temporal Inference: CG Checking the Correctness of CG Programs Implementation Conclusion Acknowledgment References Chapter 6 Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq Abstract Introduction Related Work Foundational Concepts Formal Syntax of Lolisa Formal Semantics Formal Verification of Smart Contract Using FEther Discussion Conclusion and Future Work Appendix References Chapter 7 Ontology of Domains. Ontological Description Software Engineering Domain-The Standard Life Cycle Abstract Introduction Ontology as a Basi. Formal Description of Subject Areas Life Cycles Ontology of Software Systems Description of Ontology of Process Testing LC Life Cycle Ontology on Site Conclusions References Chapter 8 Guidelines Based Software Engineering for Developing Software Components Abstract Introduction Guidelines Based Software Engineering Guidelines, Observations, Empirical Studies to Laws and Theories Conclusion References Chapter 9 Intelligent Agent Based Mapping of Software Requirement Specification to Design Model Abstract Introduction High Level Overview of IRTDM Flow-Oriented Requirement Modeling to Data-Flow Architecture Mapping Automating Flow-Oriented Requirement Modeling to Data-Flow Architecture Mapping Intelligent Agent Future Works Conclusions References Section 3 - Finite Automata Chapter 10 The Equivalent Conversion between Regular Grammar and Finite Automata Abstract Introduction Some Equivalent Conversion Algorithms between Regular Grammar and Finite Automata The Improved Version for Construction Algorithm 3 The Proposed Construction Algorithm Related Work Concluding Remarks Acknowledgements References Chapter 11 Controllability, Reachability, and Stabilizability of Finite Automata: A Controllability Matrix Method Abstract Introduction Preliminaries Main Results An Illustrative Example Conclusion Acknowledgments References Chapter 12 Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives Abstract Introduction Preliminaries Semantic BMC Encoding for Etl1+F Experimental Results Concluding Remarks References Chapter 13 An Automata-Based Approach to Pattern Matching Abstract Introduction Analysis Experiments Conclusion References Section 4 - Formal methods and Semantics in distributed software Chapter 14 Building Requirements Semantics for Networked Software Interoperability Abstract Introduction Connecting Ontologies for Networked Software Related Work Conclusions Acknowledgments References Chapter 15 Formal Semantics of OWL-S with Rewrite Logic Abstract Introduction Related Works Background Abstraction of the Model Dynamic Semantics in Maude Case Study Conclusions Acknowledgement References Chapter 16 Web Semantic and Ontology Abstract What Do We Represent in an Ontology? The Web Ontology Language Owl Ontology Language Processors Conclusion References Chapter 17 Web Services Conversation Adaptation Using Conditional Substitution Semantics of Application Domain Concepts Abstract Introduction Background Related Work A Context-Sensitive Metaontology for Applications Domains Service Conversation Model: G+ Model Signature Adaptation Conversation Protocol Adaptation Automatic Adapter Generation Experiments Case Study Conclusion References Index Back Cover