ਟੋਨੀ ਹੋਅਰ ਦੇ ਸਹੀਤਾ ਵਿਚਾਰ: ਲਾਜਿਕ ਤੋਂ ਸੁਰੱਖਿਅਤ ਕੋਡ ਤੱਕ

"ਸਹੀਤਾ" ਦਾ ਮਤਲਬ ਸਿਰਫ਼ "ਇਹ ਚਲਦਾ ਹੈ" ਨਹੀਂ ਹੈ

ਜਦ ਲੋਕ ਕਹਿੰਦੇ ਹਨ ਕਿ ਇੱਕ ਪ੍ਰੋਗਰਾਮ "ਸਹੀ" ਹੈ, ਉਹ ਅਕਸਰ ਮਤਲਬ ਲੈਂਦੇ ਹਨ: "ਮੈਂ ਇਸਨੂੰ ਕੁਝ ਵਾਰੀ ਚਲਾਇਆ ਅਤੇ ਆਉਟਪੁੱਟ ਠੀਕ ਲੱਗਿਆ।" ਇਹ ਇੱਕ ਲਾਹੇਯਕ ਸੰਗੇਤ ਹੈ—ਪਰ ਇਹ ਸਹੀਤਾ ਨਹੀਂ। ਸਧਾਰਨ ਸ਼ਬਦਾਂ ਵਿੱਚ, ਸਹੀਤਾ ਦਾ ਮਤਲਬ ਹੈ ਕਿ ਪ੍ਰੋਗਰਾਮ ਆਪਣੀ ਵਿਵਰਣ ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ: ਹਰ ਮਨਜ਼ੂਰ ਇਨਪੁਟ ਲਈ, ਇਹ ਲੋੜੀਦਾ ਨਤੀਜਾ ਦਿੰਦਾ ਹੈ ਅਤੇ ਰਾਜ, ਸਮਾਂ-ਸੀਮਾਵਾਂ ਅਤੇ ਗਲਤੀਆਂ ਬਾਰੇ ਕੋਈ ਨਿਯਮ ਮੰਨਦਾ ਹੈ।

ਫਰੇਬ ਇਹ ਹੈ ਕਿ “ਇਹ ਆਪਣੀ ਵਿਵਰਣ ਨੂੰ ਪੂਰਾ ਕਰਦਾ” ਕਿਹਾ ਲਿਖਣ ਤੋਂ ਜ਼ਿਆਦਾ ਔਖਾ ਹੈ।

ਸਹੀਤਾ ਅਸਲ ਵਿੱਚ ਕਿਉਂ ਔਖਾ ਹੈ

ਪਹਿਲਾਂ, specifications ਅਕਸਰ ਅਸਪਸ਼ਟ ਹੁੰਦੀਆਂ ਹਨ। ਇਕ ਪ੍ਰੋਡਕਟ ਦੀ ਲੋੜ ਕਹਿ ਸਕਦੀ ਹੈ “ਲਿਸਟ sort ਕਰੋ”, ਪਰ ਕੀ ਇਸਦਾ ਮਤਲਬ stable sorting ਹੈ? ਨਕਲ ਮੁੱਲਾਂ, ਖਾਲੀ ਲਿਸਟਾਂ, ਜਾਂ ਗੈਰ-ਨੰਬਰਕ ਆਈਟਮਾਂ ਨਾਲ ਕੀ ਕੀਤਾ ਜਾਵੇ? ਜੇ spec ਨਹੀਂ ਦੱਸਦੀ, ਵੱਖ-ਵੱਖ ਲੋਕ ਵੱਖ-ਵੱਖ ਧਾਰਣਾ ਕਰਦੇ ਹਨ।

ਦੂਜਾ, edge cases ਰੁੱਟੀ ਰੀਟੀ ਨਹੀਂ—ਉਹ ਸਿਰਫ ਘੱਟ ਟੈਸਟ ਕੀਤੇ ਜਾਂਦੇ ਹਨ। Null ਮੁੱਲ, overflow, off-by-one ਸੀਮਾਵਾਂ, ਅਸਧਾਰਨ ਯੂਜ਼ਰ ਲੜੀਬੰਦੀ, ਅਤੇ ਅਕਸਮਾਤ ਬਾਹਰੀ ਫੇਲ੍ਹਰ “ਇਹ ਚੱਲਦਾ ਹੈ” ਨੂੰ "ਪ੍ਰੋਡਕਸ਼ਨ ਵਿੱਚ ਫੇਲ" ਵਿੱਚ ਬਦਲ ਸਕਦੇ ਹਨ।

ਤੀਜਾ, requirements ਬਦਲਦੇ ਹਨ। ਇੱਕ ਪ੍ਰੋਗਰਾਮ ਕੱਲ ਦੀ spec ਦੇ ਨਾਤੇ ਸਹੀ ਹੋ ਸਕਦਾ ਹੈ ਅਤੇ ਅੱਜ ਦੀ spec ਦੇ ਨਾਤੇ ਗਲਤ।

ਇਸ ਲੇਖ ਦੇ ਬਾਕੀ ਹਿੱਸੇ ਤੋਂ ਕੀ ਉਮੀਦ ਰੱਖੋ

Tony Hoare ਦਾ ਵੱਡਾ ਯੋਗਦਾਨ ਇਹ ਨਹੀਂ ਸੀ ਕਿ ਅਸੀਂ ਹਰ ਚੀਜ਼ ਨੂੰ ਹਮੇਸ਼ਾ ਪ੍ਰੂਵ ਕਰੀਏ। ਉਸ ਦਾ ਵਿਚਾਰ ਇਹ ਸੀ ਕਿ ਅਸੀਂ ਇਹ ਵੱਧ ਨਿਰਧਾਰਿਤ ਤਰੀਕੇ ਨਾਲ ਬਿਆਨ ਕਰ ਸਕਦੇ ਹਾਂ ਕਿ ਕੋਡ ਨੂੰ ਕੀ ਕਰਨਾ ਚਾਹੀਦਾ ਹੈ—ਅਤੇ ਇਸ ਬਾਰੇ ਨਿਯਮਤ ਢੰਗ ਨਾਲ ਸੋਚ ਸਕਦੇ ਹਾਂ।

ਇਸ ਪੋਸਟ ਵਿੱਚ ਅਸੀਂ ਤਿੰਨ ਜੁੜੇ ਹੋਏ ਧਾਗੇ ਫਾਲੋ ਕਰਾਂਗੇ:

• Hoare logic: preconditions ਅਤੇ postconditions ਵਰਤ ਕੇ ਹਲਕਾ, ਰਚਨਾਤਮਕ ਤਰਕ।
• Quicksort: ਇੱਕ ਜਾਣਿਆ-ਪਛਾਣਿਆ ਅਲਗੋਰਿਦਮ ਜੋ ਦਿਖਾਉਂਦਾ ਹੈ ਕਿ ਛੋਟੇ "ਸਪਸ਼ਟ" ਕਦਮ (ਜਿਵੇਂ partition) ਵੀ ਧਿਆਨ ਦੀ ਲੋੜ ਰੱਖਦੇ ਹਨ।
• Safety mindset: ਜਦ ਨੁਕਸਾਨ ਦੇ ਨਤੀਜੇ ਵਾਜਬ ਹੋ ਸਕਦੇ ਹਨ, ਤਾਂ ਸਹੀਤਾ ਇੱਕ ਪ੍ਰਯੋਗੀ ਜ਼ਿੰਮੇਵਾਰੀ ਹੈ।

ਜ਼ਿਆਦਾਤਰ ਟੀਮਾਂ ਪੂਰੇ ਫਾਰਮਲ ਸਬੂਤ ਨਹੀਂ ਲਿਖਣਗੀਆਂ। ਪਰ ਅੱਧ-ਭਾਗ, “ਸਬੂਤ-ਸਟਾਈਲ” ਸੋਚ ਵੀ ਬੱਗਾਂ ਦੀ ਪਹਿਚਾਣ ਆਸਾਨ ਕਰ ਸਕਦੀ ਹੈ, ਸਮੀਖਿਆਵਾਂ ਨੂੰ ਤੇਜ਼ ਕਰਦੀ ਹੈ, ਅਤੇ ਕਿਸੇ ਚੀਜ਼ ਨੂੰ ਸ਼ਿਪ ਕਰਨ ਤੋਂ ਪਹਿਲਾਂ ਵੈਹਿਆਂਨਤਾ ਸਪਸ਼ਟ ਕਰਦੀ ਹੈ।

Tony Hoare ਸੰਖੇਪ: ਆਈਡੀਆ ਜੋ ਰੋਜ਼ਮਰਾ ਕੋਡ ਵਿੱਚ ਆ ਗਏ

Tony Hoare ਉਹਨਾਂ ਵੱਖਰੇ ਕੰਮ ਕਰਨ ਵਾਲੇ ਕੰਪਿਊਟਰ ਵਿਗਿਆਨੀਆਂ ਵਿੱਚੋਂ ਹੈ ਜਿਨ੍ਹਾਂ ਦਾ ਕੰਮ ਪੇਪਰਾਂ ਜਾਂ ਕਲਾਸਰੂਮ ਤੱਕ ਹੀ ਸੀਮਿਤ ਨਹੀਂ ਰਿਹਾ। ਉਹ ਅਕਾਡਮੀਅ ਅਤੇ ਇੰਡਸਟਰੀ ਦੋਹਾਂ ਵਿੱਚ ਨੇੜੇ ਰਹੇ, ਅਤੇ ਉਹ ਇੱਕ ਪ੍ਰਯੋਗੀ ਸਵਾਲ 'ਤੇ ਧਿਆਨ ਰੱਖਦੇ ਸਨ ਜੋ ਹਰ ਟੀਮ ਅਜੇ ਵੀ ਮੁੱਖ ਰੱਖਦੀ ਹੈ: ਵੱਡੇ ਸਟੇਕਾਂ ਵਾਲੀ ਸਥਿਤੀ ਵਿੱਚ ਅਸੀਂ ਕਿਵੇਂ ਜਾਣੀਏ ਕਿ ਪ੍ਰੋਗਰਾਮ ਉਹੀ ਕਰ ਰਿਹਾ ਹੈ ਜੋ ਅਸੀਂ ਸੋਚਦੇ ਹਾਂ?

ਇਸ ਲੇਖ ਲਈ ਮਹੱਤਵਪੂਰਨ ਯੋਗਦਾਨ

