Intro; Preface; Organization; Contents; Unification Approaches; A Calculus of Space, Time, and Causality: Its Algebra, Geometry, Logic; 1 Introduction; 2 Extended Summary; 2.1 The Calculus; 2.2 Causality, Space, and Time; 2.3 Geometry; 2.4 Logic; 3 The Calculus; 3.1 The Algebra of Traces; 3.2 Applications; 3.3 The Algebra of Programs; 4 Symmetries; 5 Future Directions; 5.1 Unifying Theories of Programming; 5.2 Applications of Concurrent Kleene Algebra; 5.3 Implementing the Calculus; 5.4 Object Orientation and UTP; 5.5 Extensions of the Calculus; 6 Conclusion; References

A Testing Perspective on Algebraic, Denotational, and Operational Semantics1 Introduction; 2 Preliminaries; 2.1 Model-Based Testing; 2.2 Model-Based Mutation Testing; 3 Operational Semanctics; 3.1 Overview; 3.2 Conformance of Input-Output LTSs; 3.3 Explicit Conformance Checking; 3.4 Action Systems; 3.5 Symbolic Conformance Checking; 4 Denotational Semantics; 4.1 Transformational Systems; 4.2 Action Systems; 5 Algebraic Semantics; 6 Concluding Remarks; References; Whither Specifications as Programs; 1 Introduction; 2 Programs and Specifications as Binary Relations

3 Programs as Forward Predicate Transformers4 Programs as h-Transformers; 5 Specifications and Refinement; 6 Related Work; 7 Conclusion; References; Connecting Fixpoints of Computations with Strict Progress; 1 Introduction; 2 Basic Definitions; 2.1 Algebraic Structures; 2.2 A Unified Model for Computations with Progress; 3 Overall Strategy; 4 Connecting Fixpoints Algebraically; 5 Connecting Fixpoints of Computations with Progress; 6 Conclusion; References; Probabilistic Semantics for RoboChart; 1 Introduction; 2 RoboChart; 3 Unifying Theories of Programming

4 Weakest Preconditions and Prespecifications5 Weakest Completion Semantics; 6 Probabilistic Programs; 7 Probabilistic Choice and Combining Distributions; 8 Nondeterministic Choice; 9 Related Work; 10 Conclusions and Future Work; A Connecting Weakest Preconditions and Prespecifications; References; Hybrid Models; Unified Graphical Co-modelling of Cyber-Physical Systems Using AADL and Simulink/Stateflow; 1 Introduction; 2 Preliminaries; 2.1 AADL; 2.2 Simulink/Stateflow; 2.3 Design by Contract; 3 Isollete System: A Running Example; 3.1 Isollete System; 3.2 Requirements

4 Combination of AADL and Simulink/Stateflow4.1 General Framework; 4.2 Computing Type Classifier for Simulink/Stateflow Diagrams; 4.3 Defining Type Classifier as Contracts; 5 Co-modelling and Co-simulation; 5.1 Co-modelling in AADL and Simulink/Stateflow; 5.2 Model Translation to C; 5.3 Co-simulation; 6 Related Work; 7 Conclusion and Future Work; References; Hybrid Relations in Isabelle/UTP; 1 Introduction; 2 Hybrid Systems and Programs; 3 Isabelle/UTP; 4 Trace Algebra and Generalised Reactive Relations; 5 Continuous State and Timed Traces; 6 Hybrid Relations; 6.1 Continuous Variables