23 ਸਤੰ 2025·8 ਮਿੰਟ
ਟੋਨੀ ਹੋਅਰ ਦੇ ਸਹੀਤਾ ਵਿਚਾਰ: ਲਾਜਿਕ ਤੋਂ ਸੁਰੱਖਿਅਤ ਕੋਡ ਤੱਕ
ਸਿੱਖੋ ਕਿ ਕਿਵੇਂ Tony Hoare ਦੀ Hoare logic, Quicksort ਅਤੇ ਸੁਰੱਖਿਆ-ਮਾਨਸਿਕਤਾ ਸਹੀ ਸੌਫਟਵੇਅਰ ਲਿਖਣ ਅਤੇ ਸਮੀਖਿਆ ਕਰਨ ਦੀਆਂ ਪ੍ਰਯੋਗੀ ਤਕਨੀਕਾਂ ਨੂੰ ਰੂਪ ਦਿੰਦੀਆਂ ਹਨ।
ਸਿੱਖੋ ਕਿ ਕਿਵੇਂ Tony Hoare ਦੀ Hoare logic, Quicksort ਅਤੇ ਸੁਰੱਖਿਆ-ਮਾਨਸਿਕਤਾ ਸਹੀ ਸੌਫਟਵੇਅਰ ਲਿਖਣ ਅਤੇ ਸਮੀਖਿਆ ਕਰਨ ਦੀਆਂ ਪ੍ਰਯੋਗੀ ਤਕਨੀਕਾਂ ਨੂੰ ਰੂਪ ਦਿੰਦੀਆਂ ਹਨ।
ਜਦ ਲੋਕ ਕਹਿੰਦੇ ਹਨ ਕਿ ਇੱਕ ਪ੍ਰੋਗਰਾਮ "ਸਹੀ" ਹੈ, ਉਹ ਅਕਸਰ ਮਤਲਬ ਲੈਂਦੇ ਹਨ: "ਮੈਂ ਇਸਨੂੰ ਕੁਝ ਵਾਰੀ ਚਲਾਇਆ ਅਤੇ ਆਉਟਪੁੱਟ ਠੀਕ ਲੱਗਿਆ।" ਇਹ ਇੱਕ ਲਾਹੇਯਕ ਸੰਗੇਤ ਹੈ—ਪਰ ਇਹ ਸਹੀਤਾ ਨਹੀਂ। ਸਧਾਰਨ ਸ਼ਬਦਾਂ ਵਿੱਚ, ਸਹੀਤਾ ਦਾ ਮਤਲਬ ਹੈ ਕਿ ਪ੍ਰੋਗਰਾਮ ਆਪਣੀ ਵਿਵਰਣ ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ: ਹਰ ਮਨਜ਼ੂਰ ਇਨਪੁਟ ਲਈ, ਇਹ ਲੋੜੀਦਾ ਨਤੀਜਾ ਦਿੰਦਾ ਹੈ ਅਤੇ ਰਾਜ, ਸਮਾਂ-ਸੀਮਾਵਾਂ ਅਤੇ ਗਲਤੀਆਂ ਬਾਰੇ ਕੋਈ ਨਿਯਮ ਮੰਨਦਾ ਹੈ।
ਫਰੇਬ ਇਹ ਹੈ ਕਿ “ਇਹ ਆਪਣੀ ਵਿਵਰਣ ਨੂੰ ਪੂਰਾ ਕਰਦਾ” ਕਿਹਾ ਲਿਖਣ ਤੋਂ ਜ਼ਿਆਦਾ ਔਖਾ ਹੈ।
ਪਹਿਲਾਂ, specifications ਅਕਸਰ ਅਸਪਸ਼ਟ ਹੁੰਦੀਆਂ ਹਨ। ਇਕ ਪ੍ਰੋਡਕਟ ਦੀ ਲੋੜ ਕਹਿ ਸਕਦੀ ਹੈ “ਲਿਸਟ sort ਕਰੋ”, ਪਰ ਕੀ ਇਸਦਾ ਮਤਲਬ stable sorting ਹੈ? ਨਕਲ ਮੁੱਲਾਂ, ਖਾਲੀ ਲਿਸਟਾਂ, ਜਾਂ ਗੈਰ-ਨੰਬਰਕ ਆਈਟਮਾਂ ਨਾਲ ਕੀ ਕੀਤਾ ਜਾਵੇ? ਜੇ spec ਨਹੀਂ ਦੱਸਦੀ, ਵੱਖ-ਵੱਖ ਲੋਕ ਵੱਖ-ਵੱਖ ਧਾਰਣਾ ਕਰਦੇ ਹਨ।
ਦੂਜਾ, edge cases ਰੁੱਟੀ ਰੀਟੀ ਨਹੀਂ—ਉਹ ਸਿਰਫ ਘੱਟ ਟੈਸਟ ਕੀਤੇ ਜਾਂਦੇ ਹਨ। Null ਮੁੱਲ, overflow, off-by-one ਸੀਮਾਵਾਂ, ਅਸਧਾਰਨ ਯੂਜ਼ਰ ਲੜੀਬੰਦੀ, ਅਤੇ ਅਕਸਮਾਤ ਬਾਹਰੀ ਫੇਲ੍ਹਰ “ਇਹ ਚੱਲਦਾ ਹੈ” ਨੂੰ "ਪ੍ਰੋਡਕਸ਼ਨ ਵਿੱਚ ਫੇਲ" ਵਿੱਚ ਬਦਲ ਸਕਦੇ ਹਨ।
ਤੀਜਾ, requirements ਬਦਲਦੇ ਹਨ। ਇੱਕ ਪ੍ਰੋਗਰਾਮ ਕੱਲ ਦੀ spec ਦੇ ਨਾਤੇ ਸਹੀ ਹੋ ਸਕਦਾ ਹੈ ਅਤੇ ਅੱਜ ਦੀ spec ਦੇ ਨਾਤੇ ਗਲਤ।
Tony Hoare ਦਾ ਵੱਡਾ ਯੋਗਦਾਨ ਇਹ ਨਹੀਂ ਸੀ ਕਿ ਅਸੀਂ ਹਰ ਚੀਜ਼ ਨੂੰ ਹਮੇਸ਼ਾ ਪ੍ਰੂਵ ਕਰੀਏ। ਉਸ ਦਾ ਵਿਚਾਰ ਇਹ ਸੀ ਕਿ ਅਸੀਂ ਇਹ ਵੱਧ ਨਿਰਧਾਰਿਤ ਤਰੀਕੇ ਨਾਲ ਬਿਆਨ ਕਰ ਸਕਦੇ ਹਾਂ ਕਿ ਕੋਡ ਨੂੰ ਕੀ ਕਰਨਾ ਚਾਹੀਦਾ ਹੈ—ਅਤੇ ਇਸ ਬਾਰੇ ਨਿਯਮਤ ਢੰਗ ਨਾਲ ਸੋਚ ਸਕਦੇ ਹਾਂ।
ਇਸ ਪੋਸਟ ਵਿੱਚ ਅਸੀਂ ਤਿੰਨ ਜੁੜੇ ਹੋਏ ਧਾਗੇ ਫਾਲੋ ਕਰਾਂਗੇ:
ਜ਼ਿਆਦਾਤਰ ਟੀਮਾਂ ਪੂਰੇ ਫਾਰਮਲ ਸਬੂਤ ਨਹੀਂ ਲਿਖਣਗੀਆਂ। ਪਰ ਅੱਧ-ਭਾਗ, “ਸਬੂਤ-ਸਟਾਈਲ” ਸੋਚ ਵੀ ਬੱਗਾਂ ਦੀ ਪਹਿਚਾਣ ਆਸਾਨ ਕਰ ਸਕਦੀ ਹੈ, ਸਮੀਖਿਆਵਾਂ ਨੂੰ ਤੇਜ਼ ਕਰਦੀ ਹੈ, ਅਤੇ ਕਿਸੇ ਚੀਜ਼ ਨੂੰ ਸ਼ਿਪ ਕਰਨ ਤੋਂ ਪਹਿਲਾਂ ਵੈਹਿਆਂਨਤਾ ਸਪਸ਼ਟ ਕਰਦੀ ਹੈ।
Tony Hoare ਉਹਨਾਂ ਵੱਖਰੇ ਕੰਮ ਕਰਨ ਵਾਲੇ ਕੰਪਿਊਟਰ ਵਿਗਿਆਨੀਆਂ ਵਿੱਚੋਂ ਹੈ ਜਿਨ੍ਹਾਂ ਦਾ ਕੰਮ ਪੇਪਰਾਂ ਜਾਂ ਕਲਾਸਰੂਮ ਤੱਕ ਹੀ ਸੀਮਿਤ ਨਹੀਂ ਰਿਹਾ। ਉਹ ਅਕਾਡਮੀਅ ਅਤੇ ਇੰਡਸਟਰੀ ਦੋਹਾਂ ਵਿੱਚ ਨੇੜੇ ਰਹੇ, ਅਤੇ ਉਹ ਇੱਕ ਪ੍ਰਯੋਗੀ ਸਵਾਲ 'ਤੇ ਧਿਆਨ ਰੱਖਦੇ ਸਨ ਜੋ ਹਰ ਟੀਮ ਅਜੇ ਵੀ ਮੁੱਖ ਰੱਖਦੀ ਹੈ: ਵੱਡੇ ਸਟੇਕਾਂ ਵਾਲੀ ਸਥਿਤੀ ਵਿੱਚ ਅਸੀਂ ਕਿਵੇਂ ਜਾਣੀਏ ਕਿ ਪ੍ਰੋਗਰਾਮ ਉਹੀ ਕਰ ਰਿਹਾ ਹੈ ਜੋ ਅਸੀਂ ਸੋਚਦੇ ਹਾਂ?
ਇਹ ਲੇਖ ਕੁਝ Hoare ਦੇ ਆਈਡੀਆ 'ਤੇ ਧਿਆਨ ਦਿੰਦਾ ਹੈ ਜੋ ਅਕਸਰ ਅਸਲੀ ਕੋਡਬੇਸਾਂ ਵਿੱਚ ਵਾਪਸ ਆਉਂਦੇ ਹਨ:
{P} C {Q} ਵਰਤ ਕੇ ਪ੍ਰੋਗਰਾਮ ਬਿਹੇਵਿਅਰ ਦਾ ਵਰਣਨ।ਤੁਸੀਂ ਇਥੇ ਡੂੰਘੀ ਗਣਿਤੀ ਫਾਰਮਲਿਜ਼ਮ ਨਹੀਂ ਲੱਭੋਗੇ, ਅਤੇ ਅਸੀਂ Quicksort ਦਾ ਪੂਰਾ, ਮਸ਼ੀਨ-ਚੈਕੇਬਲ ਸਬੂਤ ਵੀ ਨਹੀਂ ਦੇਖਾਂਗੇ। ਉਦੇਸ਼ ਇਹ ਹੈ ਕਿ ਸੰਕਲਪ ਪਹੁੰਚਯੋਗ ਰਹਿਣ: ਇਤਨਾ ਢਾਂਚਾ ਕਿ ਤੁਹਾਡੀ ਸੋਚ ਸਪਸ਼ਟ ਹੋ ਜਾਏ, ਬਿਨਾਂ ਤੁਹਾਡੇ ਕੋਡ ਰਿਵਿਊ ਨੂੰ ਡਿਗਰੀ-ਸੈਮੀਨਾਰ ਵਿੱਚ ਬਦਲ ਦੇਣ ਦੇ।
Hoare ਦੇ ਵਿਚਾਰ ਆਮ ਫੈਸਲਿਆਂ ਵਿੱਚ ਤਬਦੀਲ ਹੋ ਜਾਂਦੇ ਹਨ: ਕਿਸ assumptions 'ਤੇ ਇੱਕ ਫੰਕਸ਼ਨ ਨਿਰਭਰ ਕਰਦਾ ਹੈ, ਇਹ callers ਨੂੰ ਕੀ ਗਾਰੰਟੀ ਦਿੰਦਾ ਹੈ, ਇੱਕ ਲੂਪ ਦੇ ਅੱਧੇ-ਦੌਰਾਨ ਕੀ ਸੱਚ ਰਹਿੰਦਾ ਹੈ, ਅਤੇ ਸਮੀਖਿਆ ਦੌਰਾਨ “ਲਗਭਗ ਠੀਕ” ਤਬਦੀਲੀਆਂ ਨੂੰ ਕਿਵੇਂ ਪਛਾਣਿਆ ਜਾਵੇ। ਜੇ ਤੁਸੀਂ ਕਦੇ {P} C {Q} ਖੁਲ੍ਹ ਕੇ ਨਹੀਂ ਲਿਖਦੇ, ਉਸ ਰਚਨਾ ਵਿੱਚ ਸੋਚਣਾ ਇੰਟਰਫੇਸ, ਟੈਸਟ ਅਤੇ ਗੰਭੀਰ ਕੋਡ-ਗੱਲ-ਬਾਤ ਨੂੰ ਬਿਹਤਰ ਬਣਾਉਂਦਾ ਹੈ।
Hoare ਦੀ ਨਜ਼ਰ "ਕੁਝ ਉਦਾਹਰਣਾਂ ਪਾਸ ਹੋ ਗਈਆਂ" ਤੋਂ ਕਠੋਰ ਹੈ: ਸਹੀਤਾ ਇੱਕ ਸਹਿਮਤ ਵਾਅਦੇ (agreed promise) ਨੂੰ ਮਿਲਣਾ ਹੈ, ਨਾ ਕਿ ਛੋਟੇ ਨਮੂਨਿਆਂ 'ਤੇ ਠੀਕ ਲੱਗਣਾ।
ਬੱਗ ਆਮ ਤੌਰ 'ਤੇ ਉਦੋਂ ਹੁੰਦੇ ਹਨ ਜਦ ਟੀਮ ਮੱਧਲਾ ਕਦਮ ਛੱਡ ਦਿੰਦੀ ਹੈ: ਉਹ requirements ਤੋਂ ਸਿੱਧੇ implementation 'ਤੇ ਛਾਲ ਮਾਰ ਦਿੰਦੇ ਹਨ, ਜਿਸ ਨਾਲ ਵਾਅਦਾ ਫੱਜੀ ਰਹਿ ਜਾਂਦਾ ਹੈ।
ਅਕਸਰ ਦੋ ਦਾਅਵੇ ਮਿਲ ਜਾਂਦੇ ਹਨ:
ਅਸਲੀ ਪ੍ਰਣਾਲੀਆਂ ਲਈ, “ਕਦੇ ਖਤਮ ਨਾ ਹੋਣਾ” ਵੀ “ਗਲਤ ਜਵਾਬ ਦੇਣ” ਦੇ ਬਰਾਬਰ ਨੁਕਸਾਨ ਕਰ ਸਕਦਾ ਹੈ।
ਸਹੀਤਾ ਕਦੇ ਵੀ ਸਰਵਜਨੀਕ ਨਹੀਂ ਹੁੰਦੀ; ਇਹ ਹੇਠਾਂ ਦਿੱਤੀਆਂ assumptions 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ:
assumptions ਨੂੰ ਖੁੱਲ੍ਹਾ ਕਰਨ ਨਾਲ “ਮੇਰੀ ਮਸ਼ੀਨ ਤੇ ਚੱਲਦਾ” ਕਿਸੇ ਹੋਰ ਨੂੰ reasoning ਕਰਨ ਯੋਗ ਬਣ ਜਾਂਦਾ ਹੈ।
ਇਕ ਫੰਕਸ਼ਨ sortedCopy(xs) ਸੋਚੋ।
ਇੱਕ ਉਪਯੋਗ spec ਹੋ ਸਕਦੀ ਹੈ: “ਨਵੀਂ ਲਿਸਟ ys ਵਾਪਸ ਕਰਦਾ ਹੈ ਜਿਸ ਨਾਲ (1) ys ਉਤਾਰਦੀ ਕ੍ਰਮ ਵਿੱਚ sorted ਹੈ, ਅਤੇ (2) ys ਵਿੱਚ ਠੀਕ ਉਹੀ ਤੱਤ ਹਨ ਜੋ xs ਵਿੱਚ ਸਨ (ਗਿਣਤੀਆਂ ਸਮੇਤ), ਅਤੇ (3) xs ਬਦਲੀ ਨਹੀਂ ਗਈ।”
ਹੁਣ “ਸਹੀ” ਦਾ ਮਤਲਬ ਹੈ ਕਿ ਕੋਡ ਉਪਰੋਕਤ ਤੀਨ ਨੁਕਤਿਆਂ ਨੂੰ ਦਰਸਾਈਆਂ ਗਈਆਂ assumptions ਹੇਠਾਂ ਪੂਰਾ ਕਰਦਾ ਹੈ—ਸਿਰਫ਼ ਇਸ ਲਈ ਨਹੀਂ ਕਿ ਆਊਟਪੁੱਟ ਇੱਕ ਤੇਜ਼ ਟੈਸਟ ਵਿੱਚ sorted ਲੱਗ ਰਿਹਾ ਸੀ।
Hoare logic ਪ੍ਰੋਗਰਾਮ ਬਾਰੇ ਉਨ੍ਹਾਂ ਹੀ ਤਰ੍ਹਾਂ ਗੱਲ ਕਰਦਾ ਹੈ ਜਿਵੇਂ ਤੁਸੀਂ ਕਿਸੇ ਠੇਕੇ ਦੀ ਗੱਲ ਕਰਦੇ ਹੋ: ਜੇ ਤੁਸੀਂ ਇੱਕ ਸਥਿਤੀ ਵਿੱਚ ਸ਼ੁਰੂ ਕਰਦੇ ਹੋ ਜੋ ਕੁਝ assumptions ਪੂਰੀਆਂ ਕਰਦੀ ਹੈ, ਅਤੇ ਤੁਸੀਂ ਇਹ ਟੁਕੜਾ ਕੋਡ ਚਲਾਉਂਦੇ ਹੋ, ਤਾਂ ਤੁਸੀਂ ਇੱਕ ਐਸੀ ਸਥਿਤੀ ਤੇ ਪਹੁੰਚੋਗੇ ਜੋ ਕੁਝ ਗਾਰੰਟੀਆਂ ਪੂਰੀਆਂ ਕਰਦੀ ਹੈ।
ਮੁੱਖ ਨੋਟੇਸ਼ਨ ਹੈ Hoare triple:
{precondition} program {postcondition}
A precondition ਦਸਦੀ ਹੈ ਕਿ ਕੋਡ ਟੁਕੜਾ ਚਲਾਉਣ ਤੋਂ ਪਹਿਲਾਂ ਕੀ ਸੱਚ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ। ਇਹ ਇਹ ਨਹੀਂ ਕਿ ਤੁਸੀਂ ਆਸ ਕਰੋ—ਇਹ ਉਹ ਹੈ ਜੋ ਕੋਡ ਨੂੰ ਚਾਹੀਦਾ ਹੈ।
ਉਦਾਹਰਣ: ਮੰਨੋ ਇੱਕ ਫੰਕਸ਼ਨ ਦੋ ਨੰਬਰਾਂ ਦਾ ਔਸਤ ਦੇਂਦਾ ਹੈ ਬਗੈਰ overflow ਚੈੱਕਾਂ ਦੇ।
a + b integer ਟਾਈਪ ਵਿੱਚ ਫਿੱਟ ਹੁੰਦਾ ਹੈavg = (a + b) / 2avg ਅਕਲਪਿਕ ਔਸਤ ਦੇ ਬਰਾਬਰ ਹੈਜੇ precondition ਨਹੀਂ ਰਿਹਾ, ਤਾਂ postcondition ਦੀ ਗਾਰੰਟੀ ਲਾਗੂ ਨਹੀਂ ਹੁੰਦੀ। triple ਤੁਹਾਨੂੰ ਇਹ ਸਪਸ਼ਟ ਕਰਨ ਲਈ ਮਜਬੂਰ ਕਰਦੀ ਹੈ।
A postcondition ਦਸਦੀ ਹੈ ਕਿ ਕੋਡ ਚਲਣ ਤੋਂ ਬਾਅਦ ਕੀ ਸੱਚ ਹੋਵੇਗਾ—ਜੇ precondition ਰਿਹਾ। ਚੰਗੀਆਂ postconditions konkreਟ ਅਤੇ ਜਾਂਚਯੋਗ ਹੁੰਦੀਆਂ ਹਨ। “ਰਿਜ਼ਲਟ ਵੈਧ ਹੈ” ਕਹਿਣ ਦੀ ਥਾਂ, ਦੱਸੋ ਕਿ "ਵੈਧ" ਦਾ ਮਤਲਬ ਕੀ ਹੈ: sorted, non-negative, ਬਾਊਂਡ ਵਿੱਚ, ਮੁਖ fields ਛੱਡ ਕੇ ਬਦਲਿਆ ਗਿਆ, ਆਦਿ।
Hoare logic ਛੋਟੇ ਬਿਆਨਾਂ ਤੋਂ ਲੈ ਕੇ ਕਈ ਕਦਮਾਂ ਵਾਲੇ ਕੋਡ ਤੱਕ ਦਲਿਲਾਂ ਨੂੰ ਵਧਾਉਂਦਾ ਹੈ:
x = x + 1 ਤੋਂ ਬਾਅਦ x ਬਾਰੇ ਕੀ ਸੱਚ ਹੈ?ਮਕਸਦ ਇਹ ਨਹੀਂ ਕਿ ਹਰ ਥਾਂ curly braces ਪੈਣਾ ਸ਼ੁਰੂ ਕਰ ਦਿਓ। ਮਕਸਦ ਹੈ ਇਰਾਦਾ ਪਾਠਯੋਗ ਬਣਾਉਣਾ: ਸਪਸ਼ਟ assumptions, ਸਪਸ਼ਟ outcomes, ਅਤੇ ਸਮੀਖਿਆਵਾਂ ਵਿੱਚ "ਇਹ ਚੱਲਦਾ ਹੈ" ਵਾਲੀਆਂ ਗੱਲਾਂ ਘੱਟ।
A ਲੂਪ invariant ਇੱਕ ਬਿਆਨ ਹੈ ਜੋ ਲੂਪ ਸ਼ੁਰੂ ਹੋਣ ਤੋਂ ਪਹਿਲਾਂ ਸੱਚ ਹੋਵੇ, ਹਰ ਇਟਰੈਸ਼ਨ ਦੇ ਬਾਅਦ ਵੀ ਸੱਚ ਰਹੇ, ਅਤੇ ਲੂਪ ਖ਼ਤਮ ਹੋਣ 'ਤੇ ਵੀ ਸੱਚ ਹੋਵੇ। ਇਹ ਇੱਕ ਸਧਾਰਨ ਵਿਚਾਰ ਹੈ ਪਰ ਬਹੁਤ ਮਹੱਤਵਪੂਰਨ ਨਤੀਜੇ ਦਿੰਦਾ: ਇਹ "ਇਹ ਚੱਲਦਾ ਹੈ" ਨੂੰ ਉਹ ਮੁਲਾਂਕਣ ਦਿੰਦਾ ਹੈ ਜੋ ਹਰ ਕਦਮ 'ਤੇ ਜਾਂਚਿਆ ਜਾ ਸਕਦਾ ਹੈ।
ਇਨਵੈਰੀਐਂਟ ਨਾ হলে, ਇੱਕ ਸਮੀਖਿਆ ਅਕਸਰ ਐਸਾ ਸੁਣਾਉਂਦੀ ਹੈ: “ਅਸੀਂ ਲਿਸਟ ਉੱਤੇ ਇਟਰੈਟ ਕਰਦੇ ਹਾਂ ਅਤੇ ਕਦਮ-ਬ-ਕਦਮ ਚੀਜ਼ਾਂ ਠੀਕ ਕਰਦੇ ਹਾਂ।” ਇੱਕ invariant ਤਰਤੀਬ ਨੂੰ ਜ਼ਿਆਦਾ ਸਪਸ਼ਟ ਕਰਦਾ ਹੈ: “ਇਸ ਵੇਲੇ ਕੀ ਠੀਕ ਹੈ।” ਜਦ ਤੁਸੀਂ ਇਹ ਸਾਫ਼ ਦਸ ਦਿੰਦੇ ਹੋ ਤਾਂ off-by-one ਗਲਤੀਆਂ ਅਤੇ ਛੁੱਟ ਗਈਆਂ ਕੇਸਾਂ ਬਾਹਰ ਆ ਜਾਂਦੀਆਂ, ਕਿਉਂਕਿ ਉਹ ਉਨ੍ਹਾਂ ਮੋਹਲਤਾਂ 'ਤੇ invariant ਨੂੰ ਤੌੜ ਦੇਂਦੇ ਹਨ।
ਜ਼ਿਆਦਾਤਰ ਦਿਨ-ਪ੍ਰਤੀਦਿਨ ਕੋਡ ਕੁਝ ਨਿਰਧਾਰਿਤ ਟੈਮਪਲੇਟ ਵਰਤ ਸਕਦਾ ਹੈ।
1) ਬਾਊਂਡ / ਇੰਡੈਕਸ ਸੁਰੱਖਿਆ
0 ≤ i ≤ nlow ≤ left ≤ right ≤ highਇਹ ਕਿਸਮ ਦੇ invariants out-of-range ਐਕਸੈਸ ਰੋਕਣ ਅਤੇ array reasoning ਨੂੰ konkreਟ ਬਣਾਉਣ ਵਿੱਚ ਸ਼ਾਨਦਾਰ ਹਨ।
2) ਪ੍ਰੋਸੈਸਡ vs ਅਨ-ਪਰੋਸੈਸਡ ਆਈਟਮ
result ਵਿੱਚ ਗਇਆ ਉਹ filter predicate ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ।”ਇਸ ਨਾਲ ਅਸਪਸ਼ਟ ਪ੍ਰੋਗਰੈਸ ਨੂੰ ਇਹ ਸਪਸ਼ਟ ਕਾਂਟ੍ਰੈਕਟ ਮਿਲਦਾ ਹੈ ਕਿ “ਕੀ ਕੀਤਾ ਹੋ ਚੁਕਾ ਹੈ।”
3) Sorted prefix (ਜਾਂ partitioned prefix)
a[0..i) sorted ਹੈ।”≤ pivot ਹਨ, ਅਤੇ a[j..n) ਦੇ ਸਾਰੇ ≥ pivot ਹਨ।”ਇੱਥੇ ਤੱਕ ਕਿ ਜਦ پوری array sorted ਨਾ ਹੋਵੇ, ਤੁਸੀਂ ਉਹ ਹਿੱਸਾ ਜੋ sorted/partitioned ਹੈ, ਫਿਕਸ ਕਰ ਸਕਦੇ ਹੋ।
ਸਹੀਤਾ ਸਿਰਫ਼ ਠੀਕ ਹੋਣ ਦੀ ਗੱਲ ਨਹੀਂ—ਲੂਪ ਨੂੰ ਵੀ ਖਤਮ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ। ਇੱਕ ਸਾਦਾ ਤਰੀਕਾ ਇਹ ਦਿਖਾਉਣ ਦਾ ਹੈ ਕਿ ਕੋਈ ਮਾਪ (variant) ਹਰ ਇਟਰੈਸ਼ਨ ਨਾਲ ਘਟ ਰਿਹਾ ਹੈ ਅਤੇ ਲੋੜੀ ਜਾਂਦੀ حد ਤੋਂ ਪਿੱਛੇ ਨਹੀਂ ਜਾ ਸਕਦਾ।
ਉਦਾਹਰਣ:
n - i ਹਰ ਵਾਰੀ 1 ਨਾਲ ਘਟਦਾ ਹੈ।”ਜਦ ਤੁਸੀਂ ਘਟਦਾ ਮਾਪ ਨਹੀਂ ਲੱਭ ਪਾਂਦੇ, ਇਹ ਇੱਕ ਅਸਲੀ ਜੋਖਮ ਦਾ ਇਸ਼ਾਰਾ ਹੋ ਸਕਦਾ ਹੈ: ਕੁਝ ਇਨਪੁਟਾਂ 'ਤੇ ਅਨੰਤ ਲੂਪ।
Quicksort ਦਾ ਸਪੱਸ਼ਟ ਵਾਅਦਾ ਹੈ: ਦਿੱਤੇ ਗਏ slice (ਜਾਂ array segment) ਨੂੰ ਇਸ ਤਰੀਕੇ ਨਾਲ ਰੀਅਰੇਂਜ ਕਰੋ ਕਿ ਉਹ non-decreasing ਕ੍ਰਮ ਵਿੱਚ ਆ ਜਾਵੇ, ਬਿਨਾਂ ਕਿਸੇ ਤੱਤ ਨੂੰ ਖੋਏ ਜਾਂ ਨਵਾਂ ਬਣਾਏ। ਅਲਗੋਰਿਦਮ ਦੀ ਉੱਚ-ਸਤਹੀ ਰੂਪ ਇਹ ਹੈ:
equal ਲਈ ਵੀ)।ਇਹ ਸਿੱਖਣ ਲਈ ਵਧੀਆ ਮਿਸਾਲ ਹੈ ਕਿਉਂਕਿ ਇਹ ਦਿਮਾਗ ਵਿੱਚ ਰੱਖਣ ਲਈ ਛੋਟਾ ਹੈ, ਪਰ ਬਹੁਤ ਕੁਝ ਦਿਖਾਉਂਦਾ ਹੈ ਜਿੱਥੇ ਅਨਉਪਚਾਰਿਕ reasoning ਫੇਲ ਹੁੰਦੀ ਹੈ। ਕਈ ਵਾਰੀ Quicksort ਜੋ "ਕੁਝ ਟੈਸਟਾਂ 'ਤੇ ਚੰਗਾ ਲੱਗਦਾ" ਉਹ ਵਿਸ਼ੇਸ਼ ਇਨਪੁਟਾਂ ਜਾਂ ਸੀਮਾਵਾਂ 'ਤੇ ਗਲਤ ਹੋ ਸਕਦਾ ਹੈ।
ਕੁਝ ਮੁੱਦੇ ਸਭ ਤੋਂ ਜ਼ਿਆਦਾ ਬੱਗ ਪੈਦਾ ਕਰਦੇ ਹਨ:
equal to pivot ਨੂੰ inconsistent ਤਰੀਕੇ ਨਾਲ ਸਾਂਭਦਾ ਹੈ ਤਾਂ ਤੁਹਾਨੂੰ ਅਨੰਤ ਰਿਕਰਜ਼ਨ ਮਿਲ ਸਕਦੀ ਹੈ (subranges ਘਟਦੀਆਂ ਨਹੀਂ) ਜਾਂ partition ਆਪਣਾ ਨਿਯਮ ਤੋੜ ਸਕਦੀ ਹੈ।Hoare-ਸਟਾਈਲ ਤਰੀਕੇ ਨਾਲ correctness ਦੀ ਦਲੀਲ ਆਮ ਤੌਰ 'ਤੇ ਦੋ ਹਿੱਸਿਆਂ ਵਿੱਚ ਵੰਡਿਆ ਜਾਂਦਾ ਹੈ:
ਇਹ ਵੰਡ reasoning ਨੂੰ ਮੈਨੇਜਬਲ ਰੱਖਦੀ ਹੈ: partition ਨੂੰ ਸਹੀ ਬਣਾਓ, ਫਿਰ sorting ਦੀ correctness ਉਸਦੇ ਉੱਪਰ ਬਣਾਓ।
Quicksort ਦੀ ਤੇਜ਼ੀ ਇੱਕ ਧੋਖੇਬਾਜ਼ ਤੌਰ 'ਤੇ ਛੋਟੀ ਰੁਟੀਨ 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ: partition। ਜੇ partition ਥੋੜ੍ਹ੍ਹੀ ਵੀ ਗਲਤ ਹੋਵੇ, Quicksort ਗਲਤ sort ਕਰ ਸਕਦਾ ਹੈ, ਸਦਾ ਲਈ ਚੱਲ ਸਕਦਾ ਹੈ, ਜਾਂ edge cases 'ਤੇ crash ਕਰ ਸਕਦਾ ਹੈ।
ਅਸੀਂ ਧਾਰਮਿਕ Hoare partition scheme ਵਰਤਾਂਗੇ (ਦੋ pointers ਅੰਦਰ ਵੱਲ ਵਧਦੇ ਹਨ)।
Input: ਇੱਕ array slice A[lo..hi] ਅਤੇ ਇੱਕ ਚੁਣਿਆ ਹੋਇਆ pivot value (ਅਕਸਰ A[lo]).
Output: ਇੱਕ index p ਜਿਸ ਨਾਲ:
A[lo..p] ਵਿੱਚ ਹਰ ਤੱਤ ≤ pivot ਹੈA[p+1..hi] ਵਿੱਚ ਹਰ ਤੱਤ ≥ pivot ਹੈਨੋਟ ਕਰੋ ਕਿ ਕੀ ਨਹੀਂ ਵਾਅਦਾ ਕੀਤਾ ਗਿਆ: pivot ਜ਼ਰੂਰੀ ਨਹੀਂ ਕਿ position p 'ਤੇ ਆਵੇ, ਅਤੇ pivot ਦੇ ਬਰਾਬਰ ਵਾਲੇ ਤੱਤ ਦੋਨਾਂ ਪਾਸਿਆਂ ਆ ਸਕਦੇ ਹਨ। ਠੀਕ partition ਹੀ Quicksort ਲਈ ਲਾਜ਼ਮੀ ਹੈ।
ਜਦ algorithm ਦੋ indices—i ਖੱਬੇ ਤੋਂ ਅਤੇ j ਸੱਜੇ ਤੋਂ—ਅੱਗੇ ਵਧਾਉਂਦਾ ਹੈ, ਚੰਗੀ reasoning ਇਸ ਬਾਤ 'ਤੇ ਦਿਓ ਧਿਆਨ ਦਿੰਦੀ ਹੈ ਕਿ ਕੀ “ਲੌਕ ਇਨ” ਹੋ ਚੁੱਕਿਆ ਹੈ। ਇੱਕ ਪ੍ਰਯੋਗੀ invariants ਦਾ ਸਮੂਹ ਹੈ:
A[lo..i-1] ਦੇ ਸਾਰੇ ਕੋਸ਼ਿਕਾਵਾਂ ≤ pivot ਹਨ (ਖੱਬਾ ਪਾਸਾ ਸਾਫ਼)A[j+1..hi] ਦੇ ਸਾਰੇ ਕੋਸ਼ਿਕਾਵਾਂ ≥ pivot ਹਨ (ਸੱਜਾ ਪਾਸਾ ਸਾਫ਼)A[i..j] ਵਿੱਚ ਸਾਰੀਆਂ ਚੀਜ਼ਾਂ ਅਣ-ਸ਼੍ਰੇਣੀਬੱਧ ਹਨ (ਹਾਲੇ ਜਾਂਚਣ ਵਾਲੀਆਂ)ਜਦੋਂ ਅਸੀਂ A[i] > pivot ਅਤੇ A[j] < pivot ਲੱਭਦੇ ਹਾਂ, ਤਾਂ ਉਹਨਾਂ ਨੂੰ swap ਕਰਨਾ invariants ਨੂੰ ਬਰਕਰਾਰ ਰੱਖਦਾ ਹੈ ਅਤੇ ਅਣ-ਸ਼੍ਰੇਣੀਬੱਧ ਵਿਚਕਾਰੂ ਹਿੱਸਾ ਘਟਾਉਂਦਾ ਹੈ।
i ਸੱਜੇ ਵੱਲ ਦੌੜਦਾ ਹੈ; partition ਨੂੰ ਫਿਰ ਵੀ terminate ਕਰਨਾ ਅਤੇ ਇਕ ਸੰਦੂਕ p ਵਾਪਸ ਦੇਣਾ ਚਾਹੀਦਾ ਹੈ।j ਖੱਬੇ ਵੱਲ ਦੌੜਦਾ ਹੈ; termination ਦਾ ਇੱਕੋ ਹੀ ਅਲੋਚਨਾ।< ਵਿਰੁੱਧ ≤) ਹਨ, pointers stuck ਹੋ ਸਕਦੇ ਹਨ। Hoare ਦੀ ਯੋਜਨਾ ਇੱਕ consistent rule 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ ਤਾਂ ਕਿ ਪ੍ਰਗਤੀ ਜਾਰੀ ਰਹੇ।ਵੱਖ-ਵੱਖ partition ਸਕੀਮਾਂ (Lomuto, Hoare, three-way) ਮੌਜੂਦ ਹਨ। ਜ਼ਰੂਰੀ ਗੱਲ ਇਹ ਹੈ ਕਿ ਇੱਕ ਚੁਣੋ, ਉਸਦਾ contract ਸਪਸ਼ਟ ਕਰੋ, ਅਤੇ ਸਮੀਖਿਆ ਇਸੇ contract ਦੇ ਖਿਲਾਫ਼ ਕਰੋ।
ਰਿਕਰਸ਼ਨ ਨੂੰ ਭਰੋਸੇਯੋਗ ਸਮਝਣਾ ਸਭ ਤੋਂ ਆਸਾਨ ਹੈ ਜਦ ਤੁਸੀਂ ਦੋ ਸਵਾਲਾਂ ਦਾ ਸਪਸ਼ਟ ਜਵਾਬ ਦੇ ਸਕੋ: ਇਹ ਕਦੋਂ ਰੁਕੇਗੀ? ਅਤੇ ਹਰ ਕਦਮ ਕਿਉਂ ਸਹੀ ਹੈ? Hoare-ਸਟਾਈਲ ਸੋਚ ਮਦਦ ਕਰਦੀ ਹੈ ਕਿਉਂਕਿ ਇਹ ਤੁਹਾਨੂੰ ਜ਼ੋਰ ਦਿੰਦੀ ਹੈ ਕਿ ਤੁਸੀਂ ਦੱਸੋ ਕਿ ਕਾਲ ਤੋਂ ਪਹਿਲਾਂ ਕੀ ਸੱਚ ਹੈ ਅਤੇ ਵਾਪਸੀ 'ਤੇ ਕੀ ਸੱਚ ਹੋਵੇਗਾ।
ਇੱਕ recursive ਫੰਕਸ਼ਨ ਨੂੰ ਘੱਟੋ-ਘੱਟ ਇੱਕ base case ਚਾਹੀਦਾ ਹੈ ਜਿੱਥੇ ਇਹ ਹੋਰ recursive ਕਾਲ ਨਹੀਂ ਕਰਦਾ ਅਤੇ ਫਿਰ ਵੀ ਵਾਅਦਾ ਪੂਰਾ ਕਰਦਾ ਹੈ।
Sorting ਲਈ ਆਮ base case ਹੈ “length 0 ਜਾਂ 1 ਵਾਲੀਆਂ arrays ਪਹਿਲਾਂ ਹੀ sorted ਹਨ।” ਇੱਥੇ "sorted" ਨੂੰ ਸਪਸ਼ਟ ਰੱਖੋ: ਇੱਕ ਅਰਡਰਿੰਗ ਸੰਬੰਧ ≤ ਲਈ, output array sorted ਹੈ ਜੇ ਹਰ index i < j ਲਈ a[i] ≤ a[j]। (ਕਿਆ equal ਤੱਤ ਆਪਣੀ original order ਰੱਖਦੇ ਹਨ ਇਹ stability ਦੀ ਵਿਸ਼ੇਸਤਾ ਹੈ; Quicksort ਆਮ ਤੌਰ 'ਤੇ stable ਨਹੀਂ ਹੁੰਦਾ ਜੇ ਤਿਆਰ ਨਹੀਂ ਕੀਤਾ)।
ਹਰ recursive ਕਦਮ ਨੂੰ ਆਪਣੇ ਆਪ 'ਤੇ ਇਕ ਕਠੋਰ ਛੋਟਾ input ਚਾਹੀਦਾ ਹੈ। ਇਹ "shrinking" termination ਦਾ ਦਲੀਲ ਹੈ: ਜੇ ਸਾਈਜ਼ ਘਟਦੀ ਹੈ ਅਤੇ 0 ਤੋਂ ਘੱਟ ਨਹੀਂ ਹੋ ਸਕਦੀ, ਤਾਂ ਤੁਸੀਂ ਅਨੰਤ ਤਕ recurse ਨਹੀਂ ਕਰ ਸਕਦੇ।
ਛੋਟਾ ਹੋਣਾ স্টੈਕ ਸੁਰੱਖਿਆ ਲਈ ਵੀ ਜਰੂਰੀ ਹੈ। ਸਹੀ ਕੋਡ ਵੀ crash ਕਰ ਸਕਦਾ ਹੈ ਜੇ recursion depth ਬਹੁਤ ਵੱਧ ਜਾਵੇ। Quicksort ਵਿੱਚ, unbalanced partitions ਗਹਿਰੇ recursion ਪੈਦਾ ਕਰ ਸਕਦੇ ਹਨ। ਇਹ termination-proofs ਦੇ ਨਾਲ-ਨਾਲ ਇੱਕ ਪ੍ਰਯੋਗੀ ਯਾਦ ਦਿਵਾਉਂਦਾ ਹੈ ਕਿ worst-case depth 'ਤੇ ਵਿਚਾਰ ਕਰੋ।
Quicksort ਦਾ worst-case ਸਮਾਂ O(n²) ਤੱਕ ਘਟ ਸਕਦਾ ਹੈ ਜਦ partitions ਬਹੁਤ unbalanced हों, ਪਰ ਇਹ performance ਦਾ ਮਸਲਾ ਹੈ—ਕੋਡ ਦੀ ਸਹੀਤਾ ਫੇਲ੍ਹ ਨਹੀਂ। reasoning ਦਾ ਉਦੇਸ਼ ਹੈ: ਜੇ partition ਤੱਤ ਰੱਖਦਾ ਹੈ ਅਤੇ pivot ਅਨੁਸਾਰ ਉਨ੍ਹਾਂ ਨੂੰ ਵੇਖ ਕੇ ਵੰਡਦਾ ਹੈ, ਤਾਂ subranges ਦੀ recursive sorting ਨਾਲ ਪੂਰਾ ਰੇਂਜ sorted ਨਿਕਲਦਾ ਹੈ।
ਟੈਸਟਿੰਗ ਅਤੇ ਸਬੂਤ-ਸਟਾਈਲ reasoning ਦਾ ਮਕਸਦ ਇੱਕੋ ਹੀ ਹੈ—ਭਰੋਸਾ ਪ੍ਰਾਪਤ ਕਰਨਾ—ਪਰ ਉਹ ਵੱਖ-ਵੱਖ ਤਰੀਕਿਆਂ ਨਾਲ ਕਰਦੇ ਹਨ।
ਟੈਸਟਾਂ ਠੋਸ ਗਲਤੀਆਂ ਫੜਦੀਆਂ ਹਨ: off-by-one, ਛੁੱਟੇ ਕੇਸ, ਰਿਗ੍ਰੈਸ਼ਨ। ਪਰ ਟੈਸਟ ਸਿਰਫ ਇਨਪੁਟ ਸਪੇਸ ਨੂੰ ਸੈਂਪਲ ਕਰ ਸਕਦੇ ਹਨ। “100% coverage” ਦਾ ਅਰਥ ਹਰwerks ਰੂਪ ਵਿੱਚ “ਸਭ ਵਿਹੈਵਿਅਰ ਚੈਕ ਕੀਤੇ” ਨਹੀਂ ਹੁੰਦਾ; ਜ਼ਿਆਦਾਤਰ ਮਤਲਬ “ਸਭ ਲਾਈਨਾਂ ਚਲੀਆਂ।”
ਸਬੂਤ-ਸਟਾਈਲ ਸੋਚ (ਖ਼ਾਸ ਕਰਕੇ Hoare-ਸਟਾਈਲ reasoning) ਇੱਕ spec ਤੋਂ ਸ਼ੁਰੂ ਹੁੰਦੀ ਹੈ ਅਤੇ ਪੁੱਛਦੀ ਹੈ: ਜੇ ਇਹ preconditions ਸਹੀ ਹਨ, ਕੀ ਕੋਡ ਹਮੇਸ਼ਾਂ postconditions ਸਥਾਪਤ ਕਰੇਗਾ? ਜਦ ਤੁਸੀਂ ਇਹ ਚੰਗੀ ਤਰ੍ਹਾਂ ਕਰਦੇ ਹੋ, ਤਾਂ ਤੁਸੀਂ ਇਕ ਨਾ ਸਿਰਫ਼ ਇੱਕ ਬੱਗ ਲੱਭਦੇ ਹੋ—ਤੁਸੀਂ ਆਮਤੌਰ 'ਤੇ ਬੱਗਾਂ ਦੀ ਇੱਕ ਪੂਰੀ ਸ਼੍ਰੇਣੀ ਨੂੰ ਖਤਮ ਕਰ ਸਕਦੇ ਹੋ (ਜਿਵੇਂ "array access bounds ਵਿੱਚ ਰਹਿੰਦਾ ਹੈ" ਜਾਂ "ਲੂਪ partition property ਤੋੜਦਾ ਨਹੀਂ").
ਇੱਕ ਸਪਸ਼ਟ spec ਇੱਕ ਟੈਸਟ ਜਣਰੇਟਰ ਹੈ।
ਜੇ ਤੁਹਾਡੀ postcondition ਕਹਿੰਦੀ ਹੈ “ਆਉਟਪੁੱਟ sorted ਹੈ ਅਤੇ input ਦਾ permutation ਹੈ”, ਤਾਂ ਤੁਸੀਂ ਫੌਰاً ਟੈਸਟ ਵਿਚਾਰ ਪ੍ਰਾਪਤ ਕਰ ਲੈਂਦੇ ਹੋ:
Spec ਦੱਸਦਾ ਹੈ ਕਿ "ਸਹੀ" ਕੀ ਹੈ, ਅਤੇ ਟੈਸਟ ਇਹ ਚੈੱਕ ਕਰਦੇ ਹਨ ਕਿ ਹਕੀਕਤ ਉਸਦੇ ਨਾਲ ਮਿਲਦੀ ਹੈ।
Property-based testing ਸਬੂਤ ਅਤੇ ਉਦਾਹਰਣਾਂ ਦੇ ਵਿਚਕਾਰ ਪੱਖ ਹੀ। ਹੱਥ ਨਾਲ ਕੁਝ ਕੇਸ ਚੁਣਣ ਦੀ ਥਾਂ, ਤੁਸੀਂ ਗੁਣ ਦਰਜ ਕਰਦੇ ਹੋ ਅਤੇ ਇੱਕ ਟੂਲ ਬਹੁਤ ਸਾਰੇ ਇਨਪੁਟ ਜਣਰੇਟ ਕਰਦਾ ਹੈ।
Sorting ਲਈ ਦੋ ਸਧਾਰਨ ਗੁਣ ਲੰਬਾ ਫਾਇਦਾ ਦਿੰਦੇ ਹਨ:
ਇਹ ਗੁਣ ਅਸਲ ਵਿੱਚ postconditions ਦੇ ਐਕਜ਼ੈਕਯੂਟਬਲ ਚੈਕ ਹਨ।
ਇਕ ਹਲਕਾ ਰੂਪ ਜੋ ਵਧਦਾ ਹੈ:
ਜੇ ਤੁਸੀਂ ਇਸਨੂੰ ਸੰਸਥਾਗਤ ਕਰਨਾ ਚਾਹੁੰਦੇ ਹੋ, ਤਾਂ “spec + reasoning notes + tests” ਨੂੰ ਆਪਣੇ PR ਟੈਂਪਲੇਟ ਜਾਂ ਕੋਡ-ਰੀਵਿਊ ਚੈਕਲਿਸਟ ਦਾ ਹਿੱਸਾ ਬਣਾਓ।
ਜੇ ਤੁਸੀਂ chat- ਆਧਾਰਿਤ ਕੋਡ ਜਨਰੇਸ਼ਨ ਵਰਕਫਲੋ ਵਰਤ ਰਹੇ ਹੋ, ਉਹੀ ਅਨੁਸ਼ਾਸਨ ਲਾਗੂ ਹੁੰਦਾ—ਸ਼ਾਇਦ ਹੋਰ ਵੀ ਜ਼ਰੂਰੀ। Koder.ai ਜਿਵੇਂ ਟੂਲਾਂ ਵਿੱਚ ਤੁਸੀਂ Planning Mode ਵਿੱਚ preconditions/postconditions ਪਿਨ ਕਰ ਸਕਦੇ ਹੋ ਪਹਿਲਾਂ, ਫਿਰ property-based ਟੈਸਟਾਂ ਜੋੜ ਸਕਦੇ ਹੋ। ਟੂਲ implementation ਤੇਜ਼ ਕਰਦਾ ਹੈ, ਪਰ spec ਹੀ ਇਹ ਦਿਖਾਉਂਦੀ ਹੈ ਕਿ “ਤੇਜ਼” ਕਦੋਂ “ਨਾਜੁਕ” ਵਿੱਚ ਨਹੀਂ ਬਦਲਣਾ।
ਸਹੀਤਾ ਸਿਰਫ਼ "ਕੋਡ ਸਹੀ ਮੁੱਲ ਲਿਆਉਂਦਾ" ਨਹੀਂ ਹੈ। ਸੁਰੱਖਿਆ ਸੋਚ ਇੱਕ ਵੱਖਰਾ ਸਵਾਲ ਪੁੱਛਦੀ ਹੈ: ਕਿਹੜੇ ਨਤੀਜੇ ਅਸਵੀਕਾਰਣੀਯ ਹਨ, ਅਤੇ ਅਸੀਂ ਉਨ੍ਹਾਂ ਨੂੰ ਕਿਵੇਂ ਰੋਕੀਏ—ਭਾਵੇਂ ਕੋਡ ਟੁੱਟ ਜਾਏ, ਨਾਜ਼ੁਕ ਤਰੀਕੇ ਨਾਲ ਵਰਤਿਆ ਜਾਵੇ, ਜਾਂ ਅਧੂਰਾ ਫੇਲ੍ਹ ਹੋਵੇ? ਅਮਲੀ ਤੌਰ 'ਤੇ, ਸੁਰੱਖਿਆ ਸਹੀਤਾ ਨਾਲ ਇੱਕ ਪ੍ਰਾਥਮਿਕਤਾ ਤਰਤੀਬ ਹੈ: ਕੁਝ ਫੇਲ੍ਹਿੰਗਸ ਫਿਕਰਤ (annoying) ਹੋ ਸਕਦੇ ਹਨ, ਹੋਰ ਵਿੱਤੀ ਨੁਕਸਾਨ, ਨਿੱਜਤਾ ਉਲੰਘਣਾ, ਜਾਂ ਸਰੀਰਕ ਨੁਕਸਾਨ ਪੈਦਾ ਕਰ ਸਕਦੇ ਹਨ।
ਇੱਕ bug ਕੋਡ ਜਾਂ ਡਿਜ਼ਾਇਨ ਵਿੱਚ ਦੋਸ਼ ਹੈ। ਇੱਕ hazard ਉਹ ਸਥਿਤੀ ਹੈ ਜੋ ਅਸਵੀਕਾਰਣੀਯ ਨਤੀਜੇ ਵੱਲ ਲੈ ਜਾ ਸਕਦੀ ਹੈ। ਇਕ bug ਇੱਕ ਸੰਦਰਭ ਵਿੱਚ ਨਿਰਦੋਸ਼ ਹੋ ਸਕਦਾ ਹੈ ਅਤੇ ਦੂਜੇ ਵਿੱਚ ਖਤਰਨਾਕ।
ਉਦਾਹਰਣ: ਫ਼ੋਟੋ ਗੈਲਰੀ ਵਿੱਚ off-by-one ਇੱਕ ਚਿੱਤਰ ਨੂੰ ਗਲਤ ਲੇਬਲ ਕਰ ਸਕਦਾ; ਉਸੇ ਗਲਤੀ ਦਾ ਦਵਾਈ ਦੀ ਮਾਤਰਾ ਗਣਨਾ ਵਿੱਚ ਹੋਣਾ ਮਰੀਜ਼ ਨੂੰ ਨੁਕਸਾਨ ਪਹੁੰਚਾ ਸਕਦਾ। ਸੁਰੱਖਿਆ ਸੋਚ ਤੁਹਾਨੂੰ ਕੋਡ ਦੇ ਬਿਹੇਵਿਅਰ ਨੂੰ ਨਤੀਜਿਆਂ ਨਾਲ ਜੋੜਨ 'ਤੇ ਮਜ਼ਬੂਰ ਕਰਦੀ ਹੈ—ਸਿਰਫ spec ਦਾ ਪਾਲਣ ਹੀ ਕਾਫ਼ੀ ਨਹੀਂ।
ਭਾਰੀ ਫਾਰਮਲ ਮੈਥਡਾਂ ਦੀ ਲੋੜ ਨਹੀਂ; ਛੋਟੀ, ਦੋਹਰਾਏ ਜਾਣ ਵਾਲੀਆਂ ਪ੍ਰਥਾਵਾਂ ਤੁਰੰਤ ਫਾਇਦਾ ਦੇ ਸਕਦੀਆਂ ਹਨ:
ਇਹ ਤਕਨੀਆਂ Hoare-ਸਟਾਈਲ reasoning ਨਾਲ ਕੁਦਰਤੀ ਤੌਰ 'ਤੇ ਮਿਲਦੀਆਂ ਹਨ: ਤੁਸੀਂ preconditions ਸਪਸ਼ਟ ਕਰਦੇ ਹੋ (ਕਿਹੜੇ input ਮਨਜ਼ੂਰ ਹਨ) ਅਤੇ postconditions ਵਿਚ safety ਗੁਣ ਸ਼ਾਮਲ ਕਰੋ (ਕਿਹੜੀਆਂ ਚੀਜ਼ਾਂ ਕਦੇ ਵੀ ਨਹੀਂ ਹੋਣੇ ਚਾਹੀਦੀਆਂ)।
ਸੁਰੱਖਿਆ-ਉਪਯੋਗ ਚੈੱਕਾਂ ਦੀ ਕੀਮਤ ਹੁੰਦੀ ਹੈ—CPU ਸਮਾਂ, ਜਟਿਲਤਾ, ਜਾਂ ਕਈ ਵਾਰ ਗਲਤ ਓਡੀਆਂ।
ਸੁਰੱਖਿਆ ਸੋਚ ਸੁੰਦਰਤਾ ਨੂੰ ਸਾਬਤ ਕਰਨ ਦੀ ਨਿਗਾਹ ਨਹੀਂ ਰੱਖਦੀ; ਇਹ ਉਹਨਾਂ ਫੇਲ-ਮੋਡਾਂ ਨੂੰ ਰੋਕਦੀ ਹੈ ਜੋ ਤੁਸੀਂ ਬਰਦਾਸ਼ਤ ਨਹੀਂ ਕਰ ਸਕਦੇ।
ਕੋਡ ਰਿਵਿਊਜ਼ ਉਹ ਥਾਂ ਹਨ ਜਿੱਥੇ correctness ਸੋਚ ਸਭ ਤੋਂ ਤੇਜ਼ ਨਤੀਜੇ ਦਿੰਦੀ ਹੈ, ਕਿਉਂਕਿ ਤੁਸੀਂ missing assumptions ਨੂੰ ਪ੍ਰੋਡਕਸ਼ਨ ਤੱਕ ਪਹੁੰਚਣ ਤੋਂ ਪਹਿਲਾਂ ਪਛਾਣ ਸਕਦੇ ਹੋ। Hoare ਦਾ ਮੁੱਖ ਇੰਤਜਾਮ—"ਕੀ ਸਚ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ ਪਹਿਲਾਂ" ਅਤੇ "ਕੀ ਗਾਰੰਟੀ ਕੀਤੀ ਜਾਂਦੀ ਹੈ ਬਾਅਦ"—ਸਮੀਖਿਆ ਪ੍ਰਸ਼ਨਾਂ ਵਿੱਚ ਆਸਾਨੀ ਨਾਲ ਬਦਲ ਜਾਂਦਾ ਹੈ।
ਜਦ ਤੁਸੀਂ ਕੋਈ ਬਦਲਾਅ ਪੜ੍ਹਦੇ ਹੋ, ਹਰ ਮੁੱਖ ਫੰਕਸ਼ਨ ਨੂੰ ਇੱਕ ਛੋਟੀ promise ਵਜੋਂ ਫਰੇਮ ਕਰੋ:
ਇੱਕ ਸਾਦਾ reviewer ਆਦਤ: ਜੇ ਤੁਸੀਂ pre/post conditions ਇੱਕ ਵਾਕ ਵਿੱਚ ਨਹੀਂ ਦੱਸ ਸਕਦੇ, ਤਾਂ ਕੋਡ ਨੂੰ ਸ਼ਾਇਦ ਸਪਸ਼ਟ ਬਣਾਉਣ ਦੀ ਲੋੜ ਹੈ।
ਖ਼ਤਰਨਾਕ ਜਾਂ ਕੇਂਦਰੀ ਫੰਕਸ਼ਨਾਂ ਲਈ, signature ਦੇ ਉਪਰ ਇੱਕ ਛੋਟਾ contract comment ਜੋੜੋ। ਸਪਸ਼ਟ ਅਤੇ konkreਟ ਰੱਖੋ: ਇਨਪੁਟ, ਆਉਟਪੁੱਟ, ਸਾਈਡ-ਇਫੈਕਟ, ਅਤੇ ਗਲਤੀਆਂ।
def withdraw(account, amount):
"""Contract:
Pre: amount is an integer > 0; account is active.
Post (success): returns new_balance; account.balance decreased by amount.
Post (failure): raises InsufficientFunds; account.balance unchanged.
"""
...
ਇਹ comments ਫਾਰਮਲ ਸਬੂਤ ਨਹੀਂ ਹਨ, ਪਰ ਉਹ reviewers ਨੂੰ ਕੁਝ ਸਪਸ਼ਟ ਦੇਖਣ ਲਈ ਦਿੰਦੇ ਹਨ।
ਜਦ ਤੁਸੀਂ ਹੇਠਾਂ ਦਿੱਤੀਆਂ ਚੀਜ਼ਾਂ ਦੇ ਨਾਲ ਸੌਦਾ ਕਰ ਰਹੇ ਹੋ ਤਾਂ ਵਧੇਰੇ ਸਪਸ਼ਟ ਹੋਵੋ:
ਜੇ ਬਦਲਾਅ ਕਿਸੇ ਵੀ ਇਸ ਵਿੱਚ ਛੂਹਦਾ ਹੈ, ਪੁੱਛੋ: “preconditions ਕਿੱਥੇ enforce ਕੀਤੀਆਂ ਜਾਣਗੀਆਂ?” ਅਤੇ “ਫੇਲ੍ਹ ਹੋਣ 'ਤੇ ਅਸੀਂ ਕੀ ਗਾਰੰਟੀ ਦਿੰਦੇ ਹਾਂ?”
Formal reasoning ਦਾ ਮਤਲਬ ਇਹ ਨਹੀਂ ਕਿ ਤੁਸੀਂ ਪੂਰੇ ਕੋਡਬੇਸ ਨੂੰ ਗਣਿਤੀ ਕਾਗਜ਼ ਬਣਾਉ। ਉਦੇਸ਼ ਉਨ੍ਹਾਂ ਹਿਸਿਆਂ 'ਤੇ ਵਧੇਰੀ ਨਿਸ਼ਚਿਤਤਾ ਲਗਾਉਣਾ ਹੈ ਜਿੱਥੇ “ਟੈਸਟਾਂ ਵਿੱਚ ਠੀਕ ਲੱਗਣਾ” ਕਾਫ਼ੀ ਨਹੀਂ।
ਉਹ ਛੋਟੇ, ਨਿਰਧਾਰਿਤ ਮਾਡਿਊਲਾਂ ਲਈ ਵਧੀਆ ਹਨ ਜਿਨ੍ਹਾਂ 'ਤੇ ਹੋਰ ਸਭ ਕੁਝ ਨਿਰਭਰ ਕਰਦਾ ਹੈ (auth, payment rules, permissions, safety interlocks), ਜਾਂ ਓਹ ਜਟਿਲ algorithms ਜਿੱਥੇ off-by-one ਗਲਤੀਆਂ ਮਹੀਨਿਆਂ ਤੱਕ ਲੁਕ ਸਕਦੀਆਂ ਹਨ (parsers, schedulers, caching/eviction, concurrency primitives, partition-style code, boundary-heavy data transforms).
ਇੱਕ ਉਪਯੋਗੀ ਨਿਯਮ: ਜੇ ਇੱਕ bug حقیقی ਨੁਕਸਾਨ, ਵੱਡਾ ਮਾਲی ਨੁਕਸਾਨ, ਜਾਂ ਚੁੱਪਚਾਪ ਡੇਟਾ ਕ੍ਰਪਸ਼ਨ ਕਰ ਸਕਦੀ ਹੈ, ਤਾਂ ਤੁਹਾਨੂੰ ਸਧਾਰਨ review+tests ਤੋਂ ਵੱਧ ਚਾਹੀਦਾ ਹੈ।
ਤੁਸੀਂ "ਹਲਕਾ" ਤੋਂ "ਭਾਰੀ" ਤੱਕ ਚੁਣ ਸਕਦੇ ਹੋ, ਅਤੇ ਅਕਸਰ ਸਭ ਤੋਂ ਅchha ਨਤੀਜੇ ਮਿਲਦੇ ਹਨ ਜਦ ਤੁਸੀਂ ਉਨ੍ਹਾਂ ਨੂੰ ਮਿਲਾ ਕੇ ਵਰਤਦੇ ਹੋ:
ਫਾਰਮਲਤਾ ਦੀ ਡਿਗਰੀ ਤੈਅ ਕਰੋ risk × cost ਦੇ ਆਧਾਰ 'ਤੇ:
ਅਮਲੀ ਤੌਰ 'ਤੇ, ਤੁਸੀਂ “formalness” ਨੂੰ ਕ੍ਰਮਵੱਧੀ ਰੂਪ ਵਿੱਚ ਜੋੜ ਸਕਦੇ ਹੋ: explicit contracts ਅਤੇ invariants ਨਾਲ ਸ਼ੁਰੂ ਕਰੋ, ਫਿਰ automation ਨਾਲ ਨਿਗਰਾਨੀ ਜਾਰੀ ਰੱਖੋ।
ਇਸਨੂੰ planning ਜਾਂ ਕੋਡ ਰਿਵਿਊ ਵਿੱਚ “ਆਪਾਂ ਹੋਰ formal ਹੋਈਏ?” ਲਈ ਇੱਕ gate ਵਜੋਂ ਵਰਤੋ:
ਅੱਗੇ ਪੜ੍ਹਨ ਲਈ: design-by-contract, property-based testing, model checking for state machines, static analyzers for your language, ਅਤੇ ਸਭੂਤ-ਸੰਬੰਧੀ ਸੰਦਾਂ ਦੀ ਪ੍ਰਾਰੰਭਿਕ ਸਮੱਗਰੀ।
ਸਹੀਤਾ ਦਾ مطلب ਹੈ ਕਿ ਪਰੋਗਰਾਮ ਇੱਕ ਮੰਨੀ ਹੋਈ ਵਿਵਰਣ (specification) ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ: ਹਰ ਮਨਜ਼ੂਰ ਸ਼ੁਦਾ ਇੰਪੁਟ ਅਤੇ ਸੰਬੰਧਿਤ ਸਿਸਟਮ ਸਥਿਤੀ ਲਈ, ਇਹ ਲੋੜੀਂਦੇ ਨਤੀਜੇ ਅਤੇ ਸਾਈਡ-ਇਫੈਕਟ ਦਿੰਦਾ ਹੈ ਅਤੇ ਗਲਤੀਆਂ ਨੂੰ ਵਾਇਦੇ ਅਨੁਸਾਰ ਹੈਂਡਲ ਕਰਦਾ ਹੈ। “ਇਹ ਵਰਕ ਕਰਦਾ ਹੈ” ਆਮ ਤੌਰ 'ਤੇ ਇਸਦਾ ਅਰਥ ਹੈ ਕਿ ਤੁਸੀਂ ਸਿਰਫ ਕੁਝ ਉਦਾਹਰਣਾਂ ਦੀ ਜਾਂਚ ਕੀਤੀ—ਸਾਰਾ ਇਨਪੁਟ ਸਪੇਸ ਜਾਂ ਕਠਿਨ ਬਾਰਡਰ ਕੇਸ ਨਹੀਂ।
Requirements ਵਪਾਰਕ ਲੋੜ ਹਨ (ਜਿਵੇਂ “ਲਿਸਟ ਨੂੰ ਦਿਖਾਉਣ ਲਈ sort ਕਰੋ”). Specification ਉਹ ਸਹੀ, ਜਾਂਚਯੋਗ ਵਿਆਖਿਆ ਹੈ (ਜਿਵੇਂ “ਨਵੀਂ ਲਿਸਟ ਵਾਪਸ ਕਰਦਾ ਹੈ ਜੋ ਚੜ੍ਹਦੇ ਕ੍ਰਮ ਵਿੱਚ sorted ਹੈ, ਉਹੀ ਤੱਤ ਰੱਖਦੀ ਹੈ, ਅਤੇ ਮੁੱਖ ਇਨਪੁਟ ਬਦਲਿਆ ਨਹੀਂ ਗਿਆ”). Implementation ਉਹ ਕੋਡ ਹੈ ਜੋ ਤੁਸੀਂ ਲਿਖਦੇ ਹੋ। ਬਗ ਆਮ ਤੌਰ 'ਤੇ ਉਦੋਂ ਹੁੰਦੇ ਹਨ ਜਦ ਟੀਮ requirements ਤੋਂ ਸਿੱਧਾ implementation ਤੇ ਛਾਲ ਮਾਰ ਦੇਂਦੀ ਹੈ ਬਿਨਾਂ ਵਿਵਰਣ ਨੂੰ ਲਿਖੇ।
Partial correctness ਦਾ ਮਤਲਬ: ਜੇ ਕੋਡ ਵਾਪਸ ਆ ਰਿਹਾ ਹੈ ਤਾਂ ਨਤੀਜਾ ਸਹੀ ਹੈ। Total correctness: ਕੋਡ ਵਾਪਸ ਆਵੇਗਾ ਅਤੇ ਨਤੀਜਾ ਸਹੀ ਹੈ—ਇਸ ਲਈ terminating ਭੀ ਦਾਅਵਾ ਦਾ ਹਿੱਸਾ ਹੈ।
ਅਮਲੀ ਦੁਨੀਆ ਵਿੱਚ, ਜਦ “ਹਮੇਸ਼ਾ ਰੁਕ ਜਾਣਾ” ਯੂਜ਼ਰ-ਸਮਰਥਿਤ ਨੁਕਸਾਨ, ਰਿਸੋর্স ਲीक ਜਾਂ ਸੇਫਟੀ ਜੋਖਮ ਬਣ ਸਕਦਾ ਹੈ, ਤਾਂ total correctness ਮਹੱਤਵ ਰੱਖਦੀ ਹੈ।
Hoare triple {P} C {Q} ਇੱਕ ਛੋਟੀ ਰੀਤੀ-ਨਿਤੀ ਵਾਂਗਨ ਪੜ੍ਹਦੀ ਹੈ:
P (precondition): ਜੋ ਚੀਜ਼ਾਂ C ਚਲਾਉਣ ਤੋਂ ਪਹਿਲਾਂ ਸੱਚ ਹੋਣੀਆਂ ਚਾਹੀਦੀਆਂ ਹਨPreconditions ਉਹ ਹਨ ਜੋ ਕੋਡ ਨੂੰ ਚਲਾਉਣ ਤੋਂ ਪਹਿਲਾਂ ਲੋੜੀਂਦੇ ਹਨ (ਉਦਾਹਰਣ: “indices ਰੇਂਜ ਵਿੱਚ ਹਨ”, “ਤੱਤ ਤੁਲਨਯੋਗ ਹਨ”, “ਲੌਕ ਹੱਥ ਵਿੱਚ ਹੈ”). ਜੇ caller ਉਹਨਾਂ ਨੂੰ ਉਲੰਘ ਸਕਦਾ ਹੈ ਤਾਂ:
ਨਹੀਂ ਤਾਂ ਤੁਹਾਡੇ postconditions ਸਿਰਫ਼ ਇੱਛਾ ਬਣ ਕੇ ਰਹਿ ਜਾਂਦੀਆਂ ਹਨ।
ਲੂਪ ਇਨਵੈਰੀਐਂਟ ਉਹ ਬਿਆਨ ਹੈ ਜੋ ਲੂਪ ਡੇਖਣ ਤੋਂ ਪਹਿਲਾਂ ਸੱਚ, ਹਰ ਇਟਰੈਸ਼ਨ ਦੇ ਬਾਅਦ ਵੀ ਸੱਚ, ਅਤੇ ਲੂਪ ਖ਼ਤਮ ਹੋਣ 'ਤੇ ਵੀ ਸੱਚ ਰਹਿੰਦਾ ਹੈ। ਕੁਝ ਵਰਤਣਯੋਗ ਟੈਮਪਲੇਟ ਹਨ:
0 ≤ i ≤ n)ਜੇ ਤੁਸੀਂ ਇਨਵੈਰੀਐਂਟ ਬਿਆਨ ਨਹੀਂ ਕਰ ਸਕਦੇ ਤਾਂ ਇਹ ਨਿਸ਼ਾਨ ਹੈ ਕਿ ਲੂਪ ਬਹੁਤ ਸਾਰੀਆਂ ਚੀਜ਼ਾਂ ਇੱਕੱਠੇ ਕਰ ਰਿਹਾ ਹੈ ਜਾਂ ਸੀਮਾਵਾਂ ਅਸਪਸ਼ਟ ਹਨ।
ਆਪਣੇ ਆਪ termination ਦਿਖਾਉਣ ਲਈ ਤੁਸੀਂ ਆਮ ਤੌਰ 'ਤੇ ਕੋਈ ਮਾਪ (measure/variant) ਨਾਮ ਦਿੱਤਾ ਹੋਇਆ ਰੱਖਦੇ ਹੋ ਜੋ ਹਰ ਇਟਰੈਸ਼ਨ ਵਿੱਚ ਘਟਦਾ ਹੈ ਅਤੇ ਜੋ ਅਣੰਤ ਤੱਕ ਘਟ ਨਹੀਂ ਸਕਦਾ। ਉਦਾਹਰਣ: n - i ਹਰ ਵਾਰ 1 ਘਟਦਾ ਹੈ, ਜਾਂ ‘unprocessed items’ ਦੀ ਗਿਣਤੀ ਘਟਦੀ ਹੈ।
ਜੇ ਕੋਈ ਘਟਦਾ ਮਾਪ ਨਹੀਂ ਮਿਲ ਰਿਹਾ ਤਾਂ ਤੁਹਾਨੂੰ ਅਨਿਅੰਤ ਲੂਪ ਦਾ ਖਤਰਾ ਮਿਲ ਸਕਦਾ ਹੈ।
Quicksort ਵਿੱਚ partition ਹੀ ਉਹ ਨੁਕੜਾ ਰੂਟੀਨ ਹੈ ਜਿਸ 'ਤੇ ਸਭ ਕੁਝ ਨਿਰਭਰ ਕਰਦਾ ਹੈ। ਜੇ partition ਥੋੜ੍ਹ੍ਹੀ ਵੀ ਗਲਤ ਹੋਵੇ ਤਾਂ:
ਇਸ ਲਈ partition ਦਾ contract ਸਪਸ਼ਟ ਰੱਖਣਾ ਤੇ ਉਸ ਦੇ ਨਾਲ consistency ਨਾਲ ਕੋਡ ਦੀ ਸਮੀਖਿਆ ਕਰਨਾ ਜ਼ਰੂਰੀ ਹੈ।
ਡੁਪਲੀਕੇਟਸ ਅਤੇ pivot ਦੇ ਬਰਾਬਰ ਵਾਲੀ ਹਾਲਤ ਆਮ ਤੌਰ 'ਤੇ ਗਲਤੀਆਂ ਪੈਦਾ ਕਰਦੀ ਹੈ। ਪ੍ਰਯੋਗੀ ਨਿਯਮ ਹਨ:
ਜੇ duplicates ਵੱਧ ਹਨ ਤਾਂ three-way partitioning ਜ਼ਿਆਦਾ ਸੁਰੱਖਿਅਤ ਅਤੇ ਪ੍ਰਭਾਵਸ਼ਾਲੀ ਹੈ।
ਟੈਸਟਿੰਗ ਅਸਲ ਗਲਤੀਆਂ ਲੱਭਦੀ ਹੈ; reasoning (ਸਬੂਤ-ਸਟਾਈਲ ਸੋਚ) ਬੁਨਿਆਦੀ ਤੌਰ 'ਤੇ ਬਾਜੂਆਂ ਦੀਆਂ ਕੈਟੈਗਰੀਆਂ ਨੂੰ ਬਾਹਰ ਕੱਢ ਸਕਦੀ ਹੈ। ਇੱਕ ਪ੍ਰਯੋਗੀ ਹਾਈਬ੍ਰਿਡ ਵਰਕਫਲੋ:
Sorting ਲਈ ਦੋ ਉੱਚ-ਕੀਮਤੀ ప్రਾਪਰਟੀਆਂ ਹਨ:
C: ਕੋਡ ਦਾ ਟੁਕੜਾQ (postcondition): C ਮੁਕੰਮਲ ਹੋਣ ਤੋਂ ਬਾਅਦ ਕੀ ਸੱਚ ਹੋਵੇਗਾ, ਜੇ P ਸਹੀ ਸੀਤੁਹਾਨੂੰ ਇਹ ਨੋਟੇਸ਼ਨ ਕੋਡ ਵਿੱਚ ਲਿਖਣ ਦੀ ਲੋੜ ਨਹੀਂ—ਰੀਵਿਊ ਵਿੱਚ “ਅਸੀਂਸ਼ਨਸ in, ਗਾਰੰਟੀਜ਼ out” ਜਿਵੇਂ ਡਾਂਚਾ ਵਰਤਣਾ ਹੀ ਅਮਲ ਵਿੱਚ ਫਾਇਦਾ ਦਿੰਦਾ ਹੈ।