TY - CHAP
T1 - A Tour Through the Programming Choices
T2 - Semantics and Applications
AU - Ribeiro, Pedro
AU - Ye, Kangfeng
AU - Zeyda, Frank
AU - Miyazawa, Alvaro
N1 - © 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.
PY - 2024/9/1
Y1 - 2024/9/1
N2 - The discipline of programming, as Edsger Dijkstra would call it, has provided a formal basis for the study of programs where choices are not necessarily deterministic. That is, despite reservations from pioneers, like Tony Hoare, about the inclusion of nondeterministic behaviour in a program. For over 65 years, nondeterminism has played an important role in modelling and reasoning about programs. Moreover, there are at least two major flavours: angelic and demonic. Further programming choices, such as preferential and probabilistic, have been proposed to capture other important phenomena, for example, in the context of cyber-physical systems, distributed systems, and cryptography. In this chapter, we provide a critical account of these programming choices and their semantics, and discuss their applications. Our account focuses mainly on denotational semantics, and in particular relational models, as is fitting in honour of Jim Woodcock. We discuss approaches based on, or inspired by, weakest preconditions semantics and alphabetised relations, as found in the Unifying Theories of Programming (UTP). They are at the core of the semantics of notations such as Z and Circus, and extensions to deal with time and probabilities. Some of the ideas discussed here have been developed in close collaboration with Jim.
AB - The discipline of programming, as Edsger Dijkstra would call it, has provided a formal basis for the study of programs where choices are not necessarily deterministic. That is, despite reservations from pioneers, like Tony Hoare, about the inclusion of nondeterministic behaviour in a program. For over 65 years, nondeterminism has played an important role in modelling and reasoning about programs. Moreover, there are at least two major flavours: angelic and demonic. Further programming choices, such as preferential and probabilistic, have been proposed to capture other important phenomena, for example, in the context of cyber-physical systems, distributed systems, and cryptography. In this chapter, we provide a critical account of these programming choices and their semantics, and discuss their applications. Our account focuses mainly on denotational semantics, and in particular relational models, as is fitting in honour of Jim Woodcock. We discuss approaches based on, or inspired by, weakest preconditions semantics and alphabetised relations, as found in the Unifying Theories of Programming (UTP). They are at the core of the semantics of notations such as Z and Circus, and extensions to deal with time and probabilities. Some of the ideas discussed here have been developed in close collaboration with Jim.
KW - choice
KW - programming
KW - refinement
KW - relations
KW - semantics
KW - UTP
UR - http://www.scopus.com/inward/record.url?scp=85203091410&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-67114-2_11
DO - 10.1007/978-3-031-67114-2_11
M3 - Chapter
AN - SCOPUS:85203091410
SN - 978-3-031-67113-5
VL - 14900
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 261
EP - 305
BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
A2 - Foster, Simon
A2 - Sampaio, Auguto
PB - Springer Science and Business Media Deutschland GmbH
ER -