Treffer: Augmenting types with unbounded demonic and angelic nondeterminacy

Title:
Augmenting types with unbounded demonic and angelic nondeterminacy
Authors:
MORRIS, Joseph M
Source:
MPC 2004 : mathematics of program construction (Stirling, 12-14 July 2004)Lecture notes in computer science. :274-288
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 13 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Mathematics, Mathématiques, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Logiciel, Software, Génie logiciel, Software engineering, Développement logiciel, Software development, Desarrollo logicial, Langage programmation, Programming language, Lenguaje programación, Langage spécification, Specification language, Lenguaje especificación, Non déterminisme, Non determinism, No determinismo, Preuve programme, Program proof, Prueba programa, Relation ordre partiel, Partial ordering, Relación orden parcial, Treillis, Lattice, Enrejado
Document Type:
Konferenz Conference Paper
File Description:
text
Language:
English
Author Affiliations:
School of Computing, Dublin City University, Ireland
ISSN:
0302-9743
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=15993825
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15993825
Database:
PASCAL Archive

Weitere Informationen

We show how to introduce demonic and angelic nondeterminacy into the term language of each type in typical programming or specification language. For each type we introduce (binary infix) operators n and U on terms of the type, corresponding to demonic and angelic nondeterminacy, respectively. We generalise these operators to accommodate unbounded nondeterminacy. We axiomatise the operators and derive their important properties. We show that a suitable model for nondeterminacy is the free completely distributive complete lattice over a poset, and we use this to show that our axiomatisation is sound. In the process, we exhibit a strong relationship between nondeterminacy and free lattices that has not hitherto been evident. Although nondeterminacy arises naturally in specification and programming languages, we speculate that it combines fruitfully with function theory to the extent that it can play an important role in facilitating proofs of programs that have no apparent connection with nondeterminacy.