แนวคิดเรื่องความถูกต้องของ Tony Hoare: จากตรรกะสู่โค้ดที่ปลอดภัย

ทำไม “ความถูกต้อง” จึงมากกว่าแค่ “ดูเหมือนทำงาน”

เมื่อใครบางคนบอกว่าโปรแกรม “ถูกต้อง” มักหมายถึง: “ฉันรันมันไม่กี่ครั้งแล้วผลลัพธ์ดูถูก” นั่นเป็นสัญญาณที่มีประโยชน์—แต่ไม่ใช่ความถูกต้องในความหมายจริง ๆ โดยง่าย ความถูกต้องหมายความว่าโปรแกรมตรงตามสเปค: สำหรับทุกอินพุตที่อนุญาต มันต้องให้ผลลัพธ์ที่ต้องการและเคารพกฎเกี่ยวกับการเปลี่ยนแปลงสถานะ เวลา และการจัดการข้อผิดพลาด

สิ่งที่ซ่อนอยู่คือ “ตรงตามสเปค” ยากกว่าที่คิด

ทำไมความถูกต้องถึงยากจริง ๆ

อันดับแรก สเปคมักไม่ชัดเจน ข้อกำหนดของสินค้าอาจบอกว่า “เรียงลิสต์” แต่หมายถึงการเรียงที่คงลำดับ (stable) หรือไม่ ค่าเท่ากันจะจัดอย่างไร รายการว่างหรือข้อมูลที่ไม่ใช่ตัวเลขควรทำอย่างไร หากสเปคไม่บอก คนต่างกันจะตีความต่างกัน

ประการที่สอง กรณีขอบไม่ใช่เรื่องหายาก—แค่ทดสอบน้อยกว่า ค่าที่เป็น null, การล้น, ขอบเขต off-by-one, ลำดับการใช้งานที่ไม่ธรรมดา และความล้มเหลวจากภายนอกที่ไม่คาดคิด สามารถเปลี่ยน “ดูเหมือนทำงาน” ให้เป็น “ล้มเหลวในโปรดักชัน” ได้

ประการที่สาม ความต้องการเปลี่ยนได้ โปรแกรมอาจถูกต้องเมื่อเทียบกับสเปคของเมื่อวานแต่ไม่ถูกต้องเมื่อเทียบกับสเปคของวันนี้

จะคาดหวังอะไรจากบทความส่วนที่เหลือ

ผลงานใหญ่ของ Tony Hoare ไม่ได้กล่าวว่าเราควรพิสูจน์ทุกอย่างตลอดเวลา แต่เป็นแนวคิดที่ว่าเราสามารถเจาะจงได้มากขึ้นว่าโค้ดควรทำอะไร—และอธิบายด้วยวิธีเป็นระบบ

ในโพสต์นี้ เราจะตามสามเส้นเรื่องที่เชื่อมโยงกัน:

• ตรรกะ Hoare: การถกเถียงแบบน้ำหนักเบาและมีโครงสร้างโดยใช้ preconditions และ postconditions
• Quicksort: อัลกอริทึมที่คุ้นเคยซึ่งแสดงให้เห็นว่าก้าวเล็ก ๆ ที่ “ชัดเจน” (เช่น partition) ต้องคิดให้รอบคอบ
• ทัศนคติด้านความปลอดภัย: ความถูกต้องในฐานะความรับผิดชอบเชิงปฏิบัติเมื่อความล้มเหลวมีผลจริง

ทีมส่วนใหญ่จะไม่เขียนพิสูจน์เชิงรูปแบบทั้งหมด แต่แม้การคิดแบบ “สไตล์พิสูจน์” เพียงบางส่วนก็ช่วยให้การหาบั๊กง่ายขึ้น การรีวิวเฉียบคมขึ้น และพฤติกรรมชัดเจนขึ้นก่อนส่งโค้ด

Tony Hoare แบบย่อ: แนวคิดที่เข้าไปในโค้ดประจำวัน

Tony Hoare เป็นนักวิทยาการคอมพิวเตอร์ที่งานของเขาไม่คงอยู่แค่ในบทความหรือห้องเรียน เขาเคลื่อนระหว่างวิชาการและอุตสาหกรรม และใส่ใจคำถามเชิงปฏิบัติที่ทีมทุกทีมยังคงเผชิญ: เราจะรู้ได้อย่างไรว่าโปรแกรมทำสิ่งที่เราคิด—โดยเฉพาะเมื่อสิ่งที่เดิมพันสูง?

งานที่สำคัญสำหรับโพสต์นี้

บทความนี้เน้นแนวคิดของ Hoare ที่มักโผล่ในฐานข้อมูลโค้ดของทีมทั่วไป:

• ตรรกะ Hoare: วิธีอธิบายพฤติกรรมโปรแกรมโดยใช้ preconditions, postconditions, และ Hoare triple ที่รู้จักกัน {P} C {Q}
• loop invariants: นิสัยมีวินัยในการคิดเกี่ยวกับลูปเกินกว่าแค่ “ทำงานบนเครื่องฉัน”
• Quicksort (โดยเฉพาะขั้นตอน partition): ตัวอย่างที่ดังซึ่งการระบุความถูกต้องอย่างแม่นยำช่วยให้ชัดเจนมาก
• ทัศนคติด้านความปลอดภัย: ความถูกต้องไม่ใช่ฟีเจอร์ฟุ่มเฟือย; มันอาจเป็นความต่างระหว่างความไม่สะดวกกับอันตราย

สิ่งที่บทความนี้จะไม่ทำ

