Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2013 | Buch

Unifying Theories of Undefinedness in UTP Kapitel lesen Erstes Kapitel lesen

Unifying Theories of Programming

4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers

herausgegeben von: Burkhart Wolff, Marie-Claude Gaudel, Abderrahmane Feliachi

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 4th International Symposium on Unifying Theories of Programming, UTP 2012, held in Paris, France, in August 2012, co-located with the 18th International Symposium on Formal Methods, FM 2012. The 8 revised full papers presented together with 2 invited talks and one invited lecture were carefully reviewed and selected from 13 submissions.

Inhaltsverzeichnis

Frontmatter
Unifying Theories of Undefinedness in UTP
Abstract
In previous work, based on an original idea due to Saaltink, we proposed a unifying theory of undefined expressions in logics used for formally specifying software systems. In our current paper, we instantiate these ideas in Hoare and He’s Unifying Theories of Programming, with each different treatment of undefinedness formalized as a UTP theory. In this setting, we show how to use classical logic to prove facts in a monotonic partial logic with guards, and we describe the guards for several different UTP theories. We show how classical logic can be used to prove semi-classical facts. We apply these ideas to the COMPASS Modelling Language (CML), which is an integration of VDM and CSP in the Circus tradition. We link CML, which uses McCarthy’s left-to-right expression evaluation, and to VDM, which uses Jones’s three-valued Logic of Partial Functions.
Jim Woodcock, Victor Bandur
Unifying Theories of Programming with Monads
Abstract
The combination of probabilistic and nondeterministic choice in program calculi is a notoriously tricky problem, and one with a long history. We present a simple functional programming approach to this challenge, based on algebraic theories of computational effects. We make use of the powerful abstraction facilities of modern functional languages, to introduce the choice operations as a little embedded domain-specific language rather than having to define a language extension; we rely on referential transparency, to justify straightforward equational reasoning about program behaviour.
Jeremy Gibbons
Circus Time with Reactive Designs
Abstract
The UTP theories for CSP and Circus can be built by the combination of the theories of designs and reactive processes. Defining the CSP operators using reactive design provides a more concise, readable and uniform UTP semantics, and, more importantly, exposes the pre-postcondition semantics of the operators. For Circus Time, a few operators have been defined as reactive designs, but some important operators are still be considered. In this paper, we develop the reactive design semantics of sequential composition, hiding and recursion within Circus Time, and show how to prove some subtle laws using the new semantics.
Kun Wei, Jim Woodcock, Ana Cavalcanti
Algebra Unifies Operational Calculi
Abstract
We survey the well-known algebraic laws of sequential programming, and propose some less familiar laws for concurrent programming. On the basis of these laws, we derive a general calculus of program execution. The basic judgment of the theory is a quintuple, and we deduce its rules by algebraic reasoning. The general calculus can be specialised to obtain more familiar operational calculi, such as the structural operational semantics of Plotkin, process calculus semantics of Milner, reduction semantics with evaluation contexts of Felleisen and Hieb, and the natural semantics of Kahn. The algebra unifies these calculi, as it is simpler than each calculus derived from it, and stronger than all of them put together.
Stephan van Staden, Tony Hoare
A Probabilistic Theory of Designs Based on Distributions
Abstract
We present a theory of designs based on functions from the state space to real numbers, which we term distributions. This theory uses predicates, in the style of UTP, based on homogeneous relations between distributions, and is richer than the standard UTP theory of designs as it allows us to reason about probabilistic programs; the healthiness conditions H1–H4 of the standard theory are implicitly accounted for in the distributional theory we present. In addition we propose a Galois connection linkage between our distribution-based model of probabilistic designs, and the standard UTP model of (non-probabilistic) designs.
Riccardo Bresciani, Andrew Butterfield
The Logic of U ·(TP)2
Abstract
U ·(TP)2 is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He onwards. In this paper we focus on the underlying logic of the prover, emphasising those aspects that are tailored to support the style of proof so often used for UTP foundational work. These aspects include support for alphabets, type-inferencing, explicit substitution notation, and explicit meta-notation for general variable-binding lists in quantifiers. The need for these features is illustrated by a running example that develops a theory of UTP designs. We finish with a discussion of issues regarding the soundness of the proof tool, and linkages to existing “industrial strength” provers such as Isabelle, PVS or CoQ.
Andrew Butterfield
Conscriptions: A New Relational Model for Sequential Computations
Abstract
We define a new class of UTP homogeneous binary relations called conscriptions, which like prescriptions provide a general-correctness model of sequential computations. Their novelty is that the skip conscription is a right unit of sequential composition for all conscriptions, including even those whose assumptions refer to the after-state as well as before-state; they thus improve on prescriptions by providing a less restricted, and hence more expressive, general-correctness model for sequential computations. We also exploit our conscription concept to derive two new enriched sequential models, extended conscriptions and timed conscriptions, which differentiate between aborting and non-terminating computations.
Steve Dunne
Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude
Abstract
Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. It contains interesting features such as event-driven computation and shared-variable concurrency. This paper considers how the algebraic semantics links with the operational semantics for Verilog. Our approach is to apply the equational and rewriting logic system Maude in exploring the linking theories. Firstly we present the algebraic semantics for Verilog. We introduce the concept of head normal form and every program is expressed as a guarded choice with location status. Secondly we present the strategy of deriving operational semantics from algebraic semantics. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy. Finally we also mechanize the derived operational semantics. The results mechanized from the second and third exploration indicate that the transition system of the derived operational semantics is the same as the one based on the derivation strategy.
Huibiao Zhu, Peng Liu, Jifeng He, Shengchao Qin
Unifying Operational Semantics with Algebraic Semantics for Instantaneous Reactions
Abstract
The signal calculus for event-based synchronous languages is developed for the specification and programming of embedded systems. This paper first explores a structural operational semantics for conceptually instantaneous reactions of the signal calculus, which exhibits how the effectiveness of such reactions is produced. Further, we investigate the unifying theory of operational semantics and algebraic semantics for instantaneous reactions. On one hand, all the algebraic laws characterizing the primitives and the combinators can be established in terms of the suggested structural operational semantics which claims the soundness of the algebraic semantics. On the other hand, reactions which are equivalent from the operational perspective can be reduced to the same normal form and this demonstrates the relative completeness of algebraic semantics with respect to the operational semantics.
Chengcheng Wu, Yongxin Zhao, Huibiao Zhu
Higher-Order UTP for a Theory of Methods
Abstract
Higher-order programming admits the view of programs as values and has been shown useful to give a semantics to object-oriented languages. In building a UTP theory for object-orientation, one faces four major challenges: consistency of the program model, redefinition of methods in subclasses, recursion and mutual recursion, and simplicity. In this paper, we discuss how the UTP treatment of higher-order programs impacts on these issues and propose solutions to emerging problems. Our solutions give rise to a novel UTP theory of methods.
Frank Zeyda, Ana Cavalcanti
Denotational Semantics for a Probabilistic Timed Shared-Variable Language
Abstract
Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. We have proposed a language, which integrates probability with time and shared-variable concurrency (called PTSC [19]). We also explored its operational semantics, where a set of algebraic laws has been investigated via bisimulation.
In this paper we explore the denotational semantics for our probabilistic language. In order to deal with the above three features and the nondeterminism, we introduce a tree structure, called P-tree, to model concurrent probabilistic programs. The denotational semantics of each statement is formalized in the structure of P-tree. Based on the achieved semantics, a set of algebraic laws is explored; i.e., especially those parallel expansion laws. These laws can be proved via our achieved denotational semantics.
Huibiao Zhu, Jeff W. Sanders, Jifeng He, Shengchao Qin
Backmatter
Metadaten
Titel
Unifying Theories of Programming
herausgegeben von
Burkhart Wolff
Marie-Claude Gaudel
Abderrahmane Feliachi
Copyright-Jahr
2013
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-35705-3
Print ISBN
978-3-642-35704-6
DOI
https://doi.org/10.1007/978-3-642-35705-3

Premium Partner

    Bildnachweise