ਇਹ ਲੇਖ ਕੁਝ Hoare ਦੇ ਆਈਡੀਆ 'ਤੇ ਧਿਆਨ ਦਿੰਦਾ ਹੈ ਜੋ ਅਕਸਰ ਅਸਲੀ ਕੋਡਬੇਸਾਂ ਵਿੱਚ ਵਾਪਸ ਆਉਂਦੇ ਹਨ:

• Hoare logic: preconditions, postconditions ਅਤੇ ਮਸ਼ਹੂਰ Hoare triple {P} C {Q} ਵਰਤ ਕੇ ਪ੍ਰੋਗਰਾਮ ਬਿਹੇਵਿਅਰ ਦਾ ਵਰਣਨ।
• ਲੂਪ invariants: ਲੂਪਾਂ ਬਾਰੇ ਸੋਚਣ ਲਈ ਇਕ ਅਨੁਸ਼ਾਸਿਤ ਆਦਤ ਜੋ “ਮੇਰੇ ਮਸ਼ੀਨ ਤੇ ਚੱਲਿਆ” ਤੋਂ ਆਗੇ ਲੈ ਜਾਂਦੀ ਹੈ।
• Quicksort (ਖ਼ਾਸ ਕਰਕੇ partition ਕਦਮ): ਇੱਕ ਮਿਸਾਲ ਜਿੱਥੇ ਸਹੀਤਾ ਦਾ ਸੂਤਰਾ ਛੋਟਾ ਹੋ ਕੇ ਵੀ ਬਹੁਤ ਕੁਝ ਸਪਸ਼ਟ ਕਰ ਦਿੰਦਾ ਹੈ।
• ਸੁਰੱਖਿਆ ਸੋਚ: ਸਹੀਤਾ ਕੋਈ ਲਗਜ਼ਰੀ ਨਹੀਂ; ਜਦ ਨੁਕਸਾਨ ਵਾਸਤਵਿਕ ਹੋ ਸਕਦਾ ਹੈ ਤਾਂ ਇਹ ਫਰਕ ਪਾ ਸਕਦੀ ਹੈ।

ਇਹ ਲੇਖ ਕੀ ਨਹੀਂ ਕਰੇਗਾ

ਤੁਸੀਂ ਇਥੇ ਡੂੰਘੀ ਗਣਿਤੀ ਫਾਰਮਲਿਜ਼ਮ ਨਹੀਂ ਲੱਭੋਗੇ, ਅਤੇ ਅਸੀਂ Quicksort ਦਾ ਪੂਰਾ, ਮਸ਼ੀਨ-ਚੈਕੇਬਲ ਸਬੂਤ ਵੀ ਨਹੀਂ ਦੇਖਾਂਗੇ। ਉਦੇਸ਼ ਇਹ ਹੈ ਕਿ ਸੰਕਲਪ ਪਹੁੰਚਯੋਗ ਰਹਿਣ: ਇਤਨਾ ਢਾਂਚਾ ਕਿ ਤੁਹਾਡੀ ਸੋਚ ਸਪਸ਼ਟ ਹੋ ਜਾਏ, ਬਿਨਾਂ ਤੁਹਾਡੇ ਕੋਡ ਰਿਵਿਊ ਨੂੰ ਡਿਗਰੀ-ਸੈਮੀਨਾਰ ਵਿੱਚ ਬਦਲ ਦੇਣ ਦੇ।

ਉਸਦੇ ਕੰਮ ਦਾ ਰੋਜ਼ਮਰਾ ਪ੍ਰੋਗ੍ਰਾਮਿੰਗ 'ਤੇ ਪ੍ਰਭਾਵ

Hoare ਦੇ ਵਿਚਾਰ ਆਮ ਫੈਸਲਿਆਂ ਵਿੱਚ ਤਬਦੀਲ ਹੋ ਜਾਂਦੇ ਹਨ: ਕਿਸ assumptions 'ਤੇ ਇੱਕ ਫੰਕਸ਼ਨ ਨਿਰਭਰ ਕਰਦਾ ਹੈ, ਇਹ callers ਨੂੰ ਕੀ ਗਾਰੰਟੀ ਦਿੰਦਾ ਹੈ, ਇੱਕ ਲੂਪ ਦੇ ਅੱਧੇ-ਦੌਰਾਨ ਕੀ ਸੱਚ ਰਹਿੰਦਾ ਹੈ, ਅਤੇ ਸਮੀਖਿਆ ਦੌਰਾਨ “ਲਗਭਗ ਠੀਕ” ਤਬਦੀਲੀਆਂ ਨੂੰ ਕਿਵੇਂ ਪਛਾਣਿਆ ਜਾਵੇ। ਜੇ ਤੁਸੀਂ ਕਦੇ {P} C {Q} ਖੁਲ੍ਹ ਕੇ ਨਹੀਂ ਲਿਖਦੇ, ਉਸ ਰਚਨਾ ਵਿੱਚ ਸੋਚਣਾ ਇੰਟਰਫੇਸ, ਟੈਸਟ ਅਤੇ ਗੰਭੀਰ ਕੋਡ-ਗੱਲ-ਬਾਤ ਨੂੰ ਬਿਹਤਰ ਬਣਾਉਂਦਾ ਹੈ।

ਅਮਲੀ ਤੌਰ 'ਤੇ "ਸਹੀਤਾ" ਦਾ ਕੀ ਮਤਲਬ ਹੈ

Hoare ਦੀ ਨਜ਼ਰ "ਕੁਝ ਉਦਾਹਰਣਾਂ ਪਾਸ ਹੋ ਗਈਆਂ" ਤੋਂ ਕਠੋਰ ਹੈ: ਸਹੀਤਾ ਇੱਕ ਸਹਿਮਤ ਵਾਅਦੇ (agreed promise) ਨੂੰ ਮਿਲਣਾ ਹੈ, ਨਾ ਕਿ ਛੋਟੇ ਨਮੂਨਿਆਂ 'ਤੇ ਠੀਕ ਲੱਗਣਾ।

Requirements vs specification vs implementation

• Requirements ਕਾਰੋਬਾਰੀ ਲੋੜ ਹਨ (ਸਿੱਧੇ ਸ਼ਬਦਾਂ ਵਿੱਚ)।
• Specification ਉਸ ਲੋੜ ਦਾ ਨਿਰਧਾਰਿਤ, ਜਾਂਚਯੋਗ ਰੂਪ ਹੈ (ਫੰਕਸ਼ਨ ਨੂੰ ਕੀ ਕਰਨਾ ਚਾਹੀਦਾ ਹੈ)।
• Implementation ਉਹ ਕੋਡ ਹੈ ਜੋ ਤੁਸੀਂ ਲਿਖਦੇ ਹੋ (ਕਿਵੇਂ ਕਰਦਾ ਹੈ)।

ਬੱਗ ਆਮ ਤੌਰ 'ਤੇ ਉਦੋਂ ਹੁੰਦੇ ਹਨ ਜਦ ਟੀਮ ਮੱਧਲਾ ਕਦਮ ਛੱਡ ਦਿੰਦੀ ਹੈ: ਉਹ requirements ਤੋਂ ਸਿੱਧੇ implementation 'ਤੇ ਛਾਲ ਮਾਰ ਦਿੰਦੇ ਹਨ, ਜਿਸ ਨਾਲ ਵਾਅਦਾ ਫੱਜੀ ਰਹਿ ਜਾਂਦਾ ਹੈ।

ਆਧ部分ੀ ਸਹੀਤਾ vs ਮੁਕੰਮਲ ਸਹੀਤਾ

ਅਕਸਰ ਦੋ ਦਾਅਵੇ ਮਿਲ ਜਾਂਦੇ ਹਨ:

• Partial correctness: ਜੇ ਕੋਡ ਵਾਪਸ ਆਇਆ, ਤਾਂ ਨਤੀਜਾ ਠੀਕ ਹੈ।
• Total correctness: ਕੋਡ ਵਾਪਸ ਆਵੇਗਾ ਅਤੇ ਨਤੀਜਾ ਠੀਕ ਹੈ। (ਇਸ ਲਈ termination ਵੀ ਦਾਅਵਾ ਵਿੱਚ ਸ਼ਾਮਲ ਹੈ)

ਅਸਲੀ ਪ੍ਰਣਾਲੀਆਂ ਲਈ, “ਕਦੇ ਖਤਮ ਨਾ ਹੋਣਾ” ਵੀ “ਗਲਤ ਜਵਾਬ ਦੇਣ” ਦੇ ਬਰਾਬਰ ਨੁਕਸਾਨ ਕਰ ਸਕਦਾ ਹੈ।

ਸਹੀਤਾ ਹਮੇਸ਼ਾ assumptions 'ਤੇ ਨਿਰਭਰ ਹੁੰਦੀ ਹੈ

ਸਹੀਤਾ ਕਦੇ ਵੀ ਸਰਵਜਨੀਕ ਨਹੀਂ ਹੁੰਦੀ; ਇਹ ਹੇਠਾਂ ਦਿੱਤੀਆਂ assumptions 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ:

• ਇਨਪੁਟ (ਉਦਾਹਰਣ: ਲਿਸਟ memory ਵਿੱਚ ਆ ਸਕਦੀ ਹੈ, ਤੱਤ ਤੁਲਨਯੋਗ ਹਨ)
• ਪਾਬੰਦੀਆਂ (ਉਦਾਹਰਣ: ਸਮਾਂ ਸੀਮਾਵਾਂ, ਪੂਰੇ ਲਈ integer ਰੇਂਜ)
• ਵਾਤਾਵਰਨ (ਉਦਾਹਰਣ: concurrency, I/O ਫੇਲ੍ਹਰ, configuration)

assumptions ਨੂੰ ਖੁੱਲ੍ਹਾ ਕਰਨ ਨਾਲ “ਮੇਰੀ ਮਸ਼ੀਨ ਤੇ ਚੱਲਦਾ” ਕਿਸੇ ਹੋਰ ਨੂੰ reasoning ਕਰਨ ਯੋਗ ਬਣ ਜਾਂਦਾ ਹੈ।

ਇੱਕ ਛੋਟੀ spec ਉਦਾਹਰਣ

ਇਕ ਫੰਕਸ਼ਨ sortedCopy(xs) ਸੋਚੋ।

ਇੱਕ ਉਪਯੋਗ spec ਹੋ ਸਕਦੀ ਹੈ: “ਨਵੀਂ ਲਿਸਟ ys ਵਾਪਸ ਕਰਦਾ ਹੈ ਜਿਸ ਨਾਲ (1) ys ਉਤਾਰਦੀ ਕ੍ਰਮ ਵਿੱਚ sorted ਹੈ, ਅਤੇ (2) ys ਵਿੱਚ ਠੀਕ ਉਹੀ ਤੱਤ ਹਨ ਜੋ xs ਵਿੱਚ ਸਨ (ਗਿਣਤੀਆਂ ਸਮੇਤ), ਅਤੇ (3) xs ਬਦਲੀ ਨਹੀਂ ਗਈ।”