คุณจะไม่พบคณิตศาสตร์เชิงลึกมากมายที่นี่ และเราไม่พยายามทำพิสูจน์ Quicksort แบบตรวจสอบด้วยเครื่องทั้งหมด เป้าหมายคือทำให้แนวคิดเข้าถึงได้: มีโครงสร้างพอให้การคิดชัดขึ้น โดยไม่เปลี่ยนการทบทวนโค้ดให้กลายเป็นสัมมนาระดับบัณฑิต

ทำไมงานของเขาถึงมีผลกับการเขียนโปรแกรมปกติ

แนวคิดของ Hoare แปลงเป็นการตัดสินใจธรรมดา: สมมติฐานที่ฟังก์ชันพึ่งพา สิ่งที่มันรับประกันให้ผู้เรียก ข้อที่ต้องยังคงเป็นจริงในระหว่างลูป และวิธีสังเกตการเปลี่ยนแปลงที่ “เกือบถูกต้อง” ระหว่างการรีวิว แม้คุณจะไม่เขียน {P} C {Q} โดยชัดเจน การคิดในรูปแบบนั้นทำให้ API, การทดสอบ และการพูดคุยเกี่ยวกับโค้ดยาก ๆ ดีขึ้น

“ความถูกต้อง” หมายถึงอะไรในทางปฏิบัติ

มุมมองของ Hoare เข้มงวดกว่าการ “ผ่านตัวอย่างไม่กี่ตัว”: ความถูกต้องคือการปฏิบัติตามคำสัญญาที่ตกลงกัน ไม่ใช่แค่มองว่าถูกในการทดสอบเล็ก ๆ

ความต้องการ vs สเปค vs การทำงานจริง

• Requirements คือความต้องการของธุรกิจในภาษาธรรมดา (สิ่งที่ผู้มีส่วนได้ส่วนเสียต้องการ)
• Specification คือเวอร์ชันที่แม่นยำและตรวจสอบได้ของความต้องการนั้น (ฟังก์ชันต้องทำอะไร)
• Implementation คือโค้ดที่คุณเขียน (มันทำอย่างไร)

บั๊กมักเกิดเมื่อทีมข้ามขั้นตอนกลาง: ข้ามจาก requirements ไปเป็นโค้ดโดยตรง ทำให้ “คำสัญญา” คลุมเครือ

Partial correctness vs. total correctness

สองคำกล่าวต่างกันที่มักสับสน:

• Partial correctness: ถ้าโค้ดคืนค่า ผลลัพธ์ถูกต้อง
• Total correctness: โค้ดคืนค่าและผลลัพธ์ถูกต้อง (ดังนั้นการยุติเป็นส่วนของข้อเรียกร้อง)

สำหรับระบบจริง “ไม่จบ” อาจเป็นอันตรายเท่า ๆ กับ “จบด้วยคำตอบผิด”

ความถูกต้องขึ้นกับข้อสมมติอยู่เสมอ

คำกล่าวความถูกต้องไม่เคยเป็นสากล; มันพึ่งพาข้อสมมติเกี่ยวกับ:

• อินพุต (เช่น ลิสต์ใส่ในหน่วยความจำได้, สมาชิกเปรียบเทียบได้)\n- ข้อจำกัด (เช่น เวลาจำกัด, ขอบเขตจำนวนเต็ม)\n- สภาพแวดล้อม (เช่น ความขนาน, ความล้มเหลวของ I/O, การกำหนดค่า)

การระบุข้อสมมติให้ชัดเจนเปลี่ยน “ทำงานบนเครื่องฉัน” เป็นสิ่งที่ผู้อื่นสามารถคิดต่อได้

ตัวอย่างสเปคเล็ก ๆ

พิจารณาฟังก์ชัน sortedCopy(xs)

สเปคที่มีประโยชน์อาจเป็น: “คืนลิสต์ใหม่ ys ซึ่ง (1) ys เรียงจากน้อยไปมาก, และ (2) ys มีองค์ประกอบเหมือนกับ xs ทั้งจำนวนเท่าเดิม, และ (3) xs ไม่ถูกเปลี่ยน”

ตอนนี้ “ถูกต้อง” หมายถึงโค้ดทำตามสามข้อภายใต้ข้อสมมติที่ระบุไว้—ไม่ใช่แค่ผลลัพธ์ดูเรียงในการทดสอบเร็ว ๆ

พื้นฐานตรรกะ Hoare: preconditions, postconditions, triples

ตรรกะ Hoare เป็นวิธีพูดถึงโค้ดด้วยความชัดเจนเหมือนสัญญา: หากคุณเริ่มในสถานะที่ทำตามข้อสมมติบางอย่าง แล้วรันชิ้นโค้ดนี้ คุณจะจบในสถานะที่รับประกันบางอย่าง

สัญลักษณ์หลักคือ Hoare triple:

{precondition} program {postcondition}

Preconditions: สิ่งที่คุณสมมติ

Precondition ระบุสิ่งที่ต้องเป็นจริง ก่อน ชิ้นโค้ดทำงาน นี่ไม่ใช่สิ่งที่คุณหวัง แต่เป็นสิ่งที่โค้ด ต้องการ ให้เป็นจริง

ตัวอย่าง: สมมติฟังก์ชันคืนค่าเฉลี่ยของตัวเลขสองตัวโดยไม่มีการตรวจการล้น

• Precondition: a + b อยู่ในช่วงของชนิดจำนวนเต็ม\n- Program: avg = (a + b) / 2\n- Postcondition: avg เท่ากับค่าเฉลี่ยเชิงคณิตของ a และ b

