Difference between revisions of "Liveness"

From PKC
Jump to navigation Jump to search
(Created page with "Liveness is a complementary property of safety, which states that: '''Something good must happen with the explicitly stated logical boundaries'''. Safety is a lo...")
 
 
(3 intermediate revisions by one other user not shown)
Line 1: Line 1:
[[Liveness]] is a complementary property of [[safety]], which states that:
For a project or a computational program, [[liveness]] is about being alive, and it can be stated as a formal logical condition:
  '''Something good must happen with the explicitly stated logical boundaries'''.
  '''Something good must happen with the explicitly stated logical boundaries'''.
 
Where good is some kind of desirable and [[detectable condition]].
[[Safety]] is a logically derived property that states:  
In contrast, [[safety]] is a logically derived property that states:  
  '''Nothing bad happens given the explicitly stated logical boundaries.'''
  '''Nothing bad happens given the explicitly stated logical boundaries.'''
{{PagePostfix
|category_csd=Logic,Hoare Logic
}}

Latest revision as of 08:35, 7 December 2022

For a project or a computational program, liveness is about being alive, and it can be stated as a formal logical condition:

Something good must happen with the explicitly stated logical boundaries.

Where good is some kind of desirable and detectable condition. In contrast, safety is a logically derived property that states:

Nothing bad happens given the explicitly stated logical boundaries.

References


Related Pages