ਹੁਣ “ਸਹੀ” ਦਾ ਮਤਲਬ ਹੈ ਕਿ ਕੋਡ ਉਪਰੋਕਤ ਤੀਨ ਨੁਕਤਿਆਂ ਨੂੰ ਦਰਸਾਈਆਂ ਗਈਆਂ assumptions ਹੇਠਾਂ ਪੂਰਾ ਕਰਦਾ ਹੈ—ਸਿਰਫ਼ ਇਸ ਲਈ ਨਹੀਂ ਕਿ ਆਊਟਪੁੱਟ ਇੱਕ ਤੇਜ਼ ਟੈਸਟ ਵਿੱਚ sorted ਲੱਗ ਰਿਹਾ ਸੀ।

Hoare logic ਬੁਨਿਆਦੀ: preconditions, postconditions, triples

Hoare logic ਪ੍ਰੋਗਰਾਮ ਬਾਰੇ ਉਨ੍ਹਾਂ ਹੀ ਤਰ੍ਹਾਂ ਗੱਲ ਕਰਦਾ ਹੈ ਜਿਵੇਂ ਤੁਸੀਂ ਕਿਸੇ ਠੇਕੇ ਦੀ ਗੱਲ ਕਰਦੇ ਹੋ: ਜੇ ਤੁਸੀਂ ਇੱਕ ਸਥਿਤੀ ਵਿੱਚ ਸ਼ੁਰੂ ਕਰਦੇ ਹੋ ਜੋ ਕੁਝ assumptions ਪੂਰੀਆਂ ਕਰਦੀ ਹੈ, ਅਤੇ ਤੁਸੀਂ ਇਹ ਟੁਕੜਾ ਕੋਡ ਚਲਾਉਂਦੇ ਹੋ, ਤਾਂ ਤੁਸੀਂ ਇੱਕ ਐਸੀ ਸਥਿਤੀ ਤੇ ਪਹੁੰਚੋਗੇ ਜੋ ਕੁਝ ਗਾਰੰਟੀਆਂ ਪੂਰੀਆਂ ਕਰਦੀ ਹੈ।

ਮੁੱਖ ਨੋਟੇਸ਼ਨ ਹੈ Hoare triple:

{precondition} program {postcondition}

Preconditions: ਤੁਸੀਂ ਕੀ ਮੰਨਦੇ ਹੋ

A precondition ਦਸਦੀ ਹੈ ਕਿ ਕੋਡ ਟੁਕੜਾ ਚਲਾਉਣ ਤੋਂ ਪਹਿਲਾਂ ਕੀ ਸੱਚ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ। ਇਹ ਇਹ ਨਹੀਂ ਕਿ ਤੁਸੀਂ ਆਸ ਕਰੋ—ਇਹ ਉਹ ਹੈ ਜੋ ਕੋਡ ਨੂੰ ਚਾਹੀਦਾ ਹੈ।

ਉਦਾਹਰਣ: ਮੰਨੋ ਇੱਕ ਫੰਕਸ਼ਨ ਦੋ ਨੰਬਰਾਂ ਦਾ ਔਸਤ ਦੇਂਦਾ ਹੈ ਬਗੈਰ overflow ਚੈੱਕਾਂ ਦੇ।

• Precondition: a + b integer ਟਾਈਪ ਵਿੱਚ ਫਿੱਟ ਹੁੰਦਾ ਹੈ
• Program: avg = (a + b) / 2
• Postcondition: avg ਅਕਲਪਿਕ ਔਸਤ ਦੇ ਬਰਾਬਰ ਹੈ

ਜੇ precondition ਨਹੀਂ ਰਿਹਾ, ਤਾਂ postcondition ਦੀ ਗਾਰੰਟੀ ਲਾਗੂ ਨਹੀਂ ਹੁੰਦੀ। triple ਤੁਹਾਨੂੰ ਇਹ ਸਪਸ਼ਟ ਕਰਨ ਲਈ ਮਜਬੂਰ ਕਰਦੀ ਹੈ।

Postconditions: ਤੁਸੀਂ ਕੀ ਗਾਰੰਟੀ ਕਰਦੇ ਹੋ

A postcondition ਦਸਦੀ ਹੈ ਕਿ ਕੋਡ ਚਲਣ ਤੋਂ ਬਾਅਦ ਕੀ ਸੱਚ ਹੋਵੇਗਾ—ਜੇ precondition ਰਿਹਾ। ਚੰਗੀਆਂ postconditions konkreਟ ਅਤੇ ਜਾਂਚਯੋਗ ਹੁੰਦੀਆਂ ਹਨ। “ਰਿਜ਼ਲਟ ਵੈਧ ਹੈ” ਕਹਿਣ ਦੀ ਥਾਂ, ਦੱਸੋ ਕਿ "ਵੈਧ" ਦਾ ਮਤਲਬ ਕੀ ਹੈ: sorted, non-negative, ਬਾਊਂਡ ਵਿੱਚ, ਮੁਖ fields ਛੱਡ ਕੇ ਬਦਲਿਆ ਗਿਆ, ਆਦਿ।

Assignment ਅਤੇ sequencing (ਬਿਨਾਂ ਬਹੁਤ ਸਾਰੀਆਂ ਨਿਸ਼ਾਨੀਆਂ ਦੇ)

Hoare logic ਛੋਟੇ ਬਿਆਨਾਂ ਤੋਂ ਲੈ ਕੇ ਕਈ ਕਦਮਾਂ ਵਾਲੇ ਕੋਡ ਤੱਕ ਦਲਿਲਾਂ ਨੂੰ ਵਧਾਉਂਦਾ ਹੈ:

• Assignment ਸਥਿਤੀ ਨੂੰ ਇੱਕ ਨਿਰਧਾਰਿਤ ਤਰੀਕੇ ਨਾਲ ਬਦਲਦਾ ਹੈ। ਕਿਸੇ ਵੀ ਬਿਆਨ ਬਾਅਦ ਪੁੱਛਿਆ ਜਾਂਦਾ ਹੈ: x = x + 1 ਤੋਂ ਬਾਅਦ x ਬਾਰੇ ਕੀ ਸੱਚ ਹੈ?
• Sequencing ("ਇਹ ਕਰੋ, ਫਿਰ ਉਹ") ਗਾਰੰਟੀਆਂ ਨੂੰ ਚੇਨ ਕਰਦਾ ਹੈ: ਜੇ ਪਹਿਲਾ ਕਦਮ ਦੂਜੇ ਕਦਮ ਲਈ precondition ਸਥਾਪਤ ਕਰਦਾ ਹੈ ਤਾਂ ਪੂਰੇ ਬਲਾਕ ਨੂੰ ਭਰੋਸੇਯੋਗ ਬਣਾਉਂਦਾ ਹੈ।

ਮਕਸਦ ਇਹ ਨਹੀਂ ਕਿ ਹਰ ਥਾਂ curly braces ਪੈਣਾ ਸ਼ੁਰੂ ਕਰ ਦਿਓ। ਮਕਸਦ ਹੈ ਇਰਾਦਾ ਪਾਠਯੋਗ ਬਣਾਉਣਾ: ਸਪਸ਼ਟ assumptions, ਸਪਸ਼ਟ outcomes, ਅਤੇ ਸਮੀਖਿਆਵਾਂ ਵਿੱਚ "ਇਹ ਚੱਲਦਾ ਹੈ" ਵਾਲੀਆਂ ਗੱਲਾਂ ਘੱਟ।

ਲੂਪ invariants ਜੋ ਅਸਲ ਟੀਮਾਂ ਲਿਖ ਸਕਦੀਆਂ ਹਨ

A ਲੂਪ invariant ਇੱਕ ਬਿਆਨ ਹੈ ਜੋ ਲੂਪ ਸ਼ੁਰੂ ਹੋਣ ਤੋਂ ਪਹਿਲਾਂ ਸੱਚ ਹੋਵੇ, ਹਰ ਇਟਰੈਸ਼ਨ ਦੇ ਬਾਅਦ ਵੀ ਸੱਚ ਰਹੇ, ਅਤੇ ਲੂਪ ਖ਼ਤਮ ਹੋਣ 'ਤੇ ਵੀ ਸੱਚ ਹੋਵੇ। ਇਹ ਇੱਕ ਸਧਾਰਨ ਵਿਚਾਰ ਹੈ ਪਰ ਬਹੁਤ ਮਹੱਤਵਪੂਰਨ ਨਤੀਜੇ ਦਿੰਦਾ: ਇਹ "ਇਹ ਚੱਲਦਾ ਹੈ" ਨੂੰ ਉਹ ਮੁਲਾਂਕਣ ਦਿੰਦਾ ਹੈ ਜੋ ਹਰ ਕਦਮ 'ਤੇ ਜਾਂਚਿਆ ਜਾ ਸਕਦਾ ਹੈ।

ਇਨਵੈਰੀਐਂਟ ਹਥ-ਹਵਾਈ reasoning ਰੋਕਦੇ ਹਨ

ਇਨਵੈਰੀਐਂਟ ਨਾ হলে, ਇੱਕ ਸਮੀਖਿਆ ਅਕਸਰ ਐਸਾ ਸੁਣਾਉਂਦੀ ਹੈ: “ਅਸੀਂ ਲਿਸਟ ਉੱਤੇ ਇਟਰੈਟ ਕਰਦੇ ਹਾਂ ਅਤੇ ਕਦਮ-ਬ-ਕਦਮ ਚੀਜ਼ਾਂ ਠੀਕ ਕਰਦੇ ਹਾਂ।” ਇੱਕ invariant ਤਰਤੀਬ ਨੂੰ ਜ਼ਿਆਦਾ ਸਪਸ਼ਟ ਕਰਦਾ ਹੈ: “ਇਸ ਵੇਲੇ ਕੀ ਠੀਕ ਹੈ।” ਜਦ ਤੁਸੀਂ ਇਹ ਸਾਫ਼ ਦਸ ਦਿੰਦੇ ਹੋ ਤਾਂ off-by-one ਗਲਤੀਆਂ ਅਤੇ ਛੁੱਟ ਗਈਆਂ ਕੇਸਾਂ ਬਾਹਰ ਆ ਜਾਂਦੀਆਂ, ਕਿਉਂਕਿ ਉਹ ਉਨ੍ਹਾਂ ਮੋਹਲਤਾਂ 'ਤੇ invariant ਨੂੰ ਤੌੜ ਦੇਂਦੇ ਹਨ।

