Safety and Liveness Properties

During the execution, we will concern certain program properties, such as program correctness, program halt, no exceptions, etc. For those program properties one may interest in, it can be divided into two categories:

  • Safety Properties, It will not step into unexpected state during program execution (such as call with unmatched parameters, array subscript out of bounds, etc.):
  • Liveness Properties, The expected state will arrive during program execution eventually(such as halt, get resource request must return successfully, etc.).

The topology of program properties will be introduced below. Finally, for any program property, it can be decomposed into the intersection of its safety component and liveness component.

Continue reading