Safety and liveness properties
ಕಂಪ್ಯೂಟರ್ ಪ್ರೋಗ್ರಾಂನ ಕಾರ್ಯಗತಗೊಳಿಸುವ ಗುಣಲಕ್ಷಣಗಳು-ವಿಶೇಷವಾಗಿ ಏಕಕಾಲೀನ ಮತ್ತು ವಿತರಣಾ ವ್ಯವಸ್ಥೆಗಳಿಗೆ-ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳನ್ನು ("ಕೆಟ್ಟ ವಿಷಯಗಳು ಸಂಭವಿಸುವುದಿಲ್ಲ") ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳನ್ನು ("ಒಳ್ಳೆಯ ವಿಷಯಗಳು ಸಂಭವಿಸುತ್ತವೆ") ನೀಡುವ ಮೂಲಕ ದೀರ್ಘಕಾಲದವರೆಗೆ ರೂಪಿಸಲಾಗಿದೆ. ಒಂದು ಸರಳ ಉದಾಹರಣೆಯು ಸುರಕ್ಷತೆ ಮತ್ತು ಚೈತನ್ಯವನ್ನು ವಿವರಿಸುತ್ತದೆ. ಪೂರ್ವ ಷರತ್ತು ಮತ್ತು ನಂತರದ ಷರತ್ತಿಗೆ ಸಂಬಂಧಿಸಿದಂತೆ ಯಾವುದೇ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯು ತೃಪ್ತಿಕರ ಸ್ಥಿತಿಯಲ್ಲಿ ಕೊನೆಗೊಂಡರೆ ಪ್ರೋಗ್ರಾಂ ಸಂಪೂರ್ಣವಾಗಿ ಸರಿಯಾಗಿದೆ. ಸಂಪೂರ್ಣ ನಿಖರತೆಯು ಸುರಕ್ಷತಾ ಆಸ್ತಿ ಮತ್ತು ಜೀವಂತ ಆಸ್ತಿಯ ಸಂಯೋಜನೆಯಾಗಿದೆಃ ಸುರಕ್ಷತಾ ಆಸ್ತಿಯು ಈ "ಕೆಟ್ಟ ವಿಷಯಗಳನ್ನು" ನಿಷೇಧಿಸುತ್ತದೆಃ ತೃಪ್ತಿಕರ ಸ್ಥಿತಿಯಲ್ಲಿ ಪ್ರಾರಂಭವಾಗುವ ಮತ್ತು ತೃಪ್ತಿಪಡಿಸದ ಅಂತಿಮ ಸ್ಥಿತಿಯಲ್ಲಿ ಕೊನೆಗೊಳ್ಳುವ ಮರಣದಂಡನೆಗಳು. ಪ್ರೋಗ್ರಾಂಗಾಗಿ, ಈ ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣವನ್ನು ಸಾಮಾನ್ಯವಾಗಿ ಹೋರೆ ಟ್ರಿಪಲ್ ಬಳಸಿ ಬರೆಯಲಾಗುತ್ತದೆ. ಲೈವನ್ಸ್ ಪ್ರಾಪರ್ಟಿ, "ಒಳ್ಳೆಯ ವಿಷಯ" ಎಂದರೆ, ತೃಪ್ತಿಕರ ಸ್ಥಿತಿಯಲ್ಲಿ ಪ್ರಾರಂಭವಾಗುವ ಮರಣದಂಡನೆ ಕೊನೆಗೊಳ್ಳುತ್ತದೆ. ಕೆಟ್ಟ ವಿಷಯವು ಪ್ರತ್ಯೇಕವಾಗಿದೆ ಎಂಬುದನ್ನು ಗಮನಿಸಿ, ಏಕೆಂದರೆ ಅದು ಮರಣದಂಡನೆಯ ಸಮಯದಲ್ಲಿ ನಿರ್ದಿಷ್ಟ ಸ್ಥಳದಲ್ಲಿ ಸಂಭವಿಸುತ್ತದೆ. ಒಂದು "ಒಳ್ಳೆಯ ವಿಷಯ" ವು ಪ್ರತ್ಯೇಕವಾಗಿರಬೇಕಾಗಿಲ್ಲ, ಆದರೆ ಮುಕ್ತಾಯದ ಜೀವಂತ ಗುಣವು ಪ್ರತ್ಯೇಕವಾಗಿರುತ್ತದೆ. ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳು ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳಿಗಾಗಿ ಅಂತಿಮವಾಗಿ ಪ್ರಸ್ತಾಪಿಸಲಾದ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನಗಳು ಈ ವಿಭಜನೆಯು ಅಂತರ್ಬೋಧೆಯಿಂದ ಆಕರ್ಷಕವಾಗಿರುವುದು ಮಾತ್ರವಲ್ಲದೆ ಸಂಪೂರ್ಣವಾಗಿದೆ ಎಂದು ತೋರಿಸಿದೆಃ ಮರಣದಂಡನೆಯ ಎಲ್ಲಾ ಗುಣಲಕ್ಷಣಗಳು ಸುರಕ್ಷತೆ ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳ ಸಂಯೋಜನೆಯಾಗಿದೆ. ಇದಲ್ಲದೆ, ವಿಭಜನೆಯನ್ನು ಕೈಗೊಳ್ಳುವುದು ಸಹಾಯಕವಾಗಬಹುದು, ಏಕೆಂದರೆ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನಗಳು ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಪರಿಶೀಲಿಸಲು ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಪರಿಶೀಲಿಸಲು ವಿಭಿನ್ನ ವಿಧಾನಗಳನ್ನು ಬಳಸಬೇಕು ಎಂಬುದಕ್ಕೆ ಪುರಾವೆಯನ್ನು ಒದಗಿಸುತ್ತವೆ. ಸುರಕ್ಷತೆ ಸುರಕ್ಷತಾ ಆಸ್ತಿಯು ಮರಣದಂಡನೆಯ ಸಮಯದಲ್ಲಿ ವ್ಯತಿರಿಕ್ತವಾದ ಕೆಟ್ಟ ಸಂಗತಿಗಳು ಸಂಭವಿಸುವುದನ್ನು ನಿಷೇಧಿಸುತ್ತದೆ. ಹೀಗೆ ಸುರಕ್ಷತಾ ಆಸ್ತಿಯು ಯಾವುದನ್ನು ನಿಷೇಧಿಸಲಾಗಿದೆ ಎಂಬುದನ್ನು ಹೇಳುವ ಮೂಲಕ ಅನುಮತಿಸಲಾಗಿದೆಯೆಂದು ನಿರೂಪಿಸುತ್ತದೆ. ಕೆಟ್ಟ ವಿಷಯವು ಪ್ರತ್ಯೇಕವಾಗಿರಬೇಕು ಎಂಬ ಅವಶ್ಯಕತೆ ಎಂದರೆ ಮರಣದಂಡನೆಯ ಸಮಯದಲ್ಲಿ ಸಂಭವಿಸುವ ಕೆಟ್ಟ ವಿಷಯವು ಕೆಲವು ಗುರುತಿಸಬಹುದಾದ ಹಂತದಲ್ಲಿ ಅನಿವಾರ್ಯವಾಗಿ ಸಂಭವಿಸುತ್ತದೆ. ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣವನ್ನು ವ್ಯಾಖ್ಯಾನಿಸಲು ಬಳಸಬಹುದಾದ ಪ್ರತ್ಯೇಕವಾದ ಕೆಟ್ಟ ವಿಷಯದ ಉದಾಹರಣೆಗಳೆಂದರೆಃ ನಿರ್ದಿಷ್ಟ ಪೂರ್ವ ಷರತ್ತನ್ನು ತೃಪ್ತಿಪಡಿಸುವ ಸ್ಥಿತಿಯಲ್ಲಿ ಪ್ರಾರಂಭವಾಗುವ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯು ಕೊನೆಗೊಳ್ಳುತ್ತದೆ, ಆದರೆ ಅಂತಿಮ ಸ್ಥಿತಿಯು ಅಗತ್ಯವಾದ ಪೋಸ್ಟ್ ಷರತ್ತನ್ನು ಪೂರೈಸುವುದಿಲ್ಲ; ಎರಡು ಏಕಕಾಲೀನ ಪ್ರಕ್ರಿಯೆಗಳ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆ, ಅಲ್ಲಿ ಎರಡೂ ಪ್ರಕ್ರಿಯೆಗಳಿಗೆ ಪ್ರೋಗ್ರಾಂ ಕೌಂಟರುಗಳು ನಿರ್ಣಾಯಕ ವಿಭಾಗದೊಳಗೆ ಹೇಳಿಕೆಗಳನ್ನು ಗೊತ್ತುಪಡಿಸುತ್ತದೆ; ಪ್ರತಿ ಪ್ರಕ್ರಿಯೆಯು ಮತ್ತೊಂದು ಸ್ಥಿತಿಯನ್ನು ಬದಲಾಯಿಸಲು ಕಾಯುತ್ತಿರುವ ಎರಡು ಏಕಕಾಲೀನ ಪ್ರಕ್ರಿಯೆಗಳ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆ (ಡೆಡ್ಲಾಕ್ ಎಂದು ಕರೆಯಲಾಗುತ್ತದೆ). ಒಂದು ಪ್ರೋಗ್ರಾಂನ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯನ್ನು ಪ್ರೋಗ್ರಾಂನ ಅನಂತ ಅನುಕ್ರಮವನ್ನು ನೀಡುವ ಮೂಲಕ ಔಪಚಾರಿಕವಾಗಿ ವಿವರಿಸಬಹುದು, ಅದು ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯು ಮುಂದುವರಿಯುತ್ತದೆ, ಅಲ್ಲಿ ಕೊನೆಗೊಳ್ಳುವ ಪ್ರೋಗ್ರಾಂನ ಕೊನೆಯ ಸ್ಥಿತಿಯನ್ನು ಅನಂತವಾಗಿ ಪುನರಾವರ್ತಿಸಲಾಗುತ್ತದೆ. ಆಸಕ್ತಿಯ ಪ್ರೋಗ್ರಾಂಗಾಗಿ, ಸಂಭವನೀಯ ಪ್ರೋಗ್ರಾಂ ಸ್ಥಿತಿಗಳ ಗುಂಪನ್ನು ಸೂಚಿಸೋಣ, ಪ್ರೋಗ್ರಾಂ ಸ್ಥಿತಿಗಳ ಸೀಮಿತ ಅನುಕ್ರಮಗಳ ಗುಂಪನ್ನು ಸೂಚಿಸೋಣ ಮತ್ತು ಪ್ರೋಗ್ರಾಂ ಸ್ಥಿತಿಗಳ ಅನಂತ ಅನುಕ್ರಮಗಳ ಗುಂಪನ್ನು ಸೂಚಿಸೋಣ. ಈ ಸಂಬಂಧವು ಅನುಕ್ರಮಗಳಿಗೆ ಅನ್ವಯಿಸುತ್ತದೆ ಮತ್ತು ಐಎಫ್ಎಫ್ ಎಂಬುದು ಅಥವಾ ಸಮಾನವಾದ ಪೂರ್ವಪ್ರತ್ಯಯವಾಗಿದೆ. ಒಂದು ಕಾರ್ಯಕ್ರಮದ ಆಸ್ತಿಯು ಅನುಮತಿಸಲಾದ ಮರಣದಂಡನೆಗಳ ಗುಂಪಾಗಿದೆ. ಸುರಕ್ಷತಾ ಆಸ್ತಿಯ ಅತ್ಯಗತ್ಯ ಲಕ್ಷಣವೆಂದರೆಃ ಕೆಲವು ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯು ತೃಪ್ತಿಪಡಿಸದಿದ್ದರೆ, ಆ ಸುರಕ್ಷತಾ ಆಸ್ತಿಯನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುವ ಕೆಟ್ಟ ವಿಷಯವು ಕೆಲವು ಹಂತದಲ್ಲಿ ಸಂಭವಿಸುತ್ತದೆ. ಅಂತಹ ಕೆಟ್ಟ ವಿಷಯದ ನಂತರ, ಮುಂದಿನ ಮರಣದಂಡನೆಯು ಮರಣದಂಡನೆಗೆ ಕಾರಣವಾದರೆ, ಅದು ತೃಪ್ತಿಪಡಿಸುವುದಿಲ್ಲ ಎಂಬುದನ್ನು ಗಮನಿಸಿ, ಏಕೆಂದರೆ ಕೆಟ್ಟ ವಿಷಯವೂ ಸಹ ಸಂಭವಿಸುತ್ತದೆ. ಕೆಟ್ಟ ವಸ್ತುಗಳ ಪರಿಹಾರಸಾಧ್ಯತೆಯ ಬಗೆಗಿನ ಈ ತೀರ್ಮಾನವನ್ನು ನಾವು ಸುರಕ್ಷತಾ ಆಸ್ತಿಯೆಂದು ವ್ಯಾಖ್ಯಾನಿಸುವ ಲಕ್ಷಣವೆಂದು ಪರಿಗಣಿಸುತ್ತೇವೆ. ಇದನ್ನು ಪೂರ್ವಭಾವಿ ತರ್ಕದಲ್ಲಿ ಔಪಚಾರಿಕಗೊಳಿಸುವುದು ಸುರಕ್ಷತಾ ಆಸ್ತಿ ಎಂಬುದಕ್ಕೆ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನವನ್ನು ನೀಡುತ್ತದೆ. ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳ ಈ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನವು ಒಂದು ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯು ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣವನ್ನು ತೃಪ್ತಿಪಡಿಸಿದರೆ (ಕೊನೆಯ ಸ್ಥಿತಿಯನ್ನು ಪುನರಾವರ್ತಿಸುವುದರೊಂದಿಗೆ) ಪ್ರತಿಯೊಂದು ಪೂರ್ವಪ್ರತ್ಯಯವೂ ಸಹ ತೃಪ್ತಿಪಡಿಸುತ್ತದೆ ಎಂದು ಸೂಚಿಸುತ್ತದೆ. ಲೈವನ್ಸ್ ಆಸ್ತಿಯು ಪ್ರತಿ ಮರಣದಂಡನೆಗೆ ಒಳ್ಳೆಯ ವಿಷಯಗಳನ್ನು ಸೂಚಿಸುತ್ತದೆ ಅಥವಾ, ಸಮಾನವಾಗಿ, ಮರಣದಂಡನೆಯ ಸಮಯದಲ್ಲಿ ಸಂಭವಿಸಬೇಕಾದ ಏನನ್ನಾದರೂ ವಿವರಿಸುತ್ತದೆ. ಒಳ್ಳೆಯ ವಿಷಯವು ಪ್ರತ್ಯೇಕವಾಗಿರಬೇಕಾಗಿಲ್ಲ-ಇದು ಅನಂತ ಸಂಖ್ಯೆಯ ಹಂತಗಳನ್ನು ಒಳಗೊಂಡಿರಬಹುದು. ಲೈವನ್ಸ್ ಪ್ರಾಪರ್ಟಿಯನ್ನು ವ್ಯಾಖ್ಯಾನಿಸಲು ಬಳಸುವ ಒಳ್ಳೆಯ ವಿಷಯದ ಉದಾಹರಣೆಗಳೆಂದರೆಃ ಸೂಕ್ತ ಸ್ಥಿತಿಯಲ್ಲಿ ಪ್ರಾರಂಭಿಸಲಾದ ಮರಣದಂಡನೆಯನ್ನು ಕೊನೆಗೊಳಿಸುವುದು; ಸೂಕ್ತ ಸ್ಥಿತಿಯಲ್ಲಿ ಪ್ರಾರಂಭಿಸಲಾದ ಮರಣದಂಡನೆಯನ್ನು ಕೊನೆಗೊಳಿಸದಿರುವುದು; ಪ್ರವೇಶಿಸಲು ಪ್ರಯತ್ನಿಸಿದಾಗಲೆಲ್ಲಾ ನಿರ್ಣಾಯಕ ವಿಭಾಗಕ್ಕೆ ಅಂತಿಮವಾಗಿ ಪ್ರವೇಶವನ್ನು ಖಾತರಿಪಡಿಸುವುದು; ವಿವಾದದ ಉಪಸ್ಥಿತಿಯಲ್ಲಿ ಸಂಪನ್ಮೂಲಕ್ಕೆ ನ್ಯಾಯಯುತ ಪ್ರವೇಶ. ಮೊದಲ ಉದಾಹರಣೆಯಲ್ಲಿನ ಒಳ್ಳೆಯ ವಿಷಯವು ಪ್ರತ್ಯೇಕವಾಗಿದೆ ಆದರೆ ಇತರರಲ್ಲಿ ಅಲ್ಲ. ನಿರ್ದಿಷ್ಟ ನೈಜ-ಸಮಯದ ಮಿತಿಯೊಳಗೆ ಉತ್ತರವನ್ನು ಒದಗಿಸುವುದು ಲೈವನ್ಸ್ ಆಸ್ತಿಯ ಬದಲು ಸುರಕ್ಷತಾ ಆಸ್ತಿಯಾಗಿದೆ. ಏಕೆಂದರೆ ಒಂದು ಪ್ರತ್ಯೇಕವಾದ ಕೆಟ್ಟ ವಸ್ತುವನ್ನು ನಿಷೇಧಿಸಲಾಗುತ್ತಿದೆಃ ಉತ್ತರವನ್ನು ಇನ್ನೂ ಉತ್ಪಾದಿಸದ ಸ್ಥಿತಿಯನ್ನು ತಲುಪುವ ಭಾಗಶಃ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆ ಮತ್ತು ಗಡಿಯಾರದ ಮೌಲ್ಯವು (ಸ್ಥಿತಿ ವೇರಿಯೇಬಲ್) ಮಿತಿಯನ್ನು ಉಲ್ಲಂಘಿಸುತ್ತದೆ. ಡೆಡ್ಲಾಕ್ ಸ್ವಾತಂತ್ರ್ಯವು ಸುರಕ್ಷತೆಯ ಆಸ್ತಿಯಾಗಿದೆಃ "ಕೆಟ್ಟ ವಿಷಯ" ಎಂದರೆ ಡೆಡ್ಲಾಕ್ (ಇದು ಪ್ರತ್ಯೇಕವಾಗಿದೆ). ಹೆಚ್ಚಿನ ಸಮಯ, ಒಂದು ಪ್ರೋಗ್ರಾಂ ಅಂತಿಮವಾಗಿ ಕೆಲವು "ಒಳ್ಳೆಯ ಕೆಲಸ" ಮಾಡುತ್ತದೆ ಎಂದು ತಿಳಿದಿರುವುದು ತೃಪ್ತಿಕರವಲ್ಲ; ಪ್ರೋಗ್ರಾಂ ಕೆಲವು ಹಂತಗಳಲ್ಲಿ ಅಥವಾ ಕೆಲವು ಗಡುವಿನ ಮೊದಲು "ಒಳ್ಳೆಯ ಕೆಲಸವನ್ನು" ಮಾಡುತ್ತದೆ ಎಂದು ನಾವು ತಿಳಿದುಕೊಳ್ಳಲು ಬಯಸುತ್ತೇವೆ. "ಒಳ್ಳೆಯ ವಸ್ತು" ಗೆ ಒಂದು ನಿರ್ದಿಷ್ಟ ಮಿತಿಯನ್ನು ನೀಡುವ ಆಸ್ತಿಯು ಸುರಕ್ಷತಾ ಆಸ್ತಿಯಾಗಿದೆ (ಮೇಲೆ ತಿಳಿಸಿದಂತೆ), ಆದರೆ ಮಿತಿಯು ಅಸ್ತಿತ್ವದಲ್ಲಿದೆ ಎಂದು ಕೇವಲ ಪ್ರತಿಪಾದಿಸುವ ದುರ್ಬಲ ಆಸ್ತಿಯು ಜೀವಂತ ಆಸ್ತಿಯಾಗಿದೆ. ಅಂತಹ ಲೈವನ್ಸ್ ಆಸ್ತಿಯನ್ನು ಸಾಬೀತುಪಡಿಸುವುದು ಬಿಗಿಯಾದ ಸುರಕ್ಷತಾ ಆಸ್ತಿಯನ್ನು ಸಾಬೀತುಪಡಿಸುವುದಕ್ಕಿಂತ ಸುಲಭವಾಗಿರುತ್ತದೆ ಏಕೆಂದರೆ ಲೈವನ್ಸ್ ಆಸ್ತಿಯನ್ನು ಸಾಬೀತುಪಡಿಸಲು ಸುರಕ್ಷತಾ ಆಸ್ತಿಯನ್ನು ಸಾಬೀತುಪಡಿಸಲು ಅಗತ್ಯವಿರುವ ವಿವರವಾದ ಲೆಕ್ಕಪತ್ರದ ಅಗತ್ಯವಿರುವುದಿಲ್ಲ. ಸುರಕ್ಷತಾ ಆಸ್ತಿಯಿಂದ ಭಿನ್ನವಾಗಿ, ಲೈವನ್ಸ್ ಆಸ್ತಿಯು ಮರಣದಂಡನೆಯ ಯಾವುದೇ ಸೀಮಿತ ಪೂರ್ವಪ್ರತ್ಯಯವನ್ನು ತಳ್ಳಿಹಾಕಲು ಸಾಧ್ಯವಿಲ್ಲ (ಏಕೆಂದರೆ ಅಂತಹ ಒಂದು "ಕೆಟ್ಟ ವಿಷಯ" ಆಗಿರುತ್ತದೆ ಮತ್ತು ಆದ್ದರಿಂದ, ಸುರಕ್ಷತಾ ಆಸ್ತಿಯನ್ನು ವ್ಯಾಖ್ಯಾನಿಸುತ್ತದೆ). ಇದು ಲೈವನ್ಸ್ ಪ್ರಾಪರ್ಟಿಯನ್ನು ಯಾವುದೇ ಸೀಮಿತ ಪೂರ್ವಪ್ರತ್ಯಯವನ್ನು ತಳ್ಳಿಹಾಕದ ಪ್ರಾಪರ್ಟಿ ಎಂದು ವ್ಯಾಖ್ಯಾನಿಸಲು ಕಾರಣವಾಗುತ್ತದೆ. ಈ ವ್ಯಾಖ್ಯಾನವು ಒಂದು ಒಳ್ಳೆಯ ವಿಷಯವನ್ನು ಪ್ರತ್ಯೇಕವಾಗಿರುವುದಕ್ಕೆ ಸೀಮಿತಗೊಳಿಸುವುದಿಲ್ಲ-ಒಳ್ಳೆಯ ವಿಷಯವು ಎಲ್ಲವನ್ನು ಒಳಗೊಂಡಿರುತ್ತದೆ, ಇದು ಅನಂತ-ಉದ್ದದ ಕಾರ್ಯಗತಗೊಳಿಸುವಿಕೆಯಾಗಿದೆ. ಹಿಸ್ಟರಿ ಲ್ಯಾಂಪೋರ್ಟ್ ಬಹು ಪ್ರಕ್ರಿಯೆ (ಏಕಕಾಲೀನ) ಕಾರ್ಯಕ್ರಮಗಳ ನಿಖರತೆಯನ್ನು ಸಾಬೀತುಪಡಿಸುವ ತನ್ನ 1977ರ ಪ್ರಬಂಧದಲ್ಲಿ ಸುರಕ್ಷತಾ ಆಸ್ತಿ ಮತ್ತು ಜೀವಂತ ಆಸ್ತಿ ಎಂಬ ಪದಗಳನ್ನು ಬಳಸಿದ್ದಾರೆ. ಅವರು ಪೆಟ್ರಿ ನಿವ್ವಳ ಸಿದ್ಧಾಂತದಿಂದ ಪದಗಳನ್ನು ಎರವಲು ಪಡೆದರು, ಇದು ಪೆಟ್ರಿ ಬಲೆಯ "ಟೋಕನ್ಗಳು" ಅದರ "ಸ್ಥಳಗಳಿಗೆ" ಹೇಗೆ ವಿಕಸನಗೊಳ್ಳಬಹುದು ಎಂಬುದನ್ನು ವಿವರಿಸಲು ಜೀವಂತಿಕೆ ಮತ್ತು ಮಿತಿ ಎಂಬ ಪದಗಳನ್ನು ಬಳಸುತ್ತಿತ್ತು; ಪೆಟ್ರಿ ನಿವ್ವಳ ಸುರಕ್ಷತೆಯು ಮಿತಿಯ ಒಂದು ನಿರ್ದಿಷ್ಟ ರೂಪವಾಗಿತ್ತು. ಲ್ಯಾಂಪೋರ್ಟ್ ತರುವಾಯ ಮ್ಯೂನಿಚ್ನಲ್ಲಿ ವಿತರಣಾ ವ್ಯವಸ್ಥೆಗಳ ಕುರಿತು ನ್ಯಾಟೋ ಕಿರು ಕೋರ್ಸ್ಗೆ ಸುರಕ್ಷತೆಯ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನವನ್ನು ಅಭಿವೃದ್ಧಿಪಡಿಸಿದರು. ತೊದಲುವಿಕೆಯ ಅಡಿಯಲ್ಲಿ ಗುಣಲಕ್ಷಣಗಳು ಬದಲಾಗುವುದಿಲ್ಲ ಎಂದು ಅದು ಭಾವಿಸಿದೆ. ಮೇಲೆ ನೀಡಲಾದ ಸುರಕ್ಷತೆಯ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನವು ಅಲ್ಪರ್ನ್ ಮತ್ತು ಷ್ನೇಯ್ಡರ್ ಅವರ ಪ್ರಬಂಧದಲ್ಲಿ ಕಂಡುಬರುತ್ತದೆ; ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳ ಎರಡು ಔಪಚಾರಿಕತೆಗಳ ನಡುವಿನ ಸಂಬಂಧವು ಅಲ್ಪರ್ನ್, ಡೆಮರ್ಸ್ ಮತ್ತು ಷ್ನೇಯ್ಡರ್ ಅವರ ಪ್ರಬಂಧದಲ್ಲಿ ಕಂಡುಬರುತ್ತದೆ. ಆಲ್ಪರ್ನ್ ಮತ್ತು ಷ್ನೇಯ್ಡರ್ ಲೈವನ್ಸ್ಗೆ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನವನ್ನು ನೀಡುತ್ತಾರೆ, ಜೊತೆಗೆ ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳು ಮತ್ತು ಲೈವನ್ಸ್ ಗುಣಲಕ್ಷಣಗಳನ್ನು ಬಳಸಿಕೊಂಡು ಎಲ್ಲಾ ಗುಣಲಕ್ಷಣಗಳನ್ನು ನಿರ್ಮಿಸಬಹುದು ಎಂಬುದಕ್ಕೆ ಪುರಾವೆಯನ್ನು ನೀಡುತ್ತಾರೆ. ಆ ಪುರಾವೆಯು ಗಾರ್ಡನ್ ಪ್ಲಾಟ್ಕಿನ್ನ ಒಳನೋಟದಿಂದ ಸ್ಫೂರ್ತಿ ಪಡೆದಿದೆ, ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳು ಮುಚ್ಚಿದ ಸೆಟ್ಗಳಿಗೆ ಅನುಗುಣವಾಗಿರುತ್ತವೆ ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳು ಪ್ರೋಗ್ರಾಂ ಸ್ಥಿತಿಗಳ ಅನಂತ ಅನುಕ್ರಮಗಳ ಸೆಟ್ನಲ್ಲಿ ನೈಸರ್ಗಿಕ ಟೋಪೋಲಜಿಯಲ್ಲಿನ ದಟ್ಟವಾದ ಸೆಟ್ಗಳಿಗೆ ಅನುಗುಣವಾಗಿರುತ್ತವೆ. ತರುವಾಯ, ಅಲ್ಪರ್ನ್ ಮತ್ತು ಷ್ನೇಯ್ಡರ್ ಅವರು ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳು ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳ ಔಪಚಾರಿಕ ವ್ಯಾಖ್ಯಾನಗಳಿಗಾಗಿ ಬುಚಿ ಸ್ವಯಂಚಾಲಿತ ಗುಣಲಕ್ಷಣಗಳನ್ನು ನೀಡಿರುವುದು ಮಾತ್ರವಲ್ಲದೆ, ಸುರಕ್ಷತಾ ಗುಣಲಕ್ಷಣಗಳ ಪರಿಶೀಲನೆಗೆ ಅಸ್ಥಿರತೆಯ ಅಗತ್ಯವಿರುತ್ತದೆ ಮತ್ತು ಜೀವಂತ ಗುಣಲಕ್ಷಣಗಳ ಪರಿಶೀಲನೆಗೆ ಸುಸ್ಥಿರ ವಾದದ ಅಗತ್ಯವಿರುತ್ತದೆ ಎಂಬುದನ್ನು ತೋರಿಸಲು ಈ ಸ್ವಯಂಚಾಲಿತ ಸೂತ್ರೀಕರಣಗಳನ್ನು ಬಳಸಿದರು. ಆಸ್ತಿಯ ಪ್ರಕಾರ (ಸುರಕ್ಷತೆ ವರ್ಸಸ್ ಜೀವಂತತೆ) ಮತ್ತು ಪುರಾವೆಯ ಪ್ರಕಾರದ (ಅಸ್ಥಿರತೆ ವರ್ಸಸ್ ಸುಸ್ಥಿತಿ) ನಡುವಿನ ಪತ್ರವ್ಯವಹಾರವು, ಗುಣಲಕ್ಷಣಗಳನ್ನು ಸುರಕ್ಷತೆ ಮತ್ತು ಜೀವಂತತೆಯಾಗಿ ವಿಭಜನೆಗೊಳಿಸುವುದು (ಇತರ ಕೆಲವು ವಿಭಜನೆಗೆ ವಿರುದ್ಧವಾಗಿ) ಉಪಯುಕ್ತವಾದದ್ದು-ಯಾವ ರೀತಿಯ ಆಸ್ತಿಯನ್ನು ಸಾಬೀತುಪಡಿಸಬೇಕೆಂಬುದನ್ನು ತಿಳಿದುಕೊಳ್ಳುವುದು ಅಗತ್ಯವಿರುವ ಪುರಾವೆಯ ಪ್ರಕಾರವನ್ನು ನಿರ್ದೇಶಿಸುತ್ತದೆ ಎಂಬ ಬಲವಾದ ವಾದವಾಗಿತ್ತು. ಸಾಂದರ್ಭಿಕ ಗಣನೆಯ ಸೈದ್ಧಾಂತಿಕ ಗಣಕಯಂತ್ರ ವಿಜ್ಞಾನ ಮಾದರಿ ಪರಿಶೀಲನೆ