ถ้า precondition ไม่เป็นจริง (มีความเป็นไปได้ของการล้น) สัญญา postcondition จะไม่ใช้บังคับอีกต่อไป Triple บังคับให้คุณพูดสิ่งนั้นออกมา

Postconditions: สิ่งที่คุณรับประกัน

Postcondition ระบุสิ่งที่จะเป็นจริง หลัง โค้ดทำงาน—โดยสมมติว่า precondition เป็นจริง Postcondition ที่ดีควรเป็นรูปธรรมและตรวจสอบได้ แทนที่จะพูดว่า “ผลลัพธ์ถูกต้อง” ให้ระบุว่า “ถูกต้อง” หมายถึงอะไร: เรียงแล้ว, ไม่เป็นลบ, อยู่ในขอบเขต, ไม่เปลี่ยนแปลงยกเว้นบางช่อง ฯลฯ

Assignment และการเรียงลำดับ (แบบไม่ล้นสัญลักษณ์)

ตรรกะ Hoare ขยายจากคำกล่าวเล็ก ๆ ไปจนถึงโค้ดหลายขั้นตอน:

• Assignment เปลี่ยนสถานะอย่างชัดเจน การคิดถามว่า: หลังจาก x = x + 1 แล้ว ข้อเท็จจริงอะไรเกี่ยวกับ x จะเป็นจริง?
• Sequencing (“ทำอันนี้ แล้วทำอันนั้น”) เชื่อมประกัน: หากขั้นตอน 1 ทำให้ precondition ของขั้นตอน 2 เป็นจริง บล็อกทั้งบล็อกก็เชื่อถือได้ง่ายขึ้น

ประเด็นไม่ใช่การโรย {} ทั่วทุกที่ แต่เพื่อทำให้เจตนาอ่านง่าย: ข้อสมมติชัดเจน ผลลัพธ์ชัดเจน และการสนทนา “ดูเหมือนทำงาน” ในการรีวิวน้อยลง

Loop invariants ที่ทีมจริง ๆ จะเขียนได้

Loop invariant คือประโยคที่เป็นจริง ก่อนลูปเริ่ม, ยังคงเป็นจริง หลังทุกการวนซ้ำ, และยังเป็นจริงเมื่อลูปจบ ความคิดเรียบง่ายแต่ได้ผลมาก: มันแทนที่ “ดูเหมือนทำงาน” ด้วยข้อเรียกร้องที่คุณตรวจสอบได้ในทุกขั้นตอน

ทำไม invariant จึงหยุดการคิดแบบคลุมเครือ

ถ้าไม่มี invariant การรีวิวมักเป็นแบบ: “เราทำซ้ำลิสต์และค่อย ๆ แก้” Invariant บังคับให้ชัดเจน: อะไรที่ถูกต้องแล้ว ณ จุดนี้ แม้ลูปยังไม่เสร็จ เมื่อคุณบอกได้ชัด ข้อผิดพลาดแบบ off-by-one และกรณีที่ขาดหายจะตรวจพบง่ายขึ้น เพราะจะมีช่วงที่ invariant ถูกทำลาย

เทมเพลต invariant ที่ใช้ซ้ำได้

โค้ดประจำวันส่วนใหญ่ใช้เทมเพลตที่เชื่อถือได้ไม่กี่แบบ

1) ขอบเขต / ความปลอดภัยของดัชนี

รักษาดัชนีให้อยู่ในช่วงปลอดภัย

• 0 \u003c= i \u003c= n\n- low \u003c= left \u003c= right \u003c= high

Invariant แบบนี้ดีสำหรับป้องกันการเข้าถึงเกินขอบและทำให้การคิดกับอาเรย์เป็นรูปธรรม

2) รายการที่ประมวลผลแล้ว vs ยังไม่ประมวลผล

แบ่งข้อมูลเป็นพื้นที่ “เสร็จ” และ “ยังไม่เสร็จ”\n

• “องค์ประกอบทั้งหมดใน a[0..i) ถูกตรวจแล้ว”\n- “ทุกรายการที่ย้ายไป result ตรงตามเงื่อนไขของ filter”

สิ่งนี้เปลี่ยนความคืบหน้าแบบคลุมเครือให้เป็นสัญญาชัดเจนเกี่ยวกับความหมายของ “ประมวลผลแล้ว”

3) Prefix ที่เรียงแล้ว (หรือ partitioned prefix)

พบทั่วไปในการเรียง, การรวม, และ partitioning

• “a[0..i) เรียงแล้ว”\n- “ทุกรายการใน a[0..i) มีค่า \u003c= pivot, และทุกรายการใน a[j..n) มีค่า \u003e= pivot”

แม้ทั้งอาร์เรย์ยังไม่เรียงเต็มที่ คุณก็ระบุได้ชัดว่าส่วนไหนเรียงแล้ว

การยุติในคำง่าย ๆ: มาตรวัดที่เล็กลง

ความถูกต้องไม่ได้มีแค่ความถูกต้องเชิงค่า; ลูปต้อง จบ ด้วย วิธีง่าย ๆ ในการโต้แย้งคือเรียกชื่อ มาตรวัด (variant) ที่ลดลงในแต่ละรอบและไม่สามารถลดลงได้ตลอดไป

ตัวอย่าง:\n\n- “n - i ลดลงทีละ 1”\n- “จำนวนรายการที่ยังไม่ประมวลผลลดลง”

ถ้าคุณหามาตรวัดที่ลดลงไม่ได้ คุณอาจค้นพบความเสี่ยงจริง: ลูปไม่สิ้นสุดในอินพุตบางประเภท

Quicksort เป็นกรณีศึกษาในการคิดเกี่ยวกับโค้ด

