安全性和有效性属性

计算机程序执行的属性--特别是对于并发和分布式系统--长期以来一直是通过给出安全属性（坏事不会发生）和有效性属性（好事会发生）来制定。一个简单的例子可以说明安全性和灵活性。一个程序对于一个前提条件来说是完全正确的{displaystyleQ}的状态中终止。.完全正确性是安全属性和活泼属性的结合。安全属性禁止这些坏事：在满足P的状态下开始的执行{displaystyleP}的状态下开始执行，并在满足P的状态开始，并在最终状态下终止，该状态不满足活性属性，即好的东西，是指在满足P的状态下开始的执行{DisplaystyleP}的状态下开始的执行会终止。就会终止。请注意，坏事是离散的，因为它发生在执行过程中的一个特定地点。好事不需要是离散的，但终止的有效性属性是离散的。最终为安全属性和有效性属性提出的正式定义表明，这种分解不仅在直觉上有吸引力，而且是完整的：一个执行的所有属性都是安全和有效性属性的结合。此外，进行分解是有帮助的，因为正式的定义可以证明必须用不同的方法来验证安全属性和验证活泼性属性。

在满足给定前提条件的状态下开始执行，但最终状态不满足所需的后置条件；两个并发进程的执行，其中两个进程的程序计数器都指定了关键部分的语句；两个并发进程的执行，每个进程都在等待另一个进程改变状态（称为死锁）。程序的执行可以通过给出执行过程中产生的无限的程序状态序列来正式描述，其中终止程序的最后状态会无限重复。

有效性属性为每个执行规定了好的事情，或者说，描述了在执行过程中必须发生的事情。