ਇਨਵੈਰੀਐਂਟ ਟੈਮਪਲੇਟ ਜੋ ਤੁਸੀਂ ਦੁਬਾਰਾ ਵਰਤ ਸਕਦੇ ਹੋ

ਜ਼ਿਆਦਾਤਰ ਦਿਨ-ਪ੍ਰਤੀਦਿਨ ਕੋਡ ਕੁਝ ਨਿਰਧਾਰਿਤ ਟੈਮਪਲੇਟ ਵਰਤ ਸਕਦਾ ਹੈ।

1) ਬਾਊਂਡ / ਇੰਡੈਕਸ ਸੁਰੱਖਿਆ

• 0 ≤ i ≤ n
• low ≤ left ≤ right ≤ high

ਇਹ ਕਿਸਮ ਦੇ invariants out-of-range ਐਕਸੈਸ ਰੋਕਣ ਅਤੇ array reasoning ਨੂੰ konkreਟ ਬਣਾਉਣ ਵਿੱਚ ਸ਼ਾਨਦਾਰ ਹਨ।

2) ਪ੍ਰੋਸੈਸਡ vs ਅਨ-ਪਰੋਸੈਸਡ ਆਈਟਮ

• “a[0..i) ਦੇ ਸਾਰੇ ਤੱਤ ਵੇਖੇ ਜਾ ਚੁਕੇ ਹਨ।”
• “ਹਰ ਆਈਟਮ ਜੋ result ਵਿੱਚ ਗਇਆ ਉਹ filter predicate ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ।”

ਇਸ ਨਾਲ ਅਸਪਸ਼ਟ ਪ੍ਰੋਗਰੈਸ ਨੂੰ ਇਹ ਸਪਸ਼ਟ ਕਾਂਟ੍ਰੈਕਟ ਮਿਲਦਾ ਹੈ ਕਿ “ਕੀ ਕੀਤਾ ਹੋ ਚੁਕਾ ਹੈ।”

3) Sorted prefix (ਜਾਂ partitioned prefix)

• “a[0..i) sorted ਹੈ।”
• “a[0..i) ਦੇ ਸਾਰੇ ਆਈਟਮ ≤ pivot ਹਨ, ਅਤੇ a[j..n) ਦੇ ਸਾਰੇ ≥ pivot ਹਨ।”

ਇੱਥੇ ਤੱਕ ਕਿ ਜਦ پوری array sorted ਨਾ ਹੋਵੇ, ਤੁਸੀਂ ਉਹ ਹਿੱਸਾ ਜੋ sorted/partitioned ਹੈ, ਫਿਕਸ ਕਰ ਸਕਦੇ ਹੋ।

ਸਧਾਰਨ ਸ਼ਬਦਾਂ ਵਿੱਚ termination: ਇੱਕ ਘਟਦਾ ਮਾਪ

ਸਹੀਤਾ ਸਿਰਫ਼ ਠੀਕ ਹੋਣ ਦੀ ਗੱਲ ਨਹੀਂ—ਲੂਪ ਨੂੰ ਵੀ ਖਤਮ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ। ਇੱਕ ਸਾਦਾ ਤਰੀਕਾ ਇਹ ਦਿਖਾਉਣ ਦਾ ਹੈ ਕਿ ਕੋਈ ਮਾਪ (variant) ਹਰ ਇਟਰੈਸ਼ਨ ਨਾਲ ਘਟ ਰਿਹਾ ਹੈ ਅਤੇ ਲੋੜੀ ਜਾਂਦੀ حد ਤੋਂ ਪਿੱਛੇ ਨਹੀਂ ਜਾ ਸਕਦਾ।

ਉਦਾਹਰਣ:

• “n - i ਹਰ ਵਾਰੀ 1 ਨਾਲ ਘਟਦਾ ਹੈ।”
• “ਅਨ-ਪਰੋਸੈਸਡ ਆਈਟਮਾਂ ਦੀ ਗਿਣਤੀ ਘਟਦੀ ਹੈ।”

ਜਦ ਤੁਸੀਂ ਘਟਦਾ ਮਾਪ ਨਹੀਂ ਲੱਭ ਪਾਂਦੇ, ਇਹ ਇੱਕ ਅਸਲੀ ਜੋਖਮ ਦਾ ਇਸ਼ਾਰਾ ਹੋ ਸਕਦਾ ਹੈ: ਕੁਝ ਇਨਪੁਟਾਂ 'ਤੇ ਅਨੰਤ ਲੂਪ।

Quicksort: ਕੋਡ ਬਾਰੇ ਤਰਕ ਕਰਨ ਲਈ ਇੱਕ ਕੇਸ-ਸਟਡੀ

Quicksort ਦਾ ਸਪੱਸ਼ਟ ਵਾਅਦਾ ਹੈ: ਦਿੱਤੇ ਗਏ slice (ਜਾਂ array segment) ਨੂੰ ਇਸ ਤਰੀਕੇ ਨਾਲ ਰੀਅਰੇਂਜ ਕਰੋ ਕਿ ਉਹ non-decreasing ਕ੍ਰਮ ਵਿੱਚ ਆ ਜਾਵੇ, ਬਿਨਾਂ ਕਿਸੇ ਤੱਤ ਨੂੰ ਖੋਏ ਜਾਂ ਨਵਾਂ ਬਣਾਏ। ਅਲਗੋਰਿਦਮ ਦੀ ਉੱਚ-ਸਤਹੀ ਰੂਪ ਇਹ ਹੈ:

1. ਇੱਕ pivot ਚੁਣੋ।
2. ਰੇਂਜ ਨੂੰ partition ਕਰੋ ਤਾਂ ਕਿ pivot ਤੋਂ "ਛੋਟੇ" ਤੱਤ ਇੱਕ ਪਾਸੇ ਆ ਜਾਣ ਅਤੇ "ਵੇਹੜੇ" ਦੂਜੇ ਪਾਸੇ (ਕੁਝ rule equal ਲਈ ਵੀ)।
3. ਖੱਬੇ ਅਤੇ ਸੱਜੇ ਸਬਰੇਂਜ ਤੇ ਰਿਕਰਸ ਕਰੋ।

ਇਹ ਸਿੱਖਣ ਲਈ ਵਧੀਆ ਮਿਸਾਲ ਹੈ ਕਿਉਂਕਿ ਇਹ ਦਿਮਾਗ ਵਿੱਚ ਰੱਖਣ ਲਈ ਛੋਟਾ ਹੈ, ਪਰ ਬਹੁਤ ਕੁਝ ਦਿਖਾਉਂਦਾ ਹੈ ਜਿੱਥੇ ਅਨਉਪਚਾਰਿਕ reasoning ਫੇਲ ਹੁੰਦੀ ਹੈ। ਕਈ ਵਾਰੀ Quicksort ਜੋ "ਕੁਝ ਟੈਸਟਾਂ 'ਤੇ ਚੰਗਾ ਲੱਗਦਾ" ਉਹ ਵਿਸ਼ੇਸ਼ ਇਨਪੁਟਾਂ ਜਾਂ ਸੀਮਾਵਾਂ 'ਤੇ ਗਲਤ ਹੋ ਸਕਦਾ ਹੈ।

ਉਹ ਚੀਜ਼ਾਂ ਜੋ “ਸਪਸ਼ਟ” implementations ਨੂੰ ਤੋੜਦੀਆਂ ਹਨ

ਕੁਝ ਮੁੱਦੇ ਸਭ ਤੋਂ ਜ਼ਿਆਦਾ ਬੱਗ ਪੈਦਾ ਕਰਦੇ ਹਨ:

• Duplicates: ਜੇ partition equal to pivot ਨੂੰ inconsistent ਤਰੀਕੇ ਨਾਲ ਸਾਂਭਦਾ ਹੈ ਤਾਂ ਤੁਹਾਨੂੰ ਅਨੰਤ ਰਿਕਰਜ਼ਨ ਮਿਲ ਸਕਦੀ ਹੈ (subranges ਘਟਦੀਆਂ ਨਹੀਂ) ਜਾਂ partition ਆਪਣਾ ਨਿਯਮ ਤੋੜ ਸਕਦੀ ਹੈ।
• Empty ਜਾਂ ਇੱਕ-ਤੱਤ ਵਾਲੇ ਰੇਂਜ: base case ਸਹੀ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ; ਨਹੀਂ ਤਾਂ ਤੁਸੀਂ out-of-bounds indexing ਜਾਂ ਲੰਬੀ recursion ਦੇਖ ਸਕਦੇ ਹੋ।
• Off-by-one indices: partition ਅਕਸਰ ਦੋ pointers ਵਰਤਦਾ; ਇੱਕ ਗਲਤ ਤੁਲਨਾ ਜਾਂ increment ਇੱਕ ਤੱਤ ਛੱਡ ਸਕਦਾ ਹੈ ਜਾਂ ਰੇਂਜ ਤੋਂ ਬਾਹਰ swap ਕਰ ਸਕਦਾ ਹੈ।

ਅਸਲ ਵਿੱਚ ਕੀ ਸਾਬਤ ਕਰਨਾ ਲਾਜ਼ਮੀ ਹੈ

Hoare-ਸਟਾਈਲ ਤਰੀਕੇ ਨਾਲ correctness ਦੀ ਦਲੀਲ ਆਮ ਤੌਰ 'ਤੇ ਦੋ ਹਿੱਸਿਆਂ ਵਿੱਚ ਵੰਡਿਆ ਜਾਂਦਾ ਹੈ:

• Partition correctness: partition ਕਰਨ ਤੋਂ ਬਾਅਦ, ਖੱਬੇ ਪਾਸੇ ਹਰ ਤੱਤ pivot ਨਾਲ ਚੁਣੇ ਹੋਏ ਸੰਬੰਧ ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ, ਸੱਜੇ ਪਾਸੇ ਹਰ ਤੱਤ ਵਿਰੋਧੀ ਸੰਬੰਧ ਨੂੰ ਪੂਰਾ ਕਰਦਾ ਹੈ, ਅਤੇ ਨਤੀਜਾ ਮੂਲ ਤੱਤਾਂ ਦਾ permutation ਹੈ।
• Recursion correctness: recursive calls ਸਖਤ ਤੌਰ ਤੇ ਛੋਟੀਆਂ ਰੇਂਜਾਂ 'ਤੇ ਹੁੰਦੀਆਂ ਹਨ (termination) ਅਤੇ ਜੇ ਉਹ ਸਬਰੇਂਜਾਂ ਨੂੰ ਸਹੀ ਤਰੀਕੇ ਨਾਲ sort ਕਰਦੀਆਂ ਹਨ ਤਾਂ ਪੂਰੇ ਰੇਂਜ ਦੀ sortedness ਨਿਕਲਦੀ ਹੈ।

