Angelic nondeterminism in the unifying theories of programming

Hdl Handle:
http://hdl.handle.net/10149/58302
Title:
Angelic nondeterminism in the unifying theories of programming
Authors:
Cavalcanti, A. (Ana); Woodcock, J. C. P. (Jim); Dunne, S. E. (Steve)
Affiliation:
University of York. Department of Computer Science; University of Teesside. School of Computing.
Citation:
Cavalcanti, A., Woodcock, J. and Dunne, S. (2006) 'Angelic nondeterminism in the unifying theories of programming', Formal Aspects of Computing, 18 (3) pp.288-307.
Publisher:
Springer Verlag
Journal:
Formal Aspects of Computing
Issue Date:
Sep-2006
URI:
http://hdl.handle.net/10149/58302
DOI:
10.1007/s00165-006-0001-8
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.
Type:
Article
Keywords:
semantics; unifying theories of programming; UTP; refinement; relations; predicate transformers; programming
ISSN:
0934-5043
Rights:
Author can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 12/11/09]
Citation Count:
1 [Scopus, 12/11/2009]

Full metadata record

DC FieldValue Language
dc.contributor.authorCavalcanti, A. (Ana)-
dc.contributor.authorWoodcock, J. C. P. (Jim)-
dc.contributor.authorDunne, S. E. (Steve)-
dc.date.accessioned2009-04-01T10:48:28Z-
dc.date.available2009-04-01T10:48:28Z-
dc.date.issued2006-09-
dc.identifier.citationFormal Aspects of Computing; 18 (3): 288-307-
dc.identifier.issn0934-5043-
dc.identifier.doi10.1007/s00165-006-0001-8-
dc.identifier.urihttp://hdl.handle.net/10149/58302-
dc.description.abstractHoare 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.-
dc.publisherSpringer Verlag-
dc.rightsAuthor can archive post-print (ie final draft post-refereeing). For full details see http://www.sherpa.ac.uk/romeo/ [Accessed 12/11/09]-
dc.subjectsemantics-
dc.subjectunifying theories of programming-
dc.subjectUTP-
dc.subjectrefinement-
dc.subjectrelations-
dc.subjectpredicate transformers-
dc.subjectprogramming-
dc.titleAngelic nondeterminism in the unifying theories of programming-
dc.typeArticle-
dc.contributor.departmentUniversity of York. Department of Computer Science; University of Teesside. School of Computing.-
dc.identifier.journalFormal Aspects of Computing-
ref.assessmentRAE 2008-
ref.citationcount1 [Scopus, 12/11/2009]-
or.citation.harvardCavalcanti, A., Woodcock, J. and Dunne, S. (2006) 'Angelic nondeterminism in the unifying theories of programming', Formal Aspects of Computing, 18 (3) pp.288-307.-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.