Nothing Special   »   [go: up one dir, main page]

skip to main content
research-article
Open access

Angelic nondeterminism in the unifying theories of programming

Published: 01 September 2006 Publication History

Abstract

Hoare and He’s unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He’s work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.

References

References

[1]
Back RJR and Wright J van de Snepscheut JLA A Lattice-theoretical Basis for a Specification Language Mathematics of program construction: 375th anniversary of the Groningen University. Lecture notes in computer science, vol 375 1989 Groningen Springer 139-156
[2]
Back RJR and Wright J Duality in specification languages: a lattice-theoretical approach Acta Inf 1990 27 7 583-625
[3]
Back RJR and Wright J Combining angels, demons and miracles in program specifications Theor Comput Sci 1992 100 365-383
[4]
Back RJR and Wright J Refinement calculus: a systematic introduction. Graduate texts in computer science 1998 Berlin Heidelberg New York Springer
[5]
Cavalcanti ALC and Naumann DA Eriksson L and Lindsay PA Forward simulation for data refinement of classes FME 2002: formal methods – getting ITt. Lecture notes in computer science, vol 2391 2002 BerlinHeidelberg New York Springer 471-490
[6]
Cavalcanti ALC, Sampaio ACA, and Woodcock JCP A refinement strategy for Circus Formal Aspects Comput 2003 15 2–3 146-181
[7]
Cavalcanti ALC and Woodcock JCP A weakest precondition semantics for Z Comput J 1998 41 1 1-15
[8]
Cavalcanti ALC and Woodcock JCP ZRC—a refinement calculus for Z Formal Aspects Comput 1999 10 3 267-289
[9]
Cavalcanti ALC and Woodcock JCP Angelic nondeterminism and unifying theories of programming (extended version) 2004 Technical report University of Kent—Computing Laboratory
[10]
Cavalcanti ALC and Woodcock JCP Derrick J and Boiten E Angelic nondeterminism and unifying theories of programming REFINE 2005. Eletron Notes Theoret Comput Sci, vol 137 2005 Amsterdam Elsevier
[11]
Dijkstra EW A discipline of programming 1976 Englewood Cliffs Prentice-Hall
[12]
Dunne S Butterfield A and Pahl C Recasting Hoare and He’s unifying theories of programs in the context of general correctness IWFM’01: 5th Irish workshop in formal methods 2001 Dublin BCS electronic workshops in computing
[13]
Gardiner PHB and Morgan CC Data refinement of predicate transformers Theoret Comput Sci 1991 87 143-162
[14]
Hesselink WH Programs, recursion and unbounded choice—predicate transformation semantics and transformation rules. Cambridge tracts in theoretical computer science, vol 27 1992 Cambridge Cambridge University Press
[15]
Hoare CAR and He J The weakest prespecification. Technical monograph TM-PRG-44 1985 Oxford UK Oxford University Computing Laboratory
[16]
Hoare CAR and He Jifeng Unifying theories of programming 1998 Englewood Cliffs Prentice-Hall
[17]
Jagadeesan R, Shanbhogue V, and Saraswat V Angelic non-determinism in concurrent constraint programming 1991 Xerox Park Technical report
[18]
Martin CE, Curtis SA, Rewitzky I (2004) Modelling nondeterminism. In: Mathematics of program construction. Lecture notes in computer science, pp 228–251
[19]
Morgan CC and Gardiner PHB Data refinement by calculation Acta Inf 1990 27 6 481-503
[20]
Martin AP, Gardiner PHB, and Woodcock JCP A tactical calculus Formal Aspects Comput 1996 8 4 479-489
[21]
Morgan CC Programming from specifications 1994 2 Englewood Cliffs Prentice-Hall
[22]
Rewitzky I (2003) Binary multirelations. In: Swart H, Orlowska E, Schmidt G, Roubens M (eds) Theory and application of relational structures as knowledge instruments. Lecture notes in computer science, vol 2929, pp 256–271
[23]
Woodcock JCP and Cavalcanti ALC Bert D, Bowen JP, Henson MC, and Robinson K The semantics of Circus ZB 2002: formal specification and development in Z and B. Lecture notes in computer science, vol 2272 2002 Berlin Heidelberg New York Springer 184-203
[24]
Woodcock JCP and Cavalcanti ALC Boiten EA, Derrick J, and Smith G A tutorial introduction to designs in unifying theories of programming IFM 2004: integrated formal methods. Lecture notes in computer science, vol 2999 2004 Berlin Heidelberg New York Springer 40-66 (invited tutorial)

Cited By

View all

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing
Formal Aspects of Computing  Volume 18, Issue 3
Sep 2006
133 pages
ISSN:0934-5043
EISSN:1433-299X
Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 September 2006
Accepted: 06 April 2006
Revision received: 04 April 2006
Received: 06 June 2005
Published in FAC Volume 18, Issue 3

Author Tags

  1. Semantics
  2. Refinement
  3. Relations
  4. Predicate transformers

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)31
  • Downloads (Last 6 weeks)6
Reflects downloads up to 14 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2021)Hoare and He’s Unifying Theories of ProgrammingTheories of Programming10.1145/3477355.3477369(285-316)Online publication date: 4-Oct-2021
  • (2016)Taming MultirelationsACM Transactions on Computational Logic10.1145/296490717:4(1-34)Online publication date: 11-Nov-2016
  • (2013)Simulink timed models for program verificationTheories of Programming and Formal Methods10.5555/2554641.2554647(82-99)Online publication date: 1-Jan-2013
  • (2013)Unifying theories in ProofPower-ZFormal Aspects of Computing10.1007/s00165-007-0044-525:1(133-158)Online publication date: 1-Jan-2013
  • (2012)Mechanised support for sound refinement tacticsFormal Aspects of Computing10.1007/s00165-011-0218-z24:1(127-160)Online publication date: 1-Jan-2012
  • (2008)Monadic maps and folds for multirelations in an allegoryProceedings of the 2nd international conference on Unifying theories of programming10.5555/1893459.1893466(102-121)Online publication date: 8-Sep-2008
  • (2008)UTP and temporal logic model checkingProceedings of the 2nd international conference on Unifying theories of programming10.5555/1893459.1893462(22-41)Online publication date: 8-Sep-2008
  • (2007)Chorus angelorumProceedings of the 7th international conference on Formal Specification and Development in B10.1007/11955757_5(19-33)Online publication date: 17-Jan-2007

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media