ਇਹ ਵੰਡ reasoning ਨੂੰ ਮੈਨੇਜਬਲ ਰੱਖਦੀ ਹੈ: partition ਨੂੰ ਸਹੀ ਬਣਾਓ, ਫਿਰ sorting ਦੀ correctness ਉਸਦੇ ਉੱਪਰ ਬਣਾਓ।

Partition correctness: Quicksort ਦਾ ਦਿਲ

Quicksort ਦੀ ਤੇਜ਼ੀ ਇੱਕ ਧੋਖੇਬਾਜ਼ ਤੌਰ 'ਤੇ ਛੋਟੀ ਰੁਟੀਨ 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ: partition। ਜੇ partition ਥੋੜ੍ਹ੍ਹੀ ਵੀ ਗਲਤ ਹੋਵੇ, Quicksort ਗਲਤ sort ਕਰ ਸਕਦਾ ਹੈ, ਸਦਾ ਲਈ ਚੱਲ ਸਕਦਾ ਹੈ, ਜਾਂ edge cases 'ਤੇ crash ਕਰ ਸਕਦਾ ਹੈ।

partition contract (ਕੀ ਗਾਰੰਟੀ ਕਰਨੀ ਚਾਹੀਦੀ ਹੈ)

ਅਸੀਂ ਧਾਰਮਿਕ 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 ਲਈ ਲਾਜ਼ਮੀ ਹੈ।

scan ਅਤੇ swap ਦੇ ਦੌਰਾਨ ਮੁੱਖ invariants

ਜਦ 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 ਨੂੰ ਬਰਕਰਾਰ ਰੱਖਦਾ ਹੈ ਅਤੇ ਅਣ-ਸ਼੍ਰੇਣੀਬੱਧ ਵਿਚਕਾਰੂ ਹਿੱਸਾ ਘਟਾਉਂਦਾ ਹੈ।

Edge cases ਜੋ correctness ਨੂੰ ਕਵਰ ਕਰਨਾ ਚਾਹੀਦਾ

• ਸਭ pivot ਤੋਂ ਛੋਟੇ ਹਨ: i ਸੱਜੇ ਵੱਲ ਦੌੜਦਾ ਹੈ; partition ਨੂੰ ਫਿਰ ਵੀ terminate ਕਰਨਾ ਅਤੇ ਇਕ ਸੰਦੂਕ p ਵਾਪਸ ਦੇਣਾ ਚਾਹੀਦਾ ਹੈ।
• ਸਭ pivot ਤੋਂ ਵੱਡੇ ਹਨ: j ਖੱਬੇ ਵੱਲ ਦੌੜਦਾ ਹੈ; termination ਦਾ ਇੱਕੋ ਹੀ ਅਲੋਚਨਾ।
• ਬਹੁਤ ਸਾਰੇ ਬਰਾਬਰ ਹਨ: ਜੇ ਤੁਲਨਾਵਾਂ inconsistent (< ਵਿਰੁੱਧ ≤) ਹਨ, pointers stuck ਹੋ ਸਕਦੇ ਹਨ। Hoare ਦੀ ਯੋਜਨਾ ਇੱਕ consistent rule 'ਤੇ ਨਿਰਭਰ ਕਰਦੀ ਹੈ ਤਾਂ ਕਿ ਪ੍ਰਗਤੀ ਜਾਰੀ ਰਹੇ।
• ਪਹਿਲਾਂ ਤੋਂ sorted / reverse sorted: ਇਹ ਕਾਂਟ੍ਰੈਕਟ ਨਹੀਂ ਤੋੜਣਾ ਚਾਹੀਦਾ, ਭਾਵੇਂ 퍼ਫਾਰਮੈਂਸ ਘੱਟ ਹੋ ਜਾਵੇ।

ਵੱਖ-ਵੱਖ partition ਸਕੀਮਾਂ (Lomuto, Hoare, three-way) ਮੌਜੂਦ ਹਨ। ਜ਼ਰੂਰੀ ਗੱਲ ਇਹ ਹੈ ਕਿ ਇੱਕ ਚੁਣੋ, ਉਸਦਾ contract ਸਪਸ਼ਟ ਕਰੋ, ਅਤੇ ਸਮੀਖਿਆ ਇਸੇ contract ਦੇ ਖਿਲਾਫ਼ ਕਰੋ।

ਰਿਕਰਸ਼ਨ ਬਾਰੇ ਤਰਕ: base cases ਅਤੇ termination

ਰਿਕਰਸ਼ਨ ਨੂੰ ਭਰੋਸੇਯੋਗ ਸਮਝਣਾ ਸਭ ਤੋਂ ਆਸਾਨ ਹੈ ਜਦ ਤੁਸੀਂ ਦੋ ਸਵਾਲਾਂ ਦਾ ਸਪਸ਼ਟ ਜਵਾਬ ਦੇ ਸਕੋ: ਇਹ ਕਦੋਂ ਰੁਕੇਗੀ? ਅਤੇ ਹਰ ਕਦਮ ਕਿਉਂ ਸਹੀ ਹੈ? Hoare-ਸਟਾਈਲ ਸੋਚ ਮਦਦ ਕਰਦੀ ਹੈ ਕਿਉਂਕਿ ਇਹ ਤੁਹਾਨੂੰ ਜ਼ੋਰ ਦਿੰਦੀ ਹੈ ਕਿ ਤੁਸੀਂ ਦੱਸੋ ਕਿ ਕਾਲ ਤੋਂ ਪਹਿਲਾਂ ਕੀ ਸੱਚ ਹੈ ਅਤੇ ਵਾਪਸੀ 'ਤੇ ਕੀ ਸੱਚ ਹੋਵੇਗਾ।

base case ਸਹੀ ਹੋਣਾ ਲਾਜ਼ਮੀ ਹੈ

ਇੱਕ 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 ਨਹੀਂ ਹੁੰਦਾ ਜੇ ਤਿਆਰ ਨਹੀਂ ਕੀਤਾ)।

subproblem ਨੂੰ ਘਟਣਾ ਚਾਹੀਦਾ ਹੈ

ਹਰ recursive ਕਦਮ ਨੂੰ ਆਪਣੇ ਆਪ 'ਤੇ ਇਕ ਕਠੋਰ ਛੋਟਾ input ਚਾਹੀਦਾ ਹੈ। ਇਹ "shrinking" termination ਦਾ ਦਲੀਲ ਹੈ: ਜੇ ਸਾਈਜ਼ ਘਟਦੀ ਹੈ ਅਤੇ 0 ਤੋਂ ਘੱਟ ਨਹੀਂ ਹੋ ਸਕਦੀ, ਤਾਂ ਤੁਸੀਂ ਅਨੰਤ ਤਕ recurse ਨਹੀਂ ਕਰ ਸਕਦੇ।

ਛੋਟਾ ਹੋਣਾ স্টੈਕ ਸੁਰੱਖਿਆ ਲਈ ਵੀ ਜਰੂਰੀ ਹੈ। ਸਹੀ ਕੋਡ ਵੀ crash ਕਰ ਸਕਦਾ ਹੈ ਜੇ recursion depth ਬਹੁਤ ਵੱਧ ਜਾਵੇ। Quicksort ਵਿੱਚ, unbalanced partitions ਗਹਿਰੇ recursion ਪੈਦਾ ਕਰ ਸਕਦੇ ਹਨ। ਇਹ termination-proofs ਦੇ ਨਾਲ-ਨਾਲ ਇੱਕ ਪ੍ਰਯੋਗੀ ਯਾਦ ਦਿਵਾਉਂਦਾ ਹੈ ਕਿ worst-case depth 'ਤੇ ਵਿਚਾਰ ਕਰੋ।

ਪਹਿਲਾਂ correctness, ਫਿਰ performance

Quicksort ਦਾ worst-case ਸਮਾਂ O(n²) ਤੱਕ ਘਟ ਸਕਦਾ ਹੈ ਜਦ partitions ਬਹੁਤ unbalanced हों, ਪਰ ਇਹ performance ਦਾ ਮਸਲਾ ਹੈ—ਕੋਡ ਦੀ ਸਹੀਤਾ ਫੇਲ੍ਹ ਨਹੀਂ। reasoning ਦਾ ਉਦੇਸ਼ ਹੈ: ਜੇ partition ਤੱਤ ਰੱਖਦਾ ਹੈ ਅਤੇ pivot ਅਨੁਸਾਰ ਉਨ੍ਹਾਂ ਨੂੰ ਵੇਖ ਕੇ ਵੰਡਦਾ ਹੈ, ਤਾਂ subranges ਦੀ recursive sorting ਨਾਲ ਪੂਰਾ ਰੇਂਜ sorted ਨਿਕਲਦਾ ਹੈ।

ਸਬੂਤ-ਸਟਾਈਲ ਸੋਚ ਅਤੇ ਟੈਸਟਿੰਗ: ਇਹ ਇਕੱਠੇ ਕਿਵੇਂ ਕੰਮ ਕਰਦੇ ਹਨ

ਟੈਸਟਿੰਗ ਅਤੇ ਸਬੂਤ-ਸਟਾਈਲ reasoning ਦਾ ਮਕਸਦ ਇੱਕੋ ਹੀ ਹੈ—ਭਰੋਸਾ ਪ੍ਰਾਪਤ ਕਰਨਾ—ਪਰ ਉਹ ਵੱਖ-ਵੱਖ ਤਰੀਕਿਆਂ ਨਾਲ ਕਰਦੇ ਹਨ।

ਟੈਸਟ ਬੱਗ ਲੱਭਦੇ ਹਨ; reasoning ਬੱਗਾਂ ਦੀਆਂ ਕਲਾਸਾਂ ਬਾਹਰ ਰੱਖਦਾ ਹੈ

ਟੈਸਟਾਂ ਠੋਸ ਗਲਤੀਆਂ ਫੜਦੀਆਂ ਹਨ: off-by-one, ਛੁੱਟੇ ਕੇਸ, ਰਿਗ੍ਰੈਸ਼ਨ। ਪਰ ਟੈਸਟ ਸਿਰਫ ਇਨਪੁਟ ਸਪੇਸ ਨੂੰ ਸੈਂਪਲ ਕਰ ਸਕਦੇ ਹਨ। “100% coverage” ਦਾ ਅਰਥ ਹਰwerks ਰੂਪ ਵਿੱਚ “ਸਭ ਵਿਹੈਵਿਅਰ ਚੈਕ ਕੀਤੇ” ਨਹੀਂ ਹੁੰਦਾ; ਜ਼ਿਆਦਾਤਰ ਮਤਲਬ “ਸਭ ਲਾਈਨਾਂ ਚਲੀਆਂ।”