Quicksort ให้สัญญาง่าย ๆ: ให้ช่วงอาร์เรย์ จัดเรียงองค์ประกอบภายในให้ได้ลำดับไม่ลดลง โดยไม่สูญหายหรือสร้างค่าใหม่ รูปร่างอัลกอริทึมโดยรวมสรุปได้ง่าย:

1. เลือกค่าตัวกลาง (pivot)
2. Partition ช่วงให้ค่าที่ “น้อยกว่าตัวกลาง” ย้ายไปข้างหนึ่ง และค่าที่ “มากกว่าตัวกลาง” ย้ายไปอีกด้าน (พร้อมกฎสำหรับค่าที่เท่ากัน)
3. เรียกซ้อน บนช่วงย่อยซ้ายและขวา

มันเป็นตัวอย่างสอนที่ดีเพราะเล็กพอจะคิดในหัว แต่มีรายละเอียดพอที่จะโชว์ว่าการคิดแบบไม่เป็นทางการล้มเหลวได้อย่างไร Quicksort ที่ “ดูเหมือนทำงาน” ในการทดสอบสุ่มไม่กี่ครั้งอาจผิดในทางที่แสดงเฉพาะอินพุตหรือขอบเขตพิเศษ

กับดักที่ทำให้การทำตาม “เห็นอกเห็นใจ” พัง

ปัญหาบางอย่างทำให้เกิดบั๊กได้มากที่สุด:

• ค่าซ้ำ: ถ้า partition จัดการค่าเท่ากับ pivot อย่างไม่สอดคล้อง อาจเกิดการเรียกซ้อนไม่ยุบลง (ช่วงย่อยไม่เล็กลง) หรือ partition ที่ฝ่าฝืนกฎของมันเอง\n- ช่วงว่างหรือความยาวหนึ่ง: กรณีฐานต้องชัดเจน มิฉะนั้นคุณอาจเข้าถึงนอกขอบหรือเรียกซ้อนไม่รู้จบ\n- ดัชนี off-by-one: อัลกอริทึม partition มักใช้ตัวชี้สองตัว; การเปรียบเทียบหรือการเพิ่มที่ผิดพลาดเพียงครั้งเดียวอาจข้ามองค์ประกอบหรือสลับค่านอกช่วง

สิ่งที่ต้องพิสูจน์จริง ๆ

ในการโต้แย้งความถูกต้องแบบ Hoare คุณมักแยกการพิสูจน์เป็นสองส่วน:

• ความถูกต้องของ partition: หลังการ partition ทุกองค์ประกอบทางซ้ายเป็นไปตามความสัมพันธ์ที่เลือกกับ pivot ทุกองค์ประกอบทางขวาตรงกับความสัมพันธ์ตรงข้าม และผลลัพธ์เป็นการสลับองค์ประกอบของต้นฉบับ (permutation)
• ความถูกต้องของการเรียกซ้อน: การเรียกซ้อนทำงานบนช่วงที่เล็กลงอย่างชัดเจน (termination) และถ้าพวกมันเรียงช่วงย่อยของตนได้ ทั้งช่วงจะเรียงถูกต้อง

การแยกแบบนี้ทำให้การคิดจัดการได้: ทำให้ partition ถูกต้องก่อน แล้วสร้างความถูกต้องของการเรียงต่อจากมัน

ความถูกต้องของ partition: หัวใจของ Quicksort

ความเร็วมาจากรูทีนเล็ก ๆ ที่ดูเหมือนไม่สำคัญ: partition หาก partition ผิดแม้เล็กน้อย Quicksort อาจเรียงผิด, ทำงานไม่จบ, หรือแครชในกรณีขอบ

สัญญาของ partition (สิ่งที่มันต้องรับประกัน)

เราจะใช้ Hoare partition scheme คลาสสิก (ตัวชี้สองตัวเคลื่อนเข้าหากัน)

อินพุต: ชิ้นอาร์เรย์ A[lo..hi] และค่า pivot ที่เลือก (มักเป็น A[lo])

เอาต์พุต: ดัชนี p โดยที่:

• ทุกองค์ประกอบใน A[lo..p] เป็น \u003c= pivot\n- ทุกองค์ประกอบใน A[p+1..hi] เป็น \u003e= pivot

สังเกตสิ่งที่ไม่ได้สัญญา: pivot อาจไม่ลงที่ตำแหน่ง p และค่าที่เท่ากับ pivot อาจอยู่ทั้งสองข้าง นั่นไม่เป็นไร—Quicksort ต้องการแค่การแบ่งที่ถูกต้อง

Invariant สำคัญขณะสแกนและสลับ

เมื่ออัลกอริทึมเลื่อนตัวชี้สองตัว—i จากซ้าย, j จากขวา—การคิดที่ดีมุ่งที่สิ่งที่ “ล็อกไว้แล้ว” ชุด invariant ที่ใช้ได้จริงคือ:

• องค์ประกอบทั้งหมดใน A[lo..i-1] เป็น \u003c= pivot (ด้านซ้ายสะอาด)\n- องค์ประกอบทั้งหมดใน A[j+1..hi] เป็น \u003e= pivot (ด้านขวาสะอาด)\n- ทุกอย่างใน A[i..j] ยัง ไม่ถูกจัดประเภท (ยังต้องเช็ก)

เมื่อพบว่า A[i] \u003e= pivot และ A[j] \u003c= pivot การสลับรักษา invariant เหล่านี้และย่อส่วนกลางที่ยังไม่ถูกจัดประเภท

กรณีขอบที่ความถูกต้องต้องครอบคลุม

