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 1 Title Page 5 Copyright 6 DECLARATION 7 ABOUT THE EDITOR 9 TABLE OF CONTENTS 11 List of Contributors 17 List of Abbreviations 21 Preface 25 Section 1: Formal Methods in Programming 27 Chapter 1 Integrating Formal Methods in XP—A Conceptual Solution 29 Abstract 29 Introduction 30 Formal Methods in Practice 32 Extreme Programming an Agile Approach 34 Agile Approaches towards Formal Methods 35 Formal Methods in XP: A Conceptual Solution 37 Evaluation of Proposed Solution 41 Discussion and Conclusions 43 Limitations and Future Work 46 References 47 Chapter 2 Formal Methods for Commercial Applications Issues vs. Solutions 51 Abstract 51 Introduction 52 Formal Methods: Issues vs. Solutions 53 Formal Methods: Motivations for Commercial Applications 56 Conclusion 60 References 62 Chapter 3 Why Formal Methods Are Considered for Safety Critical Systems? 65 Abstract 65 Introduction 66 Proposed Approach & Methodology 67 Formalization of Use Case Diagram Using Z/EVES 69 Result Analysis 74 Conclusion 75 Acknowledgements 75 References 76 Chapter 4 An Integration of UML Sequence Diagram with Formal Specification Methods- A Formal Solution Based on Z 79 Abstract 79 Introduction 80 Related Work 82 Expectations from System Specifications 83 Proposed Solution 85 Formalization of Flight Reservation System 85 Testing and Verification 89 Limitations and Future Work 91 Conclusions 91 Appendix 92 References 95 Section 2: Programming Languages Semantics 99 Chapter 5 Declarative Programming with Temporal Constraints, in the Language CG 101 Abstract 101 Introduction 102 Modeling Evolving Applications 103 Asking Temporal Questions: Queries 108 Temporal Inference: CG 111 Checking the Correctness of CG Programs 113 Implementation 117 Conclusion 119 Acknowledgment 120 References 121 Chapter 6 Lolisa: Formal Syntax and Semantics for a Subset of the Solidity Programming Language in Mathematical Tool Coq 125 Abstract 125 Introduction 126 Related Work 127 Foundational Concepts 129 Formal Syntax of Lolisa 131 Formal Semantics 138 Formal Verification of Smart Contract Using FEther 143 Discussion 146 Conclusion and Future Work 147 Appendix 148 References 151 Chapter 7 Ontology of Domains. Ontological Description Software Engineering Domain-The Standard Life Cycle 155 Abstract 155 Introduction 156 Ontology as a Basi. Formal Description of Subject Areas 158 Life Cycles Ontology of Software Systems 161 Description of Ontology of Process Testing LC 171 Life Cycle Ontology on Site 177 Conclusions 178 References 180 Chapter 8 Guidelines Based Software Engineering for Developing Software Components 183 Abstract 183 Introduction 184 Guidelines Based Software Engineering 185 Guidelines, Observations, Empirical Studies to Laws and Theories 189 Conclusion 192 References 193 Chapter 9 Intelligent Agent Based Mapping of Software Requirement Specification to Design Model 195 Abstract 195 Introduction 196 High Level Overview of IRTDM 198 Flow-Oriented Requirement Modeling to Data-Flow Architecture Mapping 199 Automating Flow-Oriented Requirement Modeling to Data-Flow Architecture Mapping 200 Intelligent Agent 207 Future Works 209 Conclusions 209 References 211 Section 3 - Finite Automata 213 Chapter 10 The Equivalent Conversion between Regular Grammar and Finite Automata 215 Abstract 215 Introduction 216 Some Equivalent Conversion Algorithms between Regular Grammar and Finite Automata 216 The Improved Version for Construction Algorithm 3 219 The Proposed Construction Algorithm 220 Related Work 222 Concluding Remarks 224 Acknowledgements 224 References 225 Chapter 11 Controllability, Reachability, and Stabilizability of Finite Automata: A Controllability Matrix Method 227 Abstract 227 Introduction 228 Preliminaries 229 Main Results 231 An Illustrative Example 238 Conclusion 240 Acknowledgments 241 References 242 Chapter 12 Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives 247 Abstract 247 Introduction 248 Preliminaries 250 Semantic BMC Encoding for Etl1+F 254 Experimental Results 263 Concluding Remarks 266 References 268 Chapter 13 An Automata-Based Approach to Pattern Matching 271 Abstract 271 Introduction 272 Analysis 276 Experiments 277 Conclusion 279 References 280 Section 4 - Formal methods and Semantics in distributed software 281 Chapter 14 Building Requirements Semantics for Networked Software Interoperability 283 Abstract 283 Introduction 284 Connecting Ontologies for Networked Software 287 Related Work 301 Conclusions 302 Acknowledgments 303 References 304 Chapter 15 Formal Semantics of OWL-S with Rewrite Logic 307 Abstract 307 Introduction 308 Related Works 309 Background 310 Abstraction of the Model 312 Dynamic Semantics in Maude 317 Case Study 324 Conclusions 328 Acknowledgement 328 References 329 Chapter 16 Web Semantic and Ontology 331 Abstract 331 What Do We Represent in an Ontology? 332 The Web Ontology Language Owl 333 Ontology Language Processors 338 Conclusion 341 References 342 Chapter 17 Web Services Conversation Adaptation Using Conditional Substitution Semantics of Application Domain Concepts 345 Abstract 345 Introduction 346 Background 349 Related Work 359 A Context-Sensitive Metaontology for Applications Domains 362 Service Conversation Model: G+ Model 368 Signature Adaptation 371 Conversation Protocol Adaptation 374 Automatic Adapter Generation 379 Experiments 383 Case Study 389 Conclusion 394 References 395 Index 399 Back Cover 404