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

Mathematics a special art form

As we known, art is a diverse range of human activities and the products of those activities, usually involving imaginative or technical skill. Public can easily access to diverse types of art like visual arts including the creation of images or presenting object visually, literature and performing arts represented by music, theater, film and dance.However few people get the idea that there is a special art form,mathematics as well as science. Continue reading