随着计算机技术与网络技术的发展，人们将关注点从顺序计算转向并行计算与分布式计算.并行计算与分布式计算导致了程序的非确定性，而程序的非确定性计算是计算机科学的一个重要研究课题，其研究成果可用于程序规范，程序精细，软件合成，复杂软硬件系统的分析与设计等.这种非确定性有两种不同的情况：经典的非确定性和概率非确定性.前者是指对于同一个输入可能出现不同的结果，这种非确定性被三种幂域模拟，即Plotkin幂域，Smyth幂域，Hoare幂域.后者是指对于同一个输入，给程序可能出现的结果各赋以一个概率值，这种非确定性被概率幂域模拟.这是最近较热的一个研究课题，引起世界许多著名的理论计算机科学家与数学家的关注，并且取得了一系列重要的研究成果.因为现实世界中非确定现象除了概率现象外，还有大量的可能性现象。为此，本文提出了可能性计算的概念，即给程序可能的计算结果各赋以一个可能值，这种非确定性被可能性幂域模拟。 这篇论文的主要目的是为概率与可能性非确定计算提供语义模型，主要研究工作在下面的三个方面： 第一部分：概率计算的语义模型 程序的概率计算的研究源于Kozen开创性的工作，现在主要有四种概率程序语义模型：Kozen的模型，C.Jones的模型，何积丰的模型与C.Morgan等人的模型.我们的概率计算模型是建立在C.Morgan等人的概率计算模型基础上的。我们的研究分为亚概率程序与概率程序两个方面。在亚概率程序方面，引入了亚概率程序语言，建立其公理语义与指称语义，并且证明可靠性与完备性定理．在概率程序方面，我们的研究又分为确定性概率程序与非确定概率程序．在确定型概率程序方面，我们给出一种不同于C.Morgan等人刻画健康条件的方法，成功地建立起概率谓词转换器与确定性概率状态转换器之间的等价性。在非确定概率程序方面，我们研究了天使非确定概率程序，提出了预健康的概念，证明预健康的概率谓词转换器与非确定概率状态转换器之间等价的一个方向。 第二部分：可能性计算的语义模型 本部分我们利用可能性赋值的概念给出一种可能性计算模型，目的是为了研究具有可能性的程序语义。证明可能性幂域函子是定向完备偏序集范畴Dcpo上的一个monad函子．进一步利用可能性积分证明可能状态转换器语义与健康的可能谓词转换器语义之间的等价性．同时将可能性与天使非确定性放在一起加以讨论，得到它们有关的万有性质。 第三部分：精细演算 精细演算是Dijkstra最弱前置演算的扩充与进一步发展．近来，应明生教授研究了概率程序的精细演算．基于应明生教授的一些想法，这部分本研究分为概率精细与可能性精细两个方面。一方面，我们讨论了亚概率程序的概率精细与概率正确性．这两个概念分别反映了一个亚概率程序被另一个亚概率程序精细的程度以及一个亚概率程序三元组的正确度．证明亚概率程序间的概率精细可以通过概率正确性来描述．另一方面，我们提出了一种基于可能性的程序精细演算模型，目的是为了进一步形式化可能性计算．引入可能信念逻辑，得到了基本谓词转换器之间的对偶．给出了可能谓词转换器是可能天使更新与可能魔鬼更新的充分必要条件。进一步证明形式定理，是说任意一个强单调的可能谓词转换器都是某个可能天使更新与某个可能魔鬼更新的合成。讨论了可能谓词转换器的同态特征。 最后，本文研究了一些重要的可能谓词转换器；单调的可能谓词转换器，合取与析取的可能谓词转换器，并证明所有的程序状态都是强单调的。