Unifying theories of programming : 7th International Symposium, UTP 2019, dedicated to Tony Hoare on the occasion of his 85th birthday, Porto, Portugal, October 8, 2019 : proceedings

This volume contains papers presented at UTP 2019, the 7th International Symposium on Unifying Theories of Programming, held in Porto, Portugal, on the 8th of October 2019. This edition of the UTP symposium is in honor of Sir Tony Hoare, on the occasion of his 85th birthday. The papers contained in this volume were invited, and friendly refereed, original contributions sought from the UTP community. One of the papers is from the distinguished invited speaker Tony Hoare himself. Nine other additional papers compose this volume, covering several aspects of Unifying Theories of Programming. -- Provided by publisher Preface 7 Organization 10 Contents 11 Unification Approaches 13 A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic 14 1 Introduction 15 2 Extended Summary 17 2.1 The Calculus 17 2.2 Causality, Space, and Time 17 2.3 Geometry 18 2.4 Logic 19 3 The Calculus 19 3.1 The Algebra of Traces 21 3.2 Applications 22 3.3 The Algebra of Programs 22 4 Symmetries 23 5 Future Directions 24 5.1 Unifying Theories of Programming 24 5.2 Applications of Concurrent Kleene Algebra 25 5.3 Implementing the Calculus 25 5.4 Object Orientation and UTP 26 5.5 Extensions of the Calculus 27 6 Conclusion 27 References 28 A Testing Perspective on Algebraic, Denotational, and Operational Semantics 33 1 Introduction 33 2 Preliminaries 35 2.1 Model-Based Testing 35 2.2 Model-Based Mutation Testing 35 3 Operational Semanctics 36 3.1 Overview 36 3.2 Conformance of Input-Output LTSs 37 3.3 Explicit Conformance Checking 38 3.4 Action Systems 39 3.5 Symbolic Conformance Checking 39 4 Denotational Semantics 40 4.1 Transformational Systems 40 4.2 Action Systems 41 5 Algebraic Semantics 42 6 Concluding Remarks 43 References 44 Whither Specifications as Programs 50 1 Introduction 50 2 Programs and Specifications as Binary Relations 52 3 Programs as Forward Predicate Transformers 55 4 Programs as h-Transformers 57 5 Specifications and Refinement 64 6 Related Work 67 7 Conclusion 70 References 70 Connecting Fixpoints of Computations with Strict Progress 73 1 Introduction 73 2 Basic Definitions 75 2.1 Algebraic Structures 75 2.2 A Unified Model for Computations with Progress 77 3 Overall Strategy 79 4 Connecting Fixpoints Algebraically 80 5 Connecting Fixpoints of Computations with Progress 84 6 Conclusion 88 References 88 Probabilistic Semantics for RoboChart 91 1 Introduction 91 2 RoboChart 93 3 Unifying Theories of Programming 96 4 Weakest Preconditions and Prespecifications 98 5 Weakest Completion Semantics 100 6 Probabilistic Programs 101 7 Probabilistic Choice and Combining Distributions 104 8 Nondeterministic Choice 108 9 Related Work 109 10 Conclusions and Future Work 111 A Connecting Weakest Preconditions and Prespecifications 112 References 113 Hybrid Models 117 Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow 118 1 Introduction 118 2 Preliminaries 121 2.1 AADL 121 2.2 Simulink/Stateflow 122 2.3 Design by Contract 123 3 Isollete System: A Running Example 124 3.1 Isollete System 124 3.2 Requirements 125 4 Combination of AADL and Simulink/Stateflow 125 4.1 General Framework 126 4.2 Computing Type Classifier for Simulink/Stateflow Diagrams 128 4.3 Defining Type Classifier as Contracts 129 5 Co-modelling and Co-simulation 130 5.1 Co-modelling in AADL and Simulink/Stateflow 131 5.2 Model Translation to C 133 5.3 Co-simulation 134 6 Related Work 134 7 Conclusion and Future Work 135 References 136 Hybrid Relations in Isabelle/UTP 139 1 Introduction 139 2 Hybrid Systems and Programs 140 3 Isabelle/UTP 141 4 Trace Algebra and Generalised Reactive Relations 144 5 Continuous State and Timed Traces 146 6 Hybrid Relations 148 6.1 Continuous Variables 148 6.2 Continuous Function Evolution 150 6.3 Preemption of Evolution 151 6.4 Derivatives and Ordinary Differential Equations 152 6.5 Hybrid Reactive Contracts 154 7 Mechanisation and Example 156 8 Conclusions and Discussion 158 References 160 Concurrency 163 The Inner and Outer Algebras of Unified Concurrency 164 1 Introduction 164 2 Background 165 2.1 View Command Language 165 2.2 Denotational Semantics 165 2.3 UTP Action Semantics 166 3 Approach 167 3.1 Labels and Generators 168 3.2 Semantics with Generators 169 3.3 Static and Dynamic Observables 170 3.4 Wheels-within-Wheels 171 3.5 Label Healthiness 171 4 Inner Algebras 173 4.1 Labels and Generators 173 4.2 Ground Expressions 174 4.3 Sound Substitutions 175 4.4 Actions 176 4.5 Invariants 177 5 Outer Algebras 178 6 Related Work 180 7 Conclusions 180 References 181 Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges 183 1 Introduction 183 2 Concurrent Refinement Algebra 184 3 Tests 186 4 Assertions 186 5 Parallel 187 6 Atomic Steps and Synchronous Operators 188 6.1 Abstract Synchronisation Operator 189 6.2 Parallel as a Synchronisation Operator 190 7 Encoding Specification Commands 191 8 Encoding Guarantee and Rely Conditions 191 9 Conjoining Specifications but Respecting Assumptions 193 10 Stuttering and Mumbling 195 11 Fairness 197 12 Localisation 198 13 Some Remaining Challenges 200 14 Conclusions 201 References 202 UTP Semantics of a Calculus for Mobile Ad Hoc Networks 205 1 Introduction 205 2 Review of the mCWQ Calculus 206 3 Denotational Semantics 208 3.1 Basic Commands 210 3.2 Parallel Composition 216 4 Algebraic Properties 218 5 Conclusion and Future Work 219 A Additional Definitions for Receiving with Binder 220 B Denotational Semantics for other Processes 221 References 222 Author Index 224 Front Matter ....Pages i-xiv Front Matter ....Pages 1-1 A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic (Tony Hoare, Georg Struth, Jim Woodcock)....Pages 3-21 A Testing Perspective on Algebraic, Denotational, and Operational Semantics (Bernhard K. Aichernig)....Pages 22-38 Whither Specifications as Programs (David A. Naumann, Minh Ngo)....Pages 39-61 Connecting Fixpoints of Computations with Strict Progress (Walter Guttmann)....Pages 62-79 Probabilistic Semantics for RoboChart (Jim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota, Kangfeng Ye)....Pages 80-105 Front Matter ....Pages 107-107 Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow (Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, Naijun Zhan)....Pages 109-129 Hybrid Relations in Isabelle/UTP (Simon Foster)....Pages 130-153 Front Matter ....Pages 155-155 The Inner and Outer Algebras of Unified Concurrency (Andrew Butterfield)....Pages 157-175 Developing an Algebra for Rely/Guarantee Concurrency: Design Decisions and Challenges (Ian J. Hayes, Larissa A. Meinicke)....Pages 176-197 UTP Semantics of a Calculus for Mobile Ad Hoc Networks (Xi Wu, Huibiao Zhu, Wanling Xie)....Pages 198-216 Back Matter ....Pages 217-217