ਸਬੂਤ-ਸਟਾਈਲ ਸੋਚ (ਖ਼ਾਸ ਕਰਕੇ Hoare-ਸਟਾਈਲ reasoning) ਇੱਕ spec ਤੋਂ ਸ਼ੁਰੂ ਹੁੰਦੀ ਹੈ ਅਤੇ ਪੁੱਛਦੀ ਹੈ: ਜੇ ਇਹ preconditions ਸਹੀ ਹਨ, ਕੀ ਕੋਡ ਹਮੇਸ਼ਾਂ postconditions ਸਥਾਪਤ ਕਰੇਗਾ? ਜਦ ਤੁਸੀਂ ਇਹ ਚੰਗੀ ਤਰ੍ਹਾਂ ਕਰਦੇ ਹੋ, ਤਾਂ ਤੁਸੀਂ ਇਕ ਨਾ ਸਿਰਫ਼ ਇੱਕ ਬੱਗ ਲੱਭਦੇ ਹੋ—ਤੁਸੀਂ ਆਮਤੌਰ 'ਤੇ ਬੱਗਾਂ ਦੀ ਇੱਕ ਪੂਰੀ ਸ਼੍ਰੇਣੀ ਨੂੰ ਖਤਮ ਕਰ ਸਕਦੇ ਹੋ (ਜਿਵੇਂ "array access bounds ਵਿੱਚ ਰਹਿੰਦਾ ਹੈ" ਜਾਂ "ਲੂਪ partition property ਤੋੜਦਾ ਨਹੀਂ").

specifications ਚੰਗੀਆਂ ਟੈਸਟ ਮਾਮਲੇ ਬਣਾਉਂਦੀਆਂ ਹਨ

ਇੱਕ ਸਪਸ਼ਟ spec ਇੱਕ ਟੈਸਟ ਜਣਰੇਟਰ ਹੈ।

ਜੇ ਤੁਹਾਡੀ postcondition ਕਹਿੰਦੀ ਹੈ “ਆਉਟਪੁੱਟ sorted ਹੈ ਅਤੇ input ਦਾ permutation ਹੈ”, ਤਾਂ ਤੁਸੀਂ ਫੌਰاً ਟੈਸਟ ਵਿਚਾਰ ਪ੍ਰਾਪਤ ਕਰ ਲੈਂਦੇ ਹੋ:

• ਬਾਊਂਡਰੀਜ਼: ਖਾਲੀ ਲਿਸਟ, ਇੱਕ ਤੱਤ, ਪਹਿਲਾਂ ਤੋਂ sorted, reverse sorted।
• Invariants: ਅੰਤਰਿਮ ਗੁਣ (ਉਦਾਹਰਣ: partition ਵਿੱਚ ਅੰਤਰਿਮ ਪ੍ਰਾਪਰਟੀਆਂ)।
• ਗਲਤ ਇਨਪੁਟ: nulls, NaN, out-of-range indices, inconsistent comparators।

Spec ਦੱਸਦਾ ਹੈ ਕਿ "ਸਹੀ" ਕੀ ਹੈ, ਅਤੇ ਟੈਸਟ ਇਹ ਚੈੱਕ ਕਰਦੇ ਹਨ ਕਿ ਹਕੀਕਤ ਉਸਦੇ ਨਾਲ ਮਿਲਦੀ ਹੈ।

Property-based tests ਪ੍ਰੂਫ਼ ਅਤੇ ਉਦਾਹਰਣਾਂ ਦਾ عملي ਸੈਤ

Property-based testing ਸਬੂਤ ਅਤੇ ਉਦਾਹਰਣਾਂ ਦੇ ਵਿਚਕਾਰ ਪੱਖ ਹੀ। ਹੱਥ ਨਾਲ ਕੁਝ ਕੇਸ ਚੁਣਣ ਦੀ ਥਾਂ, ਤੁਸੀਂ ਗੁਣ ਦਰਜ ਕਰਦੇ ਹੋ ਅਤੇ ਇੱਕ ਟੂਲ ਬਹੁਤ ਸਾਰੇ ਇਨਪੁਟ ਜਣਰੇਟ ਕਰਦਾ ਹੈ।

Sorting ਲਈ ਦੋ ਸਧਾਰਨ ਗੁਣ ਲੰਬਾ ਫਾਇਦਾ ਦਿੰਦੇ ਹਨ:

• Sortedness: ਨਤੀਜਾ non-decreasing ਕ੍ਰਮ ਵਿੱਚ ਹੈ।
• Permutation: ਨਤੀਜਾ ਠੀਕ ਉਹੀ ਤੱਤ ਰੱਖਦਾ ਹੈ ਜੋ ਇਨਪੁੱਟ ਸੀ।

ਇਹ ਗੁਣ ਅਸਲ ਵਿੱਚ postconditions ਦੇ ਐਕਜ਼ੈਕਯੂਟਬਲ ਚੈਕ ਹਨ।

ਇੱਕ ਵਰਕਫਲੋ ਜੋ ਟੀਮਾਂ ਵਰਤ ਸਕਦੀਆਂ ਹਨ

ਇਕ ਹਲਕਾ ਰੂਪ ਜੋ ਵਧਦਾ ਹੈ:

1. ਪਹਿਲਾਂ spec ਲਿਖੋ (preconditions, postconditions, ਮੁੱਖ invariants)।
2. ਪਰੇਸ਼ਾਨ ਹਿੱਸਿਆਂ ਬਾਰੇ reasoning ਕਰੋ (ਲੂਪ, partitioning, recursion ਬਾਰਡਰ)।
3. Spec ਨੂੰ ਟੈਸਟਾਂ ਵਿੱਚ ਬਦਲੋ (ਬਾਊਂਡਰੀ ਕੇਸ + property-based checks)।
4. ਇਹਨਾਂ ਨੂੰ ਕੋਡ ਅਤੇ ਰਿਵਿਊਜ਼ ਨਾਲ ਇਕੱਠੇ ਰੱਖੋ, ਤਾਂ ਕਿ ਭਵਿੱਖੀ ਤਬਦੀਲੀਆਂ ਮੂਲ ਇਰਾਦਿਆਂ ਨੂੰ ਗੁਆਚ ਨਹੀਂ ਸਕਣ।

ਜੇ ਤੁਸੀਂ ਇਸਨੂੰ ਸੰਸਥਾਗਤ ਕਰਨਾ ਚਾਹੁੰਦੇ ਹੋ, ਤਾਂ “spec + reasoning notes + tests” ਨੂੰ ਆਪਣੇ PR ਟੈਂਪਲੇਟ ਜਾਂ ਕੋਡ-ਰੀਵਿਊ ਚੈਕਲਿਸਟ ਦਾ ਹਿੱਸਾ ਬਣਾਓ।

ਜੇ ਤੁਸੀਂ chat- ਆਧਾਰਿਤ ਕੋਡ ਜਨਰੇਸ਼ਨ ਵਰਕਫਲੋ ਵਰਤ ਰਹੇ ਹੋ, ਉਹੀ ਅਨੁਸ਼ਾਸਨ ਲਾਗੂ ਹੁੰਦਾ—ਸ਼ਾਇਦ ਹੋਰ ਵੀ ਜ਼ਰੂਰੀ। Koder.ai ਜਿਵੇਂ ਟੂਲਾਂ ਵਿੱਚ ਤੁਸੀਂ Planning Mode ਵਿੱਚ preconditions/postconditions ਪਿਨ ਕਰ ਸਕਦੇ ਹੋ ਪਹਿਲਾਂ, ਫਿਰ property-based ਟੈਸਟਾਂ ਜੋੜ ਸਕਦੇ ਹੋ। ਟੂਲ implementation ਤੇਜ਼ ਕਰਦਾ ਹੈ, ਪਰ spec ਹੀ ਇਹ ਦਿਖਾਉਂਦੀ ਹੈ ਕਿ “ਤੇਜ਼” ਕਦੋਂ “ਨਾਜੁਕ” ਵਿੱਚ ਨਹੀਂ ਬਦਲਣਾ।

ਸੁਰੱਖਿਆ ਸੋਚ: ਨੁਕਸਾਨ ਵਾਲੇ ਹਾਲਾਤਾਂ ਨਾਲ ਸਹੀਤਾ

ਸਹੀਤਾ ਸਿਰਫ਼ "ਕੋਡ ਸਹੀ ਮੁੱਲ ਲਿਆਉਂਦਾ" ਨਹੀਂ ਹੈ। ਸੁਰੱਖਿਆ ਸੋਚ ਇੱਕ ਵੱਖਰਾ ਸਵਾਲ ਪੁੱਛਦੀ ਹੈ: ਕਿਹੜੇ ਨਤੀਜੇ ਅਸਵੀਕਾਰਣੀਯ ਹਨ, ਅਤੇ ਅਸੀਂ ਉਨ੍ਹਾਂ ਨੂੰ ਕਿਵੇਂ ਰੋਕੀਏ—ਭਾਵੇਂ ਕੋਡ ਟੁੱਟ ਜਾਏ, ਨਾਜ਼ੁਕ ਤਰੀਕੇ ਨਾਲ ਵਰਤਿਆ ਜਾਵੇ, ਜਾਂ ਅਧੂਰਾ ਫੇਲ੍ਹ ਹੋਵੇ? ਅਮਲੀ ਤੌਰ 'ਤੇ, ਸੁਰੱਖਿਆ ਸਹੀਤਾ ਨਾਲ ਇੱਕ ਪ੍ਰਾਥਮਿਕਤਾ ਤਰਤੀਬ ਹੈ: ਕੁਝ ਫੇਲ੍ਹਿੰਗਸ ਫਿਕਰਤ (annoying) ਹੋ ਸਕਦੇ ਹਨ, ਹੋਰ ਵਿੱਤੀ ਨੁਕਸਾਨ, ਨਿੱਜਤਾ ਉਲੰਘਣਾ, ਜਾਂ ਸਰੀਰਕ ਨੁਕਸਾਨ ਪੈਦਾ ਕਰ ਸਕਦੇ ਹਨ।

hazards vs bugs: ਪ੍ਰਭਾਵ ਕਿਉਂ ਮਹੱਤਵਪੂਰਨ ਹੈ

