Difference between revisions of "Liveness"
Jump to navigation
Jump to search
Line 2: | Line 2: | ||
'''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. | 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.''' | '''Nothing bad happens given the explicitly stated logical boundaries.''' |
Revision as of 04:40, 6 September 2021
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.