Algebra of Monotonic Boolean Transformers
Algebra of Monotonic Boolean Transformers
复制标题
单调布尔变换的代数
DOI：
10.1007/978-3-642-25032-3_10
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
V. Preoteasa
中科院分区：
文献类型：
--
作者：
V. Preoteasa
命令式编程语言的代数在推理程序方面已经成功。通常，程序的代数是一个代数结构，其程序为元素，并且程序组成（顺序组成，选择，跳过）作为代数操作。引入了这些代数的各种版本，以模拟部分正确性，完全正确性，精致，恶魔选择和其他方面。我们在这里介绍一个代数，该代数可用于建模完全的正确性，精致，恶魔和天使般的选择。代数的基本模型是单调布尔变形金刚（从布尔代数到本身的单调函数）。
Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We introduce here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of our algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).