ตรวจสอบสเปกโครงการ: พบคำกล่าวอ้างเป็นเท็จ 5 จาก 18 ข้อ
นักพัฒนาสร้างเครื่องมือตรวจสอบข้อกำหนด 18 ข้อในโปรเจกต์ของตน พบเป็นจริง 9 ข้อ เป็นเท็จ 5 ข้อ และไม่ทราบผล 4 ข้อ โดยมีสาเหตุหลักจากการใช้คำศัพท์เฉพาะทางที่เกินจริง
ภาพประกอบจากคลังภาพสต็อก ไม่ใช่ภาพจากเหตุการณ์จริง
- ผู้พัฒนาสร้างเครื่องมืออัตโนมัติเพื่อตรวจสอบความถูกต้องของสเปก 18 ข้อในโปรเจกต์
- ผลลัพธ์พบว่ามีข้อความอ้างอิงเป็นเท็จถึง 5 ข้อ และไม่สามารถตัดสินได้อีก 4 ข้อ
- ข้อผิดพลาดส่วนใหญ่เกิดจากการใช้คำศัพท์ทางคณิตศาสตร์หรือคอมพิวเตอร์ที่แข็งแรงเกินไป
ข้อกำหนดหรือสเปกของโปรเจกต์นี้ตั้งใจเขียนขึ้นด้วยภาษาที่แม่นยำและเฉพาะเจาะจง โดยระบุคำว่าแผนผังนี้เป็นการส่งผ่านโครงสร้าง (homomorphism) หรือการทำงานเหล่านี้สร้างเป็นเลนส์ (lens) แทนที่จะใช้คำกว้างๆ ว่าแปลง X เป็น Y เนื่องจากคำที่แม่นยำเหล่านี้มีภาระผูกพันทางตรรกะในขณะที่คำกว้างๆ ไม่มี
ก่อนหน้านี้ไม่เคยมีใครตรวจสอบเลยว่าข้อผูกพันเหล่านี้ได้รับการปฏิบัติจริงหรือไม่ ผู้พัฒนาจึงสร้างระบบที่อ่านข้ออ้างอิงแต่ละข้อ เทียบเคียงกับคำนิยามจริง และให้ผลลัพธ์เป็นถูกต้อง ไม่ถูกต้อง หรือไม่ทราบผล จากตารางความถูกต้องทั้งหมด 18 แถว พบว่าถูกต้อง 9 ข้อ ไม่ถูกต้อง 5 ข้อ และไม่ทราบผล 4 ข้อ ซึ่งข้อที่เป็นเท็จทั้งหมดล้วนมาจากความผิดพลาดรูปแบบเดียวกัน คือการใช้คำศัพท์ที่แม่นยำในระดับความหมายที่เทียบเท่าคำพ้องความหมายแบบกว้างๆ
ภาพประกอบจากคลังภาพสต็อก ไม่ใช่ภาพจากเหตุการณ์จริง
ตัวอย่างที่ชัดเจนที่สุดคือ สเปกระบุว่าตัวเข้ารหัสเป็นการส่งผ่านโครงสร้างเข้าสู่สตริงไบต์ภายใต้การต่อสตริง (concatenation) ซึ่งเป็นคำกล่าวอ้างที่หนักแน่นและมีข้อผูกพันเดี่ยวคือ enc(a · b) = enc(a) ++ enc(b) ทว่าในความเป็นจริง ตัวเข้ารหัสสำหรับคู่ข้อมูลกลับทำงานในลักษณะ enc(pair(x, y)) = tag ++ enc(x) ++ enc(y) โดยมีไบต์แท็กอยู่ด้านหน้าเพื่อระบุประเภทข้อมูล
ไบต์เดียวนี้นี่เองที่ทำให้การเข้ารหัสสามารถถอดรหัสได้อย่างไม่กำกวม จึงเป็นงานที่สำคัญและตัดออกไม่ได้ แต่มันก็ส่งผลให้สมการดังกล่าวเป็นเท็จสำหรับทุกอินพุต ไม่มีคู่ข้อมูลใดที่ทั้งสองฝั่งเท่ากันอย่างแท้จริง สิ่งที่ตัวเข้ารหัสทำจริงๆ คือแผนผังที่มีคุณสมบัติฉีดเข้า (injective) และไร้คำนำหน้า (prefix-free) ซึ่งเป็นคุณสมบัติที่ระบบส่วนอื่นพึ่งพา แต่มันไม่ใช่การส่งผ่านโครงสร้างแต่อย่างใด
การใช้คำศัพท์เทคนิคเฉพาะทาง เช่น Homomorphism หรือ Lens ในเอกสารทางเทคนิค มักสร้างความเข้าใจผิดได้ง่ายหากไม่มีการตรวจสอบด้วยเครื่องมืออัตโนมัติ เนื่องจากมนุษย์มักอ่านผ่านๆ และตีความเข้าข้างบริบทที่ตนเองเข้าใจ ทำให้ข้อขัดแย้งในเอกสารที่อยู่ห่างกันหลายบรรทัดรอดพ้นจากการตรวจสอบด้วยสายตามานานหลายปี
ปัญหาอีกประเภทหนึ่งคือการใช้คำว่า DAG, strict order, covering relation และ transitive closure ราวกับว่าเป็นแนวคิดเดียวกัน ทั้งที่พวกมันมีความเกี่ยวข้องกันแต่ทดแทนกันไม่ได้ ตัวอย่างเช่น DAG ไม่มีความสมสัดส่วนแบบถ่ายทอด (transitive) ในขณะที่ covering relation ถูกออกแบบมาให้ไม่ถ่ายทอดเช่นกัน แต่เมื่อนำมาหาการปิดแบบถ่ายทอดจะได้ลำดับเดิมกลับมา เอกสารชิ้นนี้กลับเขียนประโยคเดียวที่ใช้ได้กับข้อความหนึ่งแต่เหมารวมว่าใช้ได้กับทั้งสี่แนวคิด
นอกจากนี้ ยังมีข้อความอ้างอิงที่ระบุถึงกฎการไปกลับ (round-trip laws) สำหรับเลนส์ที่ต้องเป็นไปตามเงื่อนไข get(put(v, s)) = v และ put(get(s), s) = s แต่ในเอกสารชุดเดียวกันในส่วนอื่นที่ห่างกันออกไป 130บรรทัด กลับระบุไว้อย่างชัดเจนว่าฟังก์ชันทั้งสองไม่ได้ประกอบกันแล้วได้ค่าเอกลักษณ์ (identity) ซึ่งความขัดแย้งเช่นนี้มักมองไม่เห็นผ่านการอ่านด้วยมนุษย์เนื่องจากสมองไม่สามารถจดจำเนื้อหาที่อยู่ห่างกันในเวลาเดียวกันได้
ที่มา: Dev.to
พบข้อมูลผิดพลาดในบทความนี้? แจ้งปัญหาบทความนี้
ความคิดเห็น
แสดงความคิดเห็น