• ทั้งหมดเล็กกว่าพิช: i วิ่งไปทางขวา; partition ต้องยังยุติและคืน p ที่สมเหตุสมผล\n- ทั้งหมดใหญ่กว่าพิช: j วิ่งไปทางซ้าย; ข้อกังวลการยุติเช่นกัน\n- มีค่าเท่ามาก: หากการเปรียบเทียบไม่สอดคล้อง (\u003c กับ \u003c=) ตัวชี้อาจติดตั้ง Hoare scheme พึ่งพากฎที่สอดคล้องเพื่อให้ความคืบหน้าต่อเนื่อง\n- เรียงแล้ว / เรียงย้อน: ไม่ควรทำลายสัญญา แม้ประสิทธิภาพจะแย่ลง

มีหลาย scheme ของ partition (Lomuto, Hoare, three-way) กุญแจคือเลือกหนึ่งแบบ ระบุสัญญาของมัน และรีวิวโค้ดตามสัญญานั้นอย่างสม่ำเสมอ

การคิดเกี่ยวกับการเรียกซ้อน: กรณีฐานและการยุติ

การเรียกซ้อนเชื่อถือได้ง่ายเมื่อคุณตอบสองคำถามชัดเจน: มันหยุดเมื่อไหร่? และ ทำไมแต่ละขั้นตอนถึงถูกต้อง? การคิดแบบ Hoare ช่วยได้เพราะบังคับให้ระบุสิ่งที่ต้องเป็นจริงก่อนเรียก และสิ่งที่จะเป็นจริงหลังการคืน

กรณีฐานต้องถูกต้อง

ฟังก์ชันเรียกซ้อนต้องมีอย่างน้อยหนึ่ง base case ที่ไม่เรียกซ้อนอีกและยังคงสอดคล้องกับผลลัพธ์ที่สัญญาไว้

สำหรับการเรียง กรณีฐานทั่วไปคือ “อาร์เรย์ความยาว 0 หรือ 1 เรียงแล้ว” ที่นี่ “เรียงแล้ว” ควรถูกนิยามชัด: สำหรับความสัมพันธ์ ≤, ผลลัพธ์เรียงเมื่อสำหรับทุกดัชนี i \u003c j, มี a[i] ≤ a[j] (ความเสถียร—stability—เป็นคุณสมบัติแยกต่างหาก; Quicksort มักไม่เสถียรเว้นแต่คุณออกแบบให้เป็น)

ปัญหาย่อยต้องเล็กลง

ทุกขั้นตอนเรียกซ้อนควรเรียกบนอินพุตที่ เล็กลงอย่างชัดเจน การ “เล็กลง” นี้คือการพิสูจน์การยุติ: หากขนาดลดลงและไม่สามารถน้อยกว่า 0 ได้ คุณจะไม่เรียกซ้อนตลอดไป

การเล็กลงยังสำคัญต่อความปลอดภัยของสแต็ก โค้ดที่ถูกต้องก็อาจแครชได้ถ้าความลึกของการเรียกซ้อนมากเกินไป ใน Quicksort การแบ่งที่ไม่สมดุลอาจทำให้ความลึกลึก นี่คือการพิสูจน์การยุติพร้อมคำเตือนเชิงปฏิบัติให้พิจารณาความลึกแย่สุด

ความถูกต้องมาก่อนประสิทธิภาพ

ความแย่สุดของ Quicksort อาจกลายเป็น O(n²) เมื่อ partition ไม่สมดุล แต่เป็นปัญหาด้านประสิทธิภาพไม่ใช่ความถูกต้อง เป้าหมายการคิดคือ: สมมติว่า partition รักษาองค์ประกอบและแบ่งตาม pivot การเรียงย่อยถ้าถูกต้อง จะทำให้ทั้งช่วงเรียงถูกต้อง

การคิดแบบสไตล์พิสูจน์และการทดสอบ: พวกมันรวมกันอย่างไร

การทดสอบและการคิดแบบพิสูจน์มุ่งผลลัพธ์เดียวกัน—ความมั่นใจ—แต่ไปถึงเป้าต่างกัน

การทดสอบค้นพบบั๊ก; การคิดเชิงเหตุผลตัดหมวดบั๊กออก

การทดสอบจับข้อผิดพลาดเชิงคอนกรีตได้ดี: off-by-one, กรณีขอบ, การถอยหลัง แต่ชุดทดสอบสามารถสุ่มตัวอย่างช่องทางอินพุตเท่านั้น แม้ “ครอบคลุม 100%” ก็หมายถึง “บรรทัดทั้งหมดถูกเรียก” เป็นส่วนใหญ่ ไม่ได้หมายความว่าพฤติกรรมทั้งหมดถูกตรวจสอบ

การคิดแบบพิสูจน์ (โดยเฉพาะตรรกะ Hoare) เริ่มจากสเปคและถามว่า ถ้า preconditions เป็นจริง โค้ดจะทำให้ postconditions เป็นจริงเสมอหรือไม่ เมื่อทำดี ๆ คุณมักไม่เพียงแค่หา bug แต่สามารถตัดหมวดของบั๊กออกได้ (เช่น “การเข้าถึงอาร์เรย์อยู่ในขอบ” หรือ “ลูปไม่ทำลายคุณสมบัติ partition”)

สเปคผลิตกรณีทดสอบที่ดีกว่า

สเปคที่ชัดเจนเป็นตัวสร้างกรณีทดสอบ

ถ้า postcondition ระบุว่า “ผลลัพธ์เรียงและเป็น permutation ของอินพุต” คุณจะได้ไอเดียการทดสอบโดยอัตโนมัติ:

• ขอบ: ลิสต์ว่าง, หนึ่งองค์ประกอบ, เรียงแล้ว, เรียงย้อน\n- Invariant: สมบัติช่วงกลาง (เช่น partition เก็บองค์ประกอบ \u003c= pivot ทางซ้าย)\n- อินพุตไม่ถูกต้อง: null, NaN, ดัชนีนอกช่วง, comparator ไม่สอดคล้อง

สเปคบอกคุณว่า “ถูกต้อง” คืออะไร และการทดสอบตรวจดูว่าเรื่องจริงตรงกับสเปคนั้นหรือไม่

การทดสอบแบบ property-based เป็นสะพานเชิงปฏิบัติ

Property-based testing อยู่กึ่งกลางระหว่างพิสูจน์และตัวอย่าง แทนที่จะเลือกกรณีด้วยมือ คุณบอกคุณสมบัติแล้วให้เครื่องมือสร้างอินพุตจำนวนมาก

สำหรับการเรียงสองคุณสมบัติง่าย ๆ ให้ผลมาก:

• Sortedness: ผลเป็นลำดับไม่ลดลง\n- Permutation: ผลมีองค์ประกอบเหมือนอินพุต

คุณสมบัติเหล่านี้คือ postconditions ที่เขียนเป็นการเช็กเชิงปฏิบัติการได้

เวิร์กโฟลว์ที่ทีมใช้ได้จริง

กิจวัตรน้ำหนักเบาที่ขยายได้:\n\n1. เขียนสเปคก่อน (preconditions, postconditions, invariant สำคัญ)\n2. คิดผ่านส่วนที่ยุ่งยาก (ลูป, partition, ขอบของการเรียกซ้อน)\n3. แปลงสเปคเป็นการทดสอบ (กรณีขอบ + property-based checks)\n4. เก็บมันไว้ด้วยกัน ในโค้ดและการรีวิว เพื่อการเปลี่ยนแปลงในอนาคตจะไม่ละเมิดเจตนารมณ์เดิม

ถ้าต้องการทำให้เป็นสถาบัน ให้ทำ “สเปค + บันทึกการคิด + การทดสอบ” เป็นส่วนหนึ่งของเทมเพลต PR หรือเช็คลิสต์การรีวิว (ดูด้วย /blog/code-review-checklist)

ถ้าคุณใช้ workflow ที่สร้างโค้ดจากแชทแบบ vibe-coding หลักการเดิมก็ใช้ได้—อาจจำเป็นมากกว่า ใน Koder.ai ตัวอย่างเช่น คุณสามารถเริ่มใน Planning Mode เพื่อปักหมุด preconditions/postconditions ก่อนจะสร้างโค้ด จากนั้นวนซ้ำด้วย snapshots และ rollback ขณะเพิ่มการทดสอบแบบ property-based เครื่องมือช่วยให้การทำงานเร็วขึ้น แต่สเปคนี่แหละที่ป้องกัน “เร็ว” ให้ไม่กลายเป็น “เปราะบาง”

ทัศนคติด้านความปลอดภัย: ความถูกต้องที่มีผลจริงในโลก

ความถูกต้องไม่ได้หมายถึงแค่ “โปรแกรมคืนค่าถูก” เท่านั้น ทัศนคติด้านความปลอดภัยถามคำถามต่างออกไป: ผลลัพธ์ไหนที่ยอมรับไม่ได้ และเราจะป้องกันยังไง—แม้เมื่อโค้ดถูกกดดัน ถูกใช้งานผิด หรือบางส่วนล้มเหลว? ในทางปฏิบัติ ความปลอดภัยคือความถูกต้องที่มีการจัดลำดับความสำคัญ: ความล้มเหลวบางอย่างแค่รำคาญ แต่บางอย่างอาจเป็นการสูญเสียทางการเงิน การละเมิดความเป็นส่วนตัว หรืออันตรายด้านร่างกาย

อันตราย (hazards) vs บั๊ก: ทำไมผลกระทบสำคัญ

Bug คือข้อบกพร่องในโค้ดหรือการออกแบบ Hazard คือสถานการณ์ที่สามารถนำไปสู่ผลลัพธ์ที่ยอมรับไม่ได้ บั๊กเดียวกันอาจไร้ผลในบริบทหนึ่งแต่เป็นอันตรายในอีกบริบทหนึ่ง

ตัวอย่าง: off-by-one ในแกลเลอรี่อาจทำให้รูปสลับป้าย แต่ข้อผิดพลาดเดียวกันในเครื่องคำนวณปริมาณยาสามารถทำร้ายผู้ป่วยได้ ทัศนคติด้านความปลอดภัยบังคับให้เชื่อมพฤติกรรมโค้ดกับผลลัพธ์ ไม่ใช่แค่การปฏิบัติตามสเปค

เทคนิคง่าย ๆ ที่ป้องกันผลลัพธ์แย่ที่สุดได้

คุณไม่ต้องใช้วิธีเชิงรูปแบบหนัก ๆ เพื่อให้ได้ประโยชน์ด้านความปลอดภัยทันที ทีมสามารถนำแนวทางเล็ก ๆ ที่ทำซ้ำได้เข้ามา:

• ค่าเริ่มต้นที่ปลอดภัย: หากระบบไม่มั่นใจ ให้เลือกพฤติกรรมที่ปลอดภัยกว่า เช่น ปฏิเสธการเข้าถึงเมื่อการตรวจสอบสิทธิ์ล้มเหลว แทนที่จะ “อนุญาตเมื่อเกิดข้อผิดพลาด”\n- ตรวจอินพุตที่ขอบเขต: ปฏิบัติต่อข้อมูลผู้ใช้ ไฟล์ และข้อมูลเครือข่ายเป็นสิ่งไม่เชื่อถือ ตรวจชนิด ช่วง รูปแบบ และ invariant ตั้งแต่ต้น\n- ขีดจำกัดและ timeouts: จำกัดการใช้หน่วยความจำ ขนาดคำขอ ความลึกของการเรียกซ้อน การรีไทร และเวลาการทำงาน หลายเหตุการณ์เกิดจากโค้ด “ถูกต้อง” ที่รันกับอินพุตที่ไม่สมเหตุผล

เทคนิคเหล่านี้เข้าคู่กับตรรกะ Hoare ได้อย่างเป็นธรรมชาติ: คุณระบุ preconditions ให้ชัด (อินพุตแบบใดที่ยอมรับได้) และทำให้ postconditions รวมถึงสมบัติด้านความปลอดภัย (สิ่งที่ต้องไม่เกิดขึ้น)

การแลกเปลี่ยน: การตรวจสอบมีค่าใช้จ่าย

การตรวจเพื่อลดความเสี่ยงต้องแลก: เวลา CPU ความซับซ้อน หรือการปฏิเสธที่ผิดพลาดบางครั้ง

• ประสิทธิภาพ vs การตรวจ: เส้นทางเร็วมีค่า แต่ขอบเขตสำคัญควรตรวจ, จำกัด, และมี timeout\n- ความเข้มงวด vs การใช้งาน: การปฏิเสธอินพุตทั้งหมดที่ไม่สมบูรณ์อาจทำให้ผู้ใช้หงุดหงิด การยอมรับทุกอย่างอาจสร้างความกำกวมและช่องโหว่ ทางสายกลางที่ใช้ได้คือ “เข้มงวดที่แกนกลาง อดทนที่ขอบ” และเก็บล็อกวัดว่ากรณีขอบเกิดบ่อยแค่ไหน

ทัศนคติด้านความปลอดภัยคือเรื่องป้องกันโหมดล้มเหลวที่คุณไม่สามารถรับได้ มากกว่าการพิสูจน์ความสวยงามเชิงทฤษฎี

นำตรรกะ Hoare ไปใช้ในการรีวิวโค้ด

การรีวิวโค้ดคือที่ที่การคิดเรื่องความถูกต้องให้ผลเร็วที่สุด เพราะคุณสามารถจับข้อสมมติที่ขาดหายได้ก่อนบั๊กเข้าผลิต Tony Hoare’s move หลัก—ระบุ สิ่งที่ต้องเป็นจริงก่อน และ สิ่งที่จะเป็นจริงหลัง—แปลงเป็นคำถามรีวิวง่าย ๆ

แปลงไอเดีย Hoare เป็นคำถามในการรีวิว

เมื่ออ่านการเปลี่ยนแปลง ให้ลองกรอบฟังก์ชันสำคัญแต่ละตัวเป็นคำสัญญาเล็ก ๆ:

• สมมติฐาน (preconditions): อะไรต้องเป็นจริงเกี่ยวกับอินพุต สถานะ และสภาพแวดล้อม? (เช่น “ลิสต์ไม่ว่าง”, “ผู้ใช้ยืนยันตัวตนแล้ว”, “ล็อกถูกยึด”)\n- ข้อรับประกัน (postconditions): อะไรจะเป็นจริงหลังเสร็จ รวมถึงค่าที่คืนและผลข้างเคียง? (เช่น “ยอดคงเหลือลดลงตามจำนวน”, “ระเบียนถูกแทรกหนึ่งครั้งเท่านั้น”)\n- Invariant: อะไรต้องยังเป็นจริงตลอดลูป การลองใหม่ หรืองานหลายขั้นตอน? (เช่น “processed_count ≤ total”, “ผลรวมของเดบิตเท่ากับผลรวมของเครดิตชั่วคราว”)\n- พฤติกรรมเมื่อล้มเหลว: หากเกิดข้อผิดพลาด เราปล่อยระบบให้อยู่ในสถานะปลอดภัยหรือไม่ อัปเดตบางส่วนถูกย้อนกลับหรือไม่?

นิสัยง่าย ๆ ของผู้รีวิว: ถ้าคุณบอก pre/post ในหนึ่งประโยคไม่ได้ โค้ดน่าจะต้องการโครงสร้างที่ชัดเจนกว่า

“คอมเมนต์สัญญา” สำหรับฟังก์ชันสำคัญ

สำหรับฟังก์ชันที่เสี่ยงหรือเป็นศูนย์กลาง ให้เพิ่มคอมเมนต์สัญญาสั้น ๆ เหนือซิกเนเจอร์ เก็บให้เป็นรูปธรรม: อินพุต เอาต์พุต ผลข้างเคียง และข้อผิดพลาด

def withdraw(account, amount):
    """Contract:
    Pre: amount is an integer \u003e 0; account is active.
    Post (success): returns new_balance; account.balance decreased by amount.
    Post (failure): raises InsufficientFunds; account.balance unchanged.
    """
    ...

คอมเมนต์เหล่านี้ไม่ใช่พิสูจน์รูปแบบเครื่อง แต่ให้ผู้รีวิวสิ่งที่ต้องเทียบกับโค้ดได้ชัด

เช็คลิสต์น้ำหนักเบาสำหรับโค้ดเสี่ยง

