Paper Info
Title
Designs with Angelic Nondeterminism
Abstract
Hoare and He's Unifying Theories of Programming (UTP) are a predicative relational framework for the definition and combination of refinement languages for a variety of programming paradigms. Previous work has defined a theory for angelic nondeterminism in the UTP; this is basically an encoding of binary multirelations in a predicative model. In the UTP a theory of designs (pre and postcondition pairs) provides, not only a model of terminating programs, but also a stepping stone to define a theory for state-rich reactive processes. In this paper, we cast the angelic nondeterminism theory of the UTP as a theory of designs with the long-term objective of providing a model for well established refinement process algebras like Communicating Sequential Processes (CSP) and Circus.
Year
DOI
Venue
2013
10.1109/TASE.2013.18
Theoretical Aspects of Software Engineering
Keywords
Field
DocType
angelic nondeterminism,predicative model,postcondition pair,refinement process algebra,refinement language,predicative relational framework,angelic nondeterminism theory,binary multirelations,communicating sequential processes,long-term objective,relational algebra,encoding,programming paradigm,programming,refinement calculus,formal specification,algebra,utp,csp,lattices
Programming language,Programming paradigm,Refinement calculus,Computer science,Communicating sequential processes,Theoretical computer science,Formal specification,Relational algebra,Postcondition,Predicative expression,Encoding (memory)
Conference
Citations 
PageRank 
References 
3
0.41
15
Authors
2
Name
Order
Citations
PageRank
Pedro Ribeiro1184.74
Ana Cavalcanti222418.41