ਇੱਕ bug ਕੋਡ ਜਾਂ ਡਿਜ਼ਾਇਨ ਵਿੱਚ ਦੋਸ਼ ਹੈ। ਇੱਕ hazard ਉਹ ਸਥਿਤੀ ਹੈ ਜੋ ਅਸਵੀਕਾਰਣੀਯ ਨਤੀਜੇ ਵੱਲ ਲੈ ਜਾ ਸਕਦੀ ਹੈ। ਇਕ bug ਇੱਕ ਸੰਦਰਭ ਵਿੱਚ ਨਿਰਦੋਸ਼ ਹੋ ਸਕਦਾ ਹੈ ਅਤੇ ਦੂਜੇ ਵਿੱਚ ਖਤਰਨਾਕ।

ਉਦਾਹਰਣ: ਫ਼ੋਟੋ ਗੈਲਰੀ ਵਿੱਚ off-by-one ਇੱਕ ਚਿੱਤਰ ਨੂੰ ਗਲਤ ਲੇਬਲ ਕਰ ਸਕਦਾ; ਉਸੇ ਗਲਤੀ ਦਾ ਦਵਾਈ ਦੀ ਮਾਤਰਾ ਗਣਨਾ ਵਿੱਚ ਹੋਣਾ ਮਰੀਜ਼ ਨੂੰ ਨੁਕਸਾਨ ਪਹੁੰਚਾ ਸਕਦਾ। ਸੁਰੱਖਿਆ ਸੋਚ ਤੁਹਾਨੂੰ ਕੋਡ ਦੇ ਬਿਹੇਵਿਅਰ ਨੂੰ ਨਤੀਜਿਆਂ ਨਾਲ ਜੋੜਨ 'ਤੇ ਮਜ਼ਬੂਰ ਕਰਦੀ ਹੈ—ਸਿਰਫ spec ਦਾ ਪਾਲਣ ਹੀ ਕਾਫ਼ੀ ਨਹੀਂ।

ਬੁਨਿਆਦੀ ਤਕਨੀਆਂ ਜੋ ਸਭ ਤੋਂ ਖਰਾਬ ਨਤੀਜੇ ਰੋਕਦੀਆਂ ਹਨ

ਭਾਰੀ ਫਾਰਮਲ ਮੈਥਡਾਂ ਦੀ ਲੋੜ ਨਹੀਂ; ਛੋਟੀ, ਦੋਹਰਾਏ ਜਾਣ ਵਾਲੀਆਂ ਪ੍ਰਥਾਵਾਂ ਤੁਰੰਤ ਫਾਇਦਾ ਦੇ ਸਕਦੀਆਂ ਹਨ:

• Fail-safe defaults: ਜੇ ਸਿਸਟਮ ਨਿਸ਼ਚਿਤ ਨਹੀਂ ਹੋ ਸਕਦਾ ਤਾਂ ਸੁਰੱਖਿਅਤ ਵਿਹੇਵਹ ਜ਼੍ਯਾਦਾ ਚੁਣੋ। ਉਦਾਹਰਣ ਵਜੋਂ, authorization ਚੈੱਕ ਫੇਲ ਹੋਣ 'ਤੇ access deny ਕਰੋ, allow ਨਾ ਕਰੋ।
• ਬਾਊਂਡਰੀ 'ਤੇ ਇਨਪੁੱਟ ਵੈਰੀਫਿਕੇਸ਼ਨ: ਯੂਜ਼ਰ ਇਨਪੁੱਟ, ਫਾਈਲ ਸਮੱਗਰੀ, ਨੈੱਟਵਰਕ ਡੇਟਾ ਨੂੰ ਅਨਟ੍ਰੱਸਟਿਡ ਮੰਨੋ। ਕਿਸਮਾਂ, ਰੇਂਜ, ਫਾਰਮੈਟ ਅਤੇ invariants ਨੂੰ ਜਲਦੀ validate ਕਰੋ।
• Limits ਅਤੇ timeouts: memory, request sizes, recursion depth, retries, ਅਤੇ execution time 'ਤੇ cap ਲਗਾਓ। ਬਹੁਤ ਸਾਰੀ ਘਟਨਾਵਾਂ “ਠੀਕ” ਕੋਡ ਨੂੰ ਬੇਹਦ ਅਸਮਾਨ ਇਨਪੁੱਟ ਮਿਲਣ ਤੇ ਘਟਦੇ ਹਨ।

ਇਹ ਤਕਨੀਆਂ Hoare-ਸਟਾਈਲ reasoning ਨਾਲ ਕੁਦਰਤੀ ਤੌਰ 'ਤੇ ਮਿਲਦੀਆਂ ਹਨ: ਤੁਸੀਂ preconditions ਸਪਸ਼ਟ ਕਰਦੇ ਹੋ (ਕਿਹੜੇ input ਮਨਜ਼ੂਰ ਹਨ) ਅਤੇ postconditions ਵਿਚ safety ਗੁਣ ਸ਼ਾਮਲ ਕਰੋ (ਕਿਹੜੀਆਂ ਚੀਜ਼ਾਂ ਕਦੇ ਵੀ ਨਹੀਂ ਹੋਣੇ ਚਾਹੀਦੀਆਂ)।

trade-offs: checks ਮੁਫ਼ਤ ਨਹੀਂ ਹੁੰਦੇ

ਸੁਰੱਖਿਆ-ਉਪਯੋਗ ਚੈੱਕਾਂ ਦੀ ਕੀਮਤ ਹੁੰਦੀ ਹੈ—CPU ਸਮਾਂ, ਜਟਿਲਤਾ, ਜਾਂ ਕਈ ਵਾਰ ਗਲਤ ਓਡੀਆਂ।

• ਪਰਫਾਰਮੈਂਸ vs checks: ਤੇਜ਼ ਰਾਹ ਕੀਮਤੀ ਹਨ, ਪਰ ਮਹੱਤਵਪੂਰਨ ਸਥਿਤੀਆਂ ਉੱਤੇ validation, rate limits, ਅਤੇ timeouts ਲਾਜ਼ਮੀ ਹਨ।
• ਕਠੋਰਤਾ vs usability: ਸਾਰੇ ਅਧੁਰੇ ਇਨਪੁੱਟ ਨੂੰ ਰੱਦ ਕਰਨਾ ਯੂਜ਼ਰ ਨੂੰ ਨਿਰਾਸ਼ ਕਰ ਸਕਦਾ ਹੈ; सब ਕੁਝ ਮਨਜ਼ੂਰ ਕਰਨਾ ਗੁੰਝਲਦਾਰ ਅਤੇ ਦੁਪੱਖੀ ਹੋ ਸਕਦਾ ਹੈ। ਇੱਕ ਕਾਰਗਰ ਸਮਝੌਤਾ ਹੈ “ਕੋਰ ਤੇ ਕਠੋਰ, ਬਾਹਰਲੇ ਹਿੱਸਿਆਂ 'ਤੇ ਮੁਆਫ਼ਦਾਰ”—ਇਸ ਦੇ ਨਾਲ ਲੋਗਿੰਗ ਅਤੇ edge-case ਘਟਨਾਵਾਂ ਦੀ ਮੱਪness ਰੱਖੋ।

ਸੁਰੱਖਿਆ ਸੋਚ ਸੁੰਦਰਤਾ ਨੂੰ ਸਾਬਤ ਕਰਨ ਦੀ ਨਿਗਾਹ ਨਹੀਂ ਰੱਖਦੀ; ਇਹ ਉਹਨਾਂ ਫੇਲ-ਮੋਡਾਂ ਨੂੰ ਰੋਕਦੀ ਹੈ ਜੋ ਤੁਸੀਂ ਬਰਦਾਸ਼ਤ ਨਹੀਂ ਕਰ ਸਕਦੇ।

Hoare-ਸਟਾਈਲ reasoning ਨੂੰ ਕੋਡ ਰਿਵਿਊਜ਼ ਵਿੱਚ ਲਾਗੂ ਕਰਨਾ

ਕੋਡ ਰਿਵਿਊਜ਼ ਉਹ ਥਾਂ ਹਨ ਜਿੱਥੇ correctness ਸੋਚ ਸਭ ਤੋਂ ਤੇਜ਼ ਨਤੀਜੇ ਦਿੰਦੀ ਹੈ, ਕਿਉਂਕਿ ਤੁਸੀਂ missing assumptions ਨੂੰ ਪ੍ਰੋਡਕਸ਼ਨ ਤੱਕ ਪਹੁੰਚਣ ਤੋਂ ਪਹਿਲਾਂ ਪਛਾਣ ਸਕਦੇ ਹੋ। Hoare ਦਾ ਮੁੱਖ ਇੰਤਜਾਮ—"ਕੀ ਸਚ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ ਪਹਿਲਾਂ" ਅਤੇ "ਕੀ ਗਾਰੰਟੀ ਕੀਤੀ ਜਾਂਦੀ ਹੈ ਬਾਅਦ"—ਸਮੀਖਿਆ ਪ੍ਰਸ਼ਨਾਂ ਵਿੱਚ ਆਸਾਨੀ ਨਾਲ ਬਦਲ ਜਾਂਦਾ ਹੈ।

Hoare ਆਈਡੀਏਜ਼ ਨੂੰ ਸਮੀਖਿਆ ਪ੍ਰਸ਼ਨਾਂ ਵਿੱਚ ਬਦਲੋ

ਜਦ ਤੁਸੀਂ ਕੋਈ ਬਦਲਾਅ ਪੜ੍ਹਦੇ ਹੋ, ਹਰ ਮੁੱਖ ਫੰਕਸ਼ਨ ਨੂੰ ਇੱਕ ਛੋਟੀ promise ਵਜੋਂ ਫਰੇਮ ਕਰੋ:

• Assumptions (preconditions): ਇਨਪੁਟ, ਸਟੇਟ, ਅਤੇ ਵਾਤਾਵਰਨ ਬਾਰੇ ਕੀ ਸੱਚ ਹੋਣਾ ਚਾਹੀਦਾ ਹੈ? (ਉਦਾਹਰਣ: “list non-empty”, “user authenticated”, “lock held”).
• Guarantees (postconditions): ਬਾਅਦ ਵਿੱਚ ਕੀ ਸੱਚ ਹੁੰਦਾ ਹੈ, ਰਿਟਰਨ ਕੀਮਤਾਂ ਅਤੇ ਸਾਈਡ-ਅਫੈਕਟ ਸਮੇਤ? (ਉਦਾਹਰਣ: "balance amount ਘਟ ਗਿਆ", "record exactly once insert ਹੋਇਆ").
• Invariants: ਲੂਪ, retry, ਜਾਂ multi-step workflow ਦੌਰਾਨ ਕੀ ਸਚ ਰਹਿਣਾ ਚਾਹੀਦਾ ਹੈ? (ਉਦਾਹਰਣ: "processed_count ≤ total", "debits ਦਾ ਜੋੜ ਅਜੇ ਤੱਕ credits ਦੇ ਜੋੜ ਦੇ ਬਰਾਬਰ").
• Failure behavior: ਗਲਤੀਆਂ ਤੇ ਕੀ ਹੁੰਦਾ—ਅਸੀਂ ਸਿਸਟਮ ਨੂੰ ਸੁਰੱਖਿਅਤ ਸਥਿਤੀ ਵਿੱਚ ਛੱਡਦੇ ਹਾਂ? partial updates rollback ਹੁੰਦੇ ਹਨ?