ระบุให้ชัดเมื่อรีวิวโค้ดที่จัดการกับ:\n\n- การแยกวิเคราะห์/การตรวจ (เส้นทางอินพุตเสีย รูปแบบขอบ)\n- ความขนาน (ล็อก, การแข่ง, idempotency, การลองใหม่)\n- เงิน/โควตา (การปัด, เรียกเก็บสองครั้ง, การล้น)\n- สิทธิ์ (ใครทำอะไรได้และเพราะอะไร)

ถ้าการเปลี่ยนแตะเรื่องเหล่านี้ ให้ถาม: “preconditions คืออะไร และที่ไหนบังคับใช้?” และ “เรารับประกันอะไรได้แม้เมื่อเกิดความล้มเหลว?”

เมื่อใดควรใช้เครื่องมือเชิงรูปแบบ—และเช็คลิสต์เชิงปฏิบัติ

การให้เหตุผลเชิงรูปแบบไม่จำเป็นต้องแปลงทั้งโค้ดเบสเป็นกระดาษคณิต เป้าหมายคือใช้ความแน่นอนเพิ่มในจุดที่คุ้มค่า: จุดที่ “ดูดีในทดสอบ” ไม่พอ

ที่ใดเครื่องมือเชิงรูปแบบช่วยได้ที่สุด

เหมาะกับโมดูลเล็กที่สำคัญ (เช่น auth, กฎการชำระเงิน, permissions, safety interlocks) หรืออัลกอริทึมยุ่งที่ off-by-one แอบซ่อน (เช่น parser, scheduler, cache/eviction, โค้ดแบบ partition) กฎปฏิบัติที่มีประโยชน์: หากบั๊กอาจก่อให้เกิด อันตรายจริง, ความสูญเสียทางการเงินมาก, หรือ การเสียหายข้อมูลเงียบ คุณต้องการมากกว่าการรีวิว+การทดสอบธรรมดา

เครื่องมือที่ควรพิจารณา (ภาพรวม)

เลือกได้ตั้งแต่ “น้ำหนักเบา” ไปถึง “หนัก” และผลดีที่สุดมักมาจากการผสม:

• Types (ระบบชนิดเข้มขึ้น, non-null, หน่วย/ปริมาณ): ป้องกันสถานะไม่ถูกต้องเป็นกลุ่มใหญ่\n- Static analysis: หาทางผ่านที่น่าสงสัย การใช้ API ผิด การไหลของข้อมูลปนเปื้อน การแข่งข้อมูล\n- Contracts (pre/post, assertions): เวอร์ชันที่รันได้ของคำกล่าวแบบ Hoare\n- Model checking: สำรวจเครื่องสถานะ (เหมาะกับโปรโตคอล, ความขนาน)\n- Formal verification: พิสูจน์ที่ตรวจสอบโดยเครื่องสำหรับส่วนที่ต้องการความมั่นใจสูงสุด

ควรลงลึกแค่ไหน?

ตัดสินระดับความเป็นรูปแบบโดยพิจารณา:\n\n- ความเสี่ยง: ผลกระทบ × ความน่าจะเป็น สูงกว่าให้เหตุผลกับการรับประกันที่เข้มงวดกว่า\n- ค่าใช้จ่าย: เวลาที่ใช้ในการระบุ พิสูจน์ และบำรุงรักษา\n- อัตราการเปลี่ยนแปลง: โค้ดที่เปลี่ยนบ่อยยากจะรักษาความเป็นทางการไว้ได้; ควรทำให้ API เสถียรก่อน\n- ทักษะของทีม: เริ่มจาก contracts และ static analysis หากพิสูจน์เต็มรูปแบบทำให้ส่งมอบช้าเกินไป

ในทางปฏิบัติ คุณยังสามารถมอง “ความเป็นทางการ” เป็นสิ่งที่เพิ่มทีละน้อย: เริ่มจากสัญญาและ invariant ชัดเจน แล้วใช้การอัตโนมัติให้คุณซื่อสัตย์ ในทีมที่สร้างเร็วด้วย Koder.ai—ซึ่งสร้าง React front end, Go backend, และ schema Postgres ในรอบสั้น—snapshots/rollback และการส่งออกโค้ดช่วยให้วนซ้ำเร็วพร้อมกับบังคับใช้สัญญาผ่านการทดสอบและ static analysis ใน CI ของคุณ

เช็คลิสต์เชิงปฏิบัติ

ใช้เป็นเกต “เราควรเพิ่มความเป็นทางการไหม?” ในการวางแผนหรือรีวิว:\n\n1. ความล้มเหลวที่แย่ที่สุดคืออะไร และใครได้รับผลกระทบ (ผู้ใช้, ฝ่ายปฏิบัติการ, หน่วยงานควบคุม)?\n2. การทดสอบครอบคลุมกรณีขอบและสถานะสำคัญจริงไหม?\n3. ลอจิกมี state, concurrency, หรือหนักเรื่อง invariant/ขอบมากไหม?\n4. เราสามารถเขียน pre/post สำหรับจุดเข้าใช้งานสาธารณะได้ชัดไหม?\n5. เรามีแกนเล็กที่แยกออกเพื่อพิสูจน์ลึกกว่านี้ไหม?\n6. เครื่องมือใดให้ผลตอบแทนดีที่สุด: type, static analysis, contracts, model checking, หรือ proof?\n7. จะมีการเปลี่ยนแปลงอะไรในไตรมาสหน้า และเราจะรักษาคำรับประกันไม่ให้เลื่อนไหลอย่างไร?

หัวข้ออ่านต่อ: design-by-contract, property-based testing, model checking สำหรับเครื่องสถานะ, static analyzers สำหรับภาษาของคุณ, และวัสดุเบื้องต้นเกี่ยวกับ proof assistants และการระบุสเปคเชิงรูปแบบ