ਇੱਕ ਸਾਦਾ reviewer ਆਦਤ: ਜੇ ਤੁਸੀਂ pre/post conditions ਇੱਕ ਵਾਕ ਵਿੱਚ ਨਹੀਂ ਦੱਸ ਸਕਦੇ, ਤਾਂ ਕੋਡ ਨੂੰ ਸ਼ਾਇਦ ਸਪਸ਼ਟ ਬਣਾਉਣ ਦੀ ਲੋੜ ਹੈ।

ਖ਼ਤਰਨਾਕ ਫੰਕਸ਼ਨਾਂ ਲਈ "contract comments"

ਖ਼ਤਰਨਾਕ ਜਾਂ ਕੇਂਦਰੀ ਫੰਕਸ਼ਨਾਂ ਲਈ, 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 ਨੂੰ ਕੁਝ ਸਪਸ਼ਟ ਦੇਖਣ ਲਈ ਦਿੰਦੇ ਹਨ।

ਖ਼ਤਰਨਾਕ ਕੋਡ ਲਈ ਇੱਕ ਹਲਕਾ ਚੈਕਲਿਸਟ

ਜਦ ਤੁਸੀਂ ਹੇਠਾਂ ਦਿੱਤੀਆਂ ਚੀਜ਼ਾਂ ਦੇ ਨਾਲ ਸੌਦਾ ਕਰ ਰਹੇ ਹੋ ਤਾਂ ਵਧੇਰੇ ਸਪਸ਼ਟ ਹੋਵੋ:

• Parsing/validation (ਮਾਲਫਾਰਮਡ ਇਨਪੁੱਟ ਰਾਹ, ਬਾਊਂਡਰੀ ਕੇਸ)
• Concurrency (ਲੌਕ, races, idempotency, retries)
• Money/quotas (rounding, double-charging, overflow)
• Permissions (ਕੌਣ ਕੀ ਕਰ ਸਕਦਾ ਹੈ ਅਤੇ ਕਿਉਂ)

ਜੇ ਬਦਲਾਅ ਕਿਸੇ ਵੀ ਇਸ ਵਿੱਚ ਛੂਹਦਾ ਹੈ, ਪੁੱਛੋ: “preconditions ਕਿੱਥੇ enforce ਕੀਤੀਆਂ ਜਾਣਗੀਆਂ?” ਅਤੇ “ਫੇਲ੍ਹ ਹੋਣ 'ਤੇ ਅਸੀਂ ਕੀ ਗਾਰੰਟੀ ਦਿੰਦੇ ਹਾਂ?”

Formal tools ਕਦੋਂ ਵਰਤਣ—ਅਤੇ ਇੱਕ ਪ੍ਰਯੋਗੀ ਚੈਕਲਿਸਟ

Formal reasoning ਦਾ ਮਤਲਬ ਇਹ ਨਹੀਂ ਕਿ ਤੁਸੀਂ ਪੂਰੇ ਕੋਡਬੇਸ ਨੂੰ ਗਣਿਤੀ ਕਾਗਜ਼ ਬਣਾਉ। ਉਦੇਸ਼ ਉਨ੍ਹਾਂ ਹਿਸਿਆਂ 'ਤੇ ਵਧੇਰੀ ਨਿਸ਼ਚਿਤਤਾ ਲਗਾਉਣਾ ਹੈ ਜਿੱਥੇ “ਟੈਸਟਾਂ ਵਿੱਚ ਠੀਕ ਲੱਗਣਾ” ਕਾਫ਼ੀ ਨਹੀਂ।

Formal methods ਸਭ ਤੋਂ ਜ਼ਿਆਦਾ ਕਿੱਥੇ ਮਦਦਗਾਰ ਹਨ

ਉਹ ਛੋਟੇ, ਨਿਰਧਾਰਿਤ ਮਾਡਿਊਲਾਂ ਲਈ ਵਧੀਆ ਹਨ ਜਿਨ੍ਹਾਂ 'ਤੇ ਹੋਰ ਸਭ ਕੁਝ ਨਿਰਭਰ ਕਰਦਾ ਹੈ (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 ਨਤੀਜੇ ਮਿਲਦੇ ਹਨ ਜਦ ਤੁਸੀਂ ਉਨ੍ਹਾਂ ਨੂੰ ਮਿਲਾ ਕੇ ਵਰਤਦੇ ਹੋ:

• Types (ਤੇਜ਼ types systems, non-null, units/quantities): ਗ਼ਲਤ ਸਥਿਤੀਆਂ ਨੂੰ ਰੋਕਦੇ ਹਨ।
• Static analysis: ਸ਼ੱਕੀ ਰਾਹ, API ਗਲਤ ਵਰਤ, data races, tainted flows ਲੱਭਦਾ ਹੈ।
• Contracts (preconditions/postconditions, assertions): Hoare-ਸਟਾਈਲ ਬਿਆਨਾਂ ਦੀ executable ਵਰਜਨ।
• Model checking: state machines ਦੀ ਖੋਜ (protobuf ਲਈ ਭਲਾ, concurrency ਅਤੇ sequences ਲਈ ਵਧੀਆ)।
• Formal verification: ਸਭ ਤੋਂ ਉੱਚੀ ਇਹਤੀਯਾਤ ਲਈ machine-checked proofs।

ਤੁਸੀਂ ਕਿੰਨਾ ਡੂੰਘਾ ਜਾਣਾ ਚਾਹੀਦਾ?

ਫਾਰਮਲਤਾ ਦੀ ਡਿਗਰੀ ਤੈਅ ਕਰੋ risk × cost ਦੇ ਆਧਾਰ 'ਤੇ:

• Risk: ਪ੍ਰਭਾਵ × ਸੰਭਾਵਨਾ। ਉੱਚ risk ਵਧੇਰੇ ਗਾਰੰਟੀ ਮੰਗਦਾ ਹੈ।
• Cost: specify, prove, ਅਤੇ maintain ਕਰਨ ਦਾ ਸਮਾਂ।
• Change rate: ਤੇਜ਼ੀ ਨਾਲ ਬਦਲਦਾ ਕੋਡ formal ਰੱਖਣਾ ਮੁਸ਼ਕਲ ਹੁੰਦਾ; ਪਹਿਲਾਂ interfaces ਨੂੰ stable ਕਰੋ।
• टीਮ skills: ਜੇ proofs ਡਿਲਿਵਰੀ ਨੂੰ ਢਿਲ੍ਹਾ ਕਰਨਗੇ ਤਾਂ ਪਹਿਲਾਂ contracts ਅਤੇ static analysis ਨਾਲ ਸ਼ੁਰੂ ਕਰੋ।

ਅਮਲੀ ਤੌਰ 'ਤੇ, ਤੁਸੀਂ “formalness” ਨੂੰ ਕ੍ਰਮਵੱਧੀ ਰੂਪ ਵਿੱਚ ਜੋੜ ਸਕਦੇ ਹੋ: explicit contracts ਅਤੇ invariants ਨਾਲ ਸ਼ੁਰੂ ਕਰੋ, ਫਿਰ automation ਨਾਲ ਨਿਗਰਾਨੀ ਜਾਰੀ ਰੱਖੋ।

ਇੱਕ ਪ੍ਰਯੋਗੀ ਚੈਕਲਿਸਟ

ਇਸਨੂੰ planning ਜਾਂ ਕੋਡ ਰਿਵਿਊ ਵਿੱਚ “ਆਪਾਂ ਹੋਰ formal ਹੋਈਏ?” ਲਈ ਇੱਕ gate ਵਜੋਂ ਵਰਤੋ:

1. ਸਭ ਤੋਂ ਭਾਰੀ ਭਰੋਸੇਯੋਗ ਨੁਕਸਾਨ ਕੀ ਹੈ, ਅਤੇ ਕੌਣ ਨੁਕਸਾਨ ਭੁੱਗੇਗਾ (ਯੂਜ਼ਰ, ops, regulators)?
2. ਕੀ ਟੈਸਟ ਅੰਦੀ realistic edge cases ਅਤੇ states ਨੂੰ cover ਕਰ ਸਕਦੇ ਹਨ?
3. ਕੀ logic stateful, concurrent, ਜਾਂ invariants/boundaries 'ਤੇ ਭਾਰੀ ਹੈ?
4. ਕੀ ਅਸੀਂ public entry points ਲਈ ਸਪਸ਼ਟ preconditions/postconditions ਲਿਖ ਸਕਦੇ ਹਾਂ?
5. ਕੀ ਸਾਡੇ ਕੋਲ ਇੱਕ ਛੋਟਾ core ਹੈ ਜਿਸਨੂੰ ਅਸੀਂ ਵੱਧ ਡੂੰਘਾਈ ਨਾਲ isolate ਕਰਕੇ verify ਕਰ ਸਕੀਏ?
6. ਕਿਹੜਾ ਟੂਲ ਇੱਥੇ ਸਭ ਤੋਂ ਵਧੀਆ ਵਾਪਸੀ ਦਿੰਦਾ: stronger types, static analysis, contracts, model checking, ਜਾਂ proof?
7. ਅਗਲੇ ਤਿਮਾਹੀ ਵਿੱਚ ਕੀ ਤਬਦੀਲ ਹੋਵੇਗੀ, ਅਤੇ ਅਸੀਂ ਗਾਰੰਟੀਜ਼ ਨੂੰ ਕਿਵੇਂ drift ਤੋਂ بچਾ ਸਕਦੇ ਹਾਂ?

ਅੱਗੇ ਪੜ੍ਹਨ ਲਈ: design-by-contract, property-based testing, model checking for state machines, static analyzers for your language, ਅਤੇ ਸਭੂਤ-ਸੰਬੰਧੀ ਸੰਦਾਂ ਦੀ ਪ੍ਰਾਰੰਭਿਕ ਸਮੱਗਰੀ।