สถานการณ์อันน่าหดหู่ของไลบรารีทดสอบแบบ Property-Based

 (stevana.github.io)
1 คะแนน โดย GN⁺ 2024-07-06 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Property-based testing แพร่จาก QuickCheck ไปยังหลายภาษา แต่ ณ กรกฎาคม 2024 ไลบรารีจำนวนมากยังให้การรองรับ การทดสอบแบบอิงสถานะ และ การทดสอบแบบขนาน ซึ่งถูกสรุปไว้แล้วตั้งแต่ปี 2009 ได้ไม่เพียงพอ
  • ช่องว่างหลักอยู่ที่ความสามารถในการตรวจสอบการเปลี่ยนสถานะตามลำดับด้วยโมเดล state machine และนำโมเดลเดียวกันกลับมาใช้ในการตรวจ ความเป็นไปได้ในการทำให้เป็นลำดับเชิงเส้น (linearisability) เพื่อหา race condition ในการรันแบบขนาน
  • ไลบรารีส่วนใหญ่ที่สำรวจไม่มีการทดสอบแบบอิงสถานะ หรือยังอยู่ในขั้นทดลอง ส่วนการทดสอบแบบขนานยิ่งพบได้น้อยกว่า โดย FsCheck, Gopter, RapidCheck, SwiftCheck, jsverify ฯลฯ ยังมี issue ที่เกี่ยวข้องค้างมาหลายปี
  • อิมพลีเมนต์ Haskell ประมาณ 400 บรรทัดจำลอง property-based testing แบบอิงสถานะและแบบขนาน และใช้ reference implementation แบบ fake ที่โปรแกรมเมอร์คุ้นเคยเป็นโมเดล แทนสเปก state machine แบบดั้งเดิม
  • fake ที่ผ่าน contract test สามารถนำกลับมาใช้ได้ ไม่ใช่แค่สำหรับตรวจสอบคอมโพเนนต์เดี่ยว แต่ยังใช้ใน integration test ที่เร็วและกำหนดผลลัพธ์ได้แน่นอน โดยฉีดเข้าไปแทน dependency จริง

ช่องว่างของฟีเจอร์ที่เกิดขึ้นหลัง QuickCheck

  • Property-based testing แพร่ไปยังชุมชนภาษาโปรแกรมหลายแห่งภายใต้คำขวัญว่า “อย่าเขียนเทสต์ แต่ให้สร้างเทสต์”
  • หน้า Wikipedia ของ QuickCheck ซึ่งเป็นไลบรารี Haskell ต้นฉบับ ระบุรายการการนำไปอิมพลีเมนต์ใหม่ในภาษาอื่น 57 รายการ
  • เปเปอร์ QuickCheck ฉบับแรก QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs ถูกนำเสนอที่ ICFP 2000 และซอร์สโค้ดทั้งหมดของอิมพลีเมนต์แรกอยู่ในภาคผนวกของเปเปอร์ เป็นโค้ดประมาณ 300 บรรทัด
  • QuickCheck ช่วงแรกทดสอบได้เฉพาะ ฟังก์ชันบริสุทธิ์ และในปี 2002 Testing monadic code with QuickCheck ได้วางรากฐานสำหรับจัดการโค้ดที่มีเอฟเฟกต์ เช่น mutable state, file I/O และ networking

การเกิดขึ้นของการทดสอบแบบอิงสถานะและแบบขนาน

  • Quviq AB ก่อตั้งในปี 2006 โดย John Hughes และ Thomas Arts และกรณีใช้งานช่วงแรกคือการทดสอบโปรเจกต์ Erlang ของ Ericsson
  • Erlang ไม่ใช่ภาษา functional แบบบริสุทธิ์ และมีการทำงานพร้อมกันเป็นเรื่องปกติ ดังนั้น monadic QuickCheck เดิมจึงยังไม่สะดวกพอสำหรับการใช้งาน
  • Erlang QuickCheck แบบ closed source ของ Quviq มีสองฟีเจอร์ที่ต่อมาขาดหายไปในอิมพลีเมนต์โอเพนซอร์สหลายตัว
    • property-based testing แบบอิงสถานะตามลำดับ ที่ใช้โมเดล state machine
    • การทดสอบแบบขนาน ที่นำโมเดล state machine แบบลำดับเดียวกันกลับมาใช้เพื่อตรวจจับ race condition
  • การทดสอบแบบอิงสถานะปรากฏในรูปแบบปัจจุบันใน QuickCheck testing for fun and profit (2007)
  • การทดสอบแบบขนานถูกอธิบายอย่างละเอียดใน Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009) โดยใช้ Linearizability: a correctness condition for concurrent objects (1990) ของ Herlihy และ Wing เป็นเทคนิคหลัก
  • โค้ดไลบรารีของ Quviq QuickCheck ไม่ได้ถูกเผยแพร่ในเปเปอร์ สิ่งที่เปิดเผยมีเพียง API และตัวอย่างเทสต์ที่ใช้ API นั้น

ผลสำรวจไลบรารีในปี 2024

  • state-of-the-art ในปัจจุบันคือ stateful testing ที่อิงโมเดล state machine และ parallel testing ที่ผสาน linearisability เข้ากับโมเดลแบบลำดับเดียวกัน
  • การสำรวจนี้สรุปจากการอ่านเอกสาร, issue tracker และซอร์สโค้ดบางส่วน ณ กรกฎาคม 2024
  • ไลบรารีจำนวนมากไม่มีการทดสอบแบบอิงสถานะ หรือรองรับอย่างจำกัด
    • QuickCheck(Haskell) มี issue สำหรับเพิ่มการทดสอบแบบอิงสถานะเปิดมาตั้งแต่ปี 2016
    • SwiftCheck ก็มี issue สำหรับเพิ่มการทดสอบแบบอิงสถานะเปิดมาตั้งแต่ปี 2016
    • jsverify มี issue สำหรับเพิ่มการทดสอบแบบอิงสถานะค้างมาตั้งแต่ปี 2015
    • proptest(Rust) ต้องอ้างอิง proptest-state-machine แยกต่างหาก
  • การรองรับการทดสอบแบบขนานพบได้น้อยยิ่งกว่า
    • Gopter เขียนไว้ใน README ว่า “No parallel commands … yet?” และมี issue จากปี 2017
    • FsCheck มี issue สำหรับเพิ่ม parallel support เปิดมาตั้งแต่ปี 2016
    • RapidCheck มี issue สำหรับเพิ่ม parallel support เปิดมาตั้งแต่ปี 2015
    • propcheck มี issue สำหรับเพิ่ม parallel testing ตั้งแต่ปี 2020
  • ตัวอย่างโอเพนซอร์สที่รองรับทั้งสองฟีเจอร์ ได้แก่ PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine, stateful-check เป็นต้น
  • แม้จะมีฟีเจอร์ขนาน ก็มีบางกรณีที่มีข้อจำกัด
    • คอมเมนต์ในซอร์สของการทดสอบแบบขนานของ QuickTheories ระบุว่า จำนวน end state ที่เป็นไปได้เพิ่มขึ้นอย่างรวดเร็วตามจำนวนคำสั่ง จึงมักต้องจำกัด command list ไว้ไม่เกิน 10 รายการ
    • ตัวอย่าง LevelDB และ Redis ของ ScalaCheck ถูกนำเสนอเป็นตัวอย่างแบบลำดับที่มี threadCount = 1
    • การรองรับ race condition ของ fast-check ดูเหมือนไม่ได้นำโมเดล state machine แบบลำดับกลับมาใช้ หรือใช้ linearisability เหมือนการทดสอบแบบขนานของ Quviq QuickCheck
  • ไม่พบตัวอย่างที่ชัดเจนของการเพิ่มฟีเจอร์ขนานในภายหลัง และหากไม่ได้สะท้อนในดีไซน์ API ตั้งแต่แรก อาจต้องออกแบบใหม่ค่อนข้างมาก

เหตุผลที่ฟีเจอร์แพร่กระจายช้า

  • เหตุผลที่ John Hughes เสนอมีสามข้อ
    • การทดสอบแบบอิงสถานะและแบบขนานไม่ได้มีประโยชน์เท่าการทดสอบฟังก์ชันบริสุทธิ์
    • การเขียนโมเดล state machine ต้องใช้วิธีคิดที่ต่างจากการทดสอบทั่วไป และต้องมีการให้ความรู้
    • open source เพียงอย่างเดียวไม่ได้นำไปสู่การใช้งานในอุตสาหกรรมได้ดีนัก ขณะที่ผลิตภัณฑ์ closed source พร้อมการฝึกอบรมและคอนซัลติ้งช่วยให้เกิดการนำไปใช้
  • แม้การทำ property-based testing เฉพาะชิ้นส่วนที่เป็นฟังก์ชันบริสุทธิ์จะให้ผลได้มาก แต่ระบบอุตสาหกรรมมี database, stateful protocol และ concurrent data structure จำนวนมาก ดังนั้น การทดสอบแบบอิงสถานะและแบบขนาน จึงสำคัญเกือบพอ ๆ กัน
  • สเปกแบบอิงสถานะไม่ได้ยากกว่าสเปกฟังก์ชันบริสุทธิ์เสมอไป
    • โมเดล key-value store สามารถไปได้ไกลพอสมควรด้วยเพียงลิสต์ของ key-value pair
    • ในกรณีของ LevelDB โมเดลแบบง่ายหา counterexample ที่ย่อแล้วเหลือ 17 ขั้นตอนได้ภายในไม่กี่นาที และหลัง Google แก้ไข ก็พบ counterexample 31 ขั้นตอนอีกครั้งภายในไม่กี่นาที
    • ปัญหาที่สองเป็นบั๊กใน background compaction process โดย compaction มีความสำคัญต่อการปรับปรุงประสิทธิภาพการอ่านและการเรียกคืน disk space แต่ไม่ได้ถูกรวมไว้อย่างชัดเจนในโมเดล
  • แม้ closed source อาจช่วยการนำไปใช้ในอุตสาหกรรม แต่ประเมินว่าไม่ได้ช่วยการนำ open source ไปใช้
  • หากต้องการทำซ้ำผลลัพธ์ในเปเปอร์โดยไม่มีไลเซนส์ Quviq QuickCheck ต้องทำ reverse engineering จำนวนมาก จึงมองว่าแทบเป็นไปไม่ได้

ข้อเสนอ: อิมพลีเมนต์ขนาดเล็กที่เปิดเผย และสเปกที่เขียนง่าย

  • แนวทางปรับปรุงมีสองข้อ
    • จัดหาอิมพลีเมนต์โอเพนซอร์สขนาดสั้นของ property-based testing แบบอิงสถานะและแบบขนาน เช่นเดียวกับอิมพลีเมนต์ QuickCheck ดั้งเดิมประมาณ 300 บรรทัด
    • ลด ภาระในการเขียนสเปก โดยนำแนวคิด mock และ test double ที่โปรแกรมเมอร์คุ้นเคยอยู่แล้วกลับมาใช้ แทน state machine
  • เพื่อทดสอบสมมติฐานนี้ แสดงให้เห็นสองอย่าง
    • อิมพลีเมนต์ property-based testing แบบอิงสถานะและแบบขนานด้วยโค้ดประมาณ 400 บรรทัด
    • ใช้ in-memory reference implementation หรือก็คือ fake เป็นโมเดล แทน state machine

สรุปการทดสอบแบบ property-based testing ล้วน ๆ

  • ในการทดสอบฟังก์ชันบริสุทธิ์ จะสร้างอินพุตและตรวจสอบว่าเอาต์พุตของฟังก์ชันมีความสัมพันธ์บางอย่างกับอินพุตหรือไม่
  • ตัวอย่างเช่น reverse สามารถทดสอบด้วย property อย่าง reverse (reverse xs) == xs สำหรับลิสต์ใด ๆ xs
  • โดยค่าเริ่มต้น QuickCheck จะสร้างการทดสอบ 100 รายการ และเมื่อพบความล้มเหลวจะ shrink อินพุตเพื่อเสนอ counterexample ที่เล็กที่สุด
  • property ที่ผิดอย่าง reverse xs == xs จะถูกย่อให้เหลือ counterexample ขั้นต่ำอย่าง [0,1]
  • รูปแบบ property ที่พบบ่อย ได้แก่ inverse, idempotency, associativity, axiom ของ abstract data type, metamorphic property เป็นต้น
    • inverse: deserialise (serialise i) == i
    • idempotency: sort (sort xs) == sort xs
    • associativity: (i + j) + k == i + (j + k)

การทดสอบแบบ property-based testing ที่อิงสถานะ

  • คอมโพเนนต์ที่มีสถานะไม่ได้ให้เอาต์พุตเดียวกันเสมอไปเมื่อได้รับอินพุตเดียวกัน
    • ผลลัพธ์ของ incr ครั้งแรกของ counter กับผลลัพธ์ของ incr ครั้งที่สองจะแตกต่างกันตามสถานะก่อนหน้า
    • database และ file system ก็มีประวัติอินพุตก่อนหน้าที่ส่งผลต่อเอาต์พุตถัดไปเช่นกัน
  • หากการทดสอบฟังก์ชันบริสุทธิ์จัดการกับอินพุตเดี่ยว การทดสอบที่อิงสถานะจะสร้าง ลำดับอินพุต เพื่อตรวจสอบว่าระบบเปลี่ยนแปลงอย่างไรตามเวลา
  • โมเดลแสดงเป็น fake รูปแบบ m -> i -> (m, o)
    • คำนวณโมเดลถัดไปและเอาต์พุต o จากสถานะโมเดลก่อนหน้า m และอินพุต i
    • เปรียบเทียบเอาต์พุตของระบบจริงกับเอาต์พุตของ fake ในแต่ละขั้น
    • หากไม่ตรงกัน จะ shrink ลำดับอินพุตเพื่อหา counterexample ขนาดเล็ก

  • ตัวอย่าง Counter

    • ใช้ Haskell counter ที่ใช้ตัวแปร global mutable เป็นเป้าหมายทดสอบ
    • incr เพิ่มค่า counter และ get อ่านค่าปัจจุบัน
    • โมเดลใช้เพียง Counter Int ตัวเดียวก็พอ และอินสแตนซ์ StateModel นิยามสถานะเริ่มต้น Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal และ command generator
    • หากใส่บั๊กแบบ incr42Bug ที่ไม่เพิ่มค่าเมื่อค่า counter เป็น 42 QuickCheck จะพบความล้มเหลวหลังทดสอบ 66 รายการ และ shrink 29 ครั้ง ก่อนเสนอ counterexample ขั้นต่ำคือ increment 43 ครั้งแล้ว Get
    • หากไม่ reset global counter จริงระหว่างการทดสอบ โมเดลจะเริ่มจาก 0 เสมอ แต่ counter จริงจะคงสถานะจากการทดสอบก่อนหน้า ทำให้เกิด mismatch

  • อินเทอร์เฟซของไลบรารีที่อิงสถานะ

    • อินเทอร์เฟซ StateModel มองระบบที่ทดสอบเป็น black box โดยให้ command เป็นอินพุตและ response เป็นเอาต์พุต
    • ส่วนประกอบหลักคือ Command state, Response state, initialState, runFake, runReal, generateCommand
    • ส่วนประกอบ optional มีดังนี้
      • Reference: ใช้เมื่อ command ภายหลังต้องอ้างถึง resource ที่ response ก่อนหน้าสร้างขึ้น เช่น file handle
      • PreconditionFailure: แสดงความล้มเหลวของ precondition เช่น ป้องกันไม่ให้ read จาก handle ที่ไม่ใช่ไฟล์ที่เปิดอยู่
      • CommandMonad: ค่าเริ่มต้นคือ IO แต่สามารถใช้ monad อื่นได้
      • monitoring, commandName: ใช้สำหรับ coverage และสถิติ
    • ตอนสร้าง command ไม่สามารถสร้างค่าจริงอย่าง file handle ได้ จึงสร้าง symbolic reference ในรูป Var Int แล้วแทนที่ด้วย reference จริงระหว่างรัน
    • หลัง shrink จะลบ command ที่ละเมิด precondition หรือใช้ symbolic reference นอก scope

  • ตัวอย่าง Circular buffer

    • ทดสอบ circular queue ที่เขียนด้วย C ผ่าน Haskell FFI และเขียนโมเดลเป็น queue แบบอิงลิสต์อย่างง่าย
    • implementation ของ C ไม่มี error checking จึงอาจคืน memory ที่ยังไม่ได้ initialize เมื่อ get จาก empty queue
    • implementation จริงมีประสิทธิภาพด้วย circular index แต่ไม่ได้ correct อย่างชัดเจน ส่วน fake มีประสิทธิภาพน้อยกว่าแต่ใช้เพื่อการทดสอบจึงไม่เป็นปัญหา
    • เนื่องจาก new คืนค่า queue reference โมเดลจึงจัดการ queue หลายตัวด้วย Map (Var Queue) FQueue
    • ตอนแรกขาด precondition สำหรับการ put ลงใน full queue จึงเมื่อใส่ 0, 1 ลงใน queue ขนาด 1 แล้ว get โมเดลคาดว่าเป็น FIFO จึงควรได้ 0 แต่โค้ด C คืนค่า 1
    • นี่ไม่ใช่บั๊กของ implementation แต่เป็นการตกหล่นของ precondition ในโมเดล จึงแก้โดยเพิ่ม precondition QueueIsFull
    • การที่ command Size หายไปจาก generator ถูกเปิดเผยจากผลลัพธ์ coverage และเมื่อเพิ่มเข้าไปก็พบ bug ในการคำนวณขนาด queue
    • เมื่อใส่ item หนึ่งรายการใน queue ขนาด 1 แล้วเรียก Size ค่าที่คาดคือ 1 แต่ค่าจริงคือ 0 และมีการเสนอให้แก้โดยกำหนดขนาด buffer ภายในใน new เป็น n + 1
    • หลังจากนั้น abs(q->inp - q->outp) % q->size ผ่านสำหรับขนาด 1 แต่ล้มเหลวอีกครั้งที่ขนาด 2 และการแก้ไขสุดท้ายคือ (q->inp - q->outp + q->size) % q->size

  • ปริศนาถังน้ำ Die Hard 3

    • แก้ปริศนาการทำให้น้ำมีปริมาณพอดี 4L ด้วยถังน้ำ 3L และ 5L โดยใช้การทดสอบที่อิงสถานะ
    • แม้จะไม่มี implementation จริง เพียงรันโมเดลกับ fake ก็สามารถทำให้การทดสอบล้มเหลวเมื่อไปถึงสถานะหนึ่ง และได้ action sequence ที่ถูก shrink แล้ว
    • sequence ที่เสนอหลังทดสอบ 199 รายการและ shrink 11 ครั้ง มีลำดับดังนี้
      • เติมถังน้ำ 5L ให้เต็ม
      • เทจากถัง 5L ไปยังถัง 3L
      • เทน้ำในถัง 3L ทิ้ง
      • เทจากถัง 5L ไปยังถัง 3L อีกครั้ง
      • เติมถังน้ำ 5L ให้เต็ม
      • เทจากถัง 5L ไปยังถัง 3L
    • trace แสดงสถานะระหว่างทาง ทำให้ตรวจสอบกระบวนการที่เหยือกใบใหญ่มีน้ำ 4L ได้

การทดสอบแบบ property-based แบบขนาน

  • บั๊กของ concurrent code ทำซ้ำและตรวจสอบการแก้ไขได้ยาก เพราะ thread interleaving เปลี่ยนไปในแต่ละครั้งที่รัน
  • เป้าหมายคือทำให้ผู้ใช้สามารถทดสอบแบบขนานได้เหมือนการทดสอบตามสถานะแบบลำดับ โดยไม่ต้องเขียนโค้ดทดสอบเพิ่มเติมมากนัก
  • ในตัวอย่าง counter หาก incr ทำ readIORef แล้วตามด้วย writeIORef แบบไม่เป็น atomic จะเกิด race condition เพราะสอง thread เขียนทับ increment ของกันและกัน
  • การทดสอบแบบขนานจะรวบรวมเวลาที่ command ถูก invocation และเวลาที่ response กลับมาระหว่างการรัน เพื่อสร้าง concurrent history แล้วตรวจสอบว่า history นั้นสามารถอธิบายได้ด้วย sequential interleaving ใด
  • หากมี interleaving ใดสักแบบที่ตรงกับโมเดลแบบลำดับ ก็ถือว่า history นั้น linearise ได้และตัดสินว่า correct
  • หากไม่มี sequential interleaving ใดอธิบาย response จริงได้ จะถือว่าเป็นผลลัพธ์แบบ non-linearisable

  • การสร้าง command แบบขนานและการ shrink

    • โปรแกรมแบบขนานถูกแทนด้วย ParallelCommands และ Fork หลายตัว โดย command ภายในแต่ละ Fork จะถูกรันแบบขนาน
    • implementation ตัวอย่างครอบคลุมการรันแบบ single, double และ triple threaded execution
    • ในการรันแบบขนาน สถานะของโมเดลที่เป็นไปได้อาจเปลี่ยนไปตาม interleaving เช่น Fork [Write "a" "foo", Write "a" "bar"]
    • โมเดลแบบขนานทำการสร้าง command และ shrink โดยอิงจาก ชุดของ state ไม่ใช่ state เดียว
    • parallelSafe ตรวจสอบว่า precondition ยังคงอยู่ครบในทุก permutation ของ command ภายใน Fork
    • ตัวอย่างเช่น หาก Write "a" และ Delete "a" อยู่ใน fork เดียวกัน command หนึ่งอาจทำลาย precondition ของอีก command ได้
    • ในขั้นตอน shrink จะเหลือไว้เฉพาะ command ที่ยังรักษา precondition และ scope ของ symbolic reference ไว้ได้

  • การรันแบบขนานและการตรวจสอบ linearisability

    • การรันแบบขนานจะบันทึก event Invoke และ Ok ของแต่ละ command ลงใน history
    • หาก response มี reference ใหม่ จะขยาย environment ด้วย atomic counter เพื่อเลี่ยงการชนกันของหมายเลข reference ระหว่าง thread
    • แจกแจง interleaving ที่เป็นไปได้ทั้งหมดจาก history เป็น Rose tree
    • linearisable ตรวจสอบว่า path ใดใน tree นี้ทำให้ response ตรงกับโมเดล runFake แบบลำดับหรือไม่
    • สุดท้ายแล้วการทดสอบแบบขนานนำโมเดลแบบลำดับกลับมาใช้ซ้ำ ดังนั้นผู้ใช้เขียนโมเดลแบบลำดับก่อน แล้วเพิ่มโค้ดเพียงเล็กน้อยก็ได้การทดสอบแบบขนาน

  • ตัวอย่าง Parallel counter

    • โค้ดที่เพิ่มเพื่อเปิดใช้การทดสอบแบบขนานของ counter มีเพียง instance ParallelModel Counter และ property เท่านั้น
    • หากใช้ incrRaceCondition แบบไม่เป็น atomic จะพบ race condition
    • แม้ใน test case ที่เล็กกว่าจะยังมี race อยู่ แต่ถ้าความล้มเหลวทำซ้ำไม่ได้เพราะ interleaving อื่น QuickCheck อาจมองว่า test case ที่เล็กกว่านั้นผ่านและหยุด shrink
    • วิธีแก้ที่ถูกต้องคือ deterministic thread scheduler และบทความวิจัยเรื่องการทดสอบแบบขนานใช้วิธีนี้
    • implementation ตัวอย่างใช้ workaround ที่ง่ายกว่า โดยใส่ sleep สั้น ๆ รอบการ read/write ของ shared memory เพื่อเพิ่มโอกาสให้เกิด interleaving เดิม
    • sleep ไม่ได้จำเป็นเพื่อหา race แต่จำเป็นเพื่อทำให้ counterexample ของ race ที่พบมีขนาดเล็กลง
    • หลังเพิ่ม sleep แล้ว ตัวอย่างโต้แย้งขั้นต่ำถูกย่อเหลือ ParallelCommands [Fork [Incr,Incr],Fork [Get]]

  • ตัวอย่าง Process registry

    • ใช้ระบบคล้าย Erlang process registry เป็นตัวอย่าง ซึ่ง spawn thread แล้ว register, lookup, unregister และ kill ThreadId ด้วยชื่อ
    • โมเดลแบบลำดับติดตาม thread id ที่ถูกสร้าง, pair ของ name-thread ที่ถูก register และ thread id ที่ถูก kill
    • Register และ Unregister อาจล้มเหลวได้ จึงใช้ Either ErrorCall () ใน response
    • ข้อมูล error location ของ implementation จริงถูกลบด้วย abstractError เพื่อให้ตรงกับ fake
    • monitoring แสดง coverage ของ RegisterFailed, RegisterSucceeded, UnregisterFailed, UnregisterSucceeded
    • เมื่อตั้งใจใส่บั๊กให้ register เขียนทับ registry เดิม จะได้ตัวอย่างโต้แย้งแบบลำดับที่ไม่สามารถ unregister "e" ซึ่ง register ไปแล้วได้
    • ในการทดสอบแบบขนานจะได้ตัวอย่างโต้แย้งที่ยาวกว่า และเมื่อใช้ SleepyIORef จะ shrink เหลือรูปแบบ Fork [Register "b" (Var 0), Register "c" (Var 0)]
    • ปัญหาคือ race ที่ thread อื่นสามารถแทรกเข้ามาได้ระหว่างหลังตรวจสอบด้วย readRegistry กับก่อนเรียก atomicModifyIORef
    • หลังใช้ global lock กับ register, unregister, kill แล้ว การทดสอบแบบขนานผ่าน

โมเดลที่ใช้ Fake และการทดสอบแบบ Integration

  • แทนที่จะใช้ state machine specification with post-conditions แบบดั้งเดิม จะใช้ fake แบบ in-memory เป็น reference implementation
  • บทความปี 2019 ของ Edsko de Vries บทความปี 2019 ถูกแนะนำว่าเป็นบทความแรกที่เสนอวิธีนำ fake ไป implement บนข้อกำหนด state machine แบบอิง post-condition
  • fake คล้ายกับ mock จึงถูกเสนอว่าเป็นแนวทางที่เข้าถึงง่ายกว่าสำหรับโปรแกรมเมอร์ที่ไม่คุ้นเคยกับ formal specification
  • fake ยังมีข้อดีที่สามารถใช้แทนคอมโพเนนต์ที่พึ่งพาในการทดสอบแบบ integration ได้ด้วย
    • ไม่จำเป็นต้องเริ่มหรือ enable dependency จริง
    • สามารถสร้าง integration test ที่เร็วกว่าและ deterministic กว่าได้
  • ปัญหาที่ fake อาจผิดพลาดได้จะจัดการด้วย contract test
  • เนื่องจาก state-based และ parallel property-based test ตรวจสอบความสอดคล้องระหว่าง fake กับ implementation จริง fake จึงทำหน้าที่เป็น dependency ที่ผ่านการ contract-tested แล้ว

  • แยกการทดสอบกับการ deploy ด้วย Queue fake

    • อินเทอร์เฟซ queue IQueue มี iNew, iPut, iGet, iSize
    • implementation จริงเชื่อมต่อ C queue wrapper ตามเดิม
    • implementation แบบ fake เก็บสถานะของโมเดลไว้ใน IORef และอัปเดตผ่าน fNew, fPut, fGet, fSize
    • คอมโพเนนต์ถูกเขียนให้ทำงานกับอินเทอร์เฟซ IQueue q
    • ในการทดสอบใช้ instance fake และในการ deploy ใช้ instance real
    • ใช้ state-based property-based test เพื่อวางสมมติฐานว่า fake faithful ต่อ real

  • File system fake

    • อินเทอร์เฟซ file system IFileSystem h มี iMkDir, iOpen, iWrite, iClose, iRead
    • implementation จริงใช้ file system จริงใต้ /tmp/qc-test
    • fake ถูก implement เป็น FakeFS แบบ in-memory ที่มี directory set, file content map, open handle map และ next handle
    • fOpen, fWrite, fClose, fRead model precondition failure เช่น busy file, directory ที่ไม่มีอยู่ และ handle ที่ถูกปิดแล้ว
    • หากทดสอบแล้วว่า fake file system faithful ต่อ file system จริง คอมโพเนนต์ที่พึ่งพา file system ก็สามารถทดสอบ integration ด้วย fake และสลับเป็น file system จริงตอน deploy ได้
    • หากเกิดบั๊กเมื่อสลับเป็น real ต้องตรวจสอบว่า mismatch ระหว่าง fake กับ real ผ่าน state-based property-based test มาได้อย่างไร

  • ระบบคอมโพเนนต์ที่ใหญ่ขึ้น

    • ระบบที่ A พึ่งพา B และ B พึ่งพา C ก็ขยายด้วยวิธีเดียวกันได้
    • กำหนดอินเทอร์เฟซให้แต่ละคอมโพเนนต์
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • กลยุทธ์การทดสอบมีดังนี้
      • ตรวจสอบ C ด้วย state-based และ parallel property-based test เพื่อให้ได้ fake C ที่ผ่าน contract test แล้ว
      • ใน integration test ของ B ใช้ fake C
      • ในการทดสอบ A ใช้ fake B ที่ใช้ fake C
    • วิธีนี้ขยายตามแพตเทิร์นเดิมไปยังคอมโพเนนต์หรือบริการจำนวนมากขึ้นได้

สรุป

  • state-based และ parallel property-based testing สามารถ implement ได้ด้วยโค้ดราว 400 บรรทัด ซึ่งมีขนาดเทียบได้กับ implementation แรกของ QuickCheck ที่ยังไม่มี shrinking ซึ่งมีราว 300 บรรทัด
  • เมื่อใช้ fake เป็นโมเดล การเขียนข้อกำหนดสำหรับ state-based และ parallel test จะอยู่ในรูปแบบที่คุ้นเคยกว่า และสามารถนำกลับมาใช้ซ้ำเพื่อทดสอบระบบที่ใหญ่ขึ้นแบบ compositional ได้
  • หากคอมมูนิตี้ของแต่ละภาษายังทดลองต่อไป ก็ยังมีโอกาสปรับปรุงสถานะของไลบรารี property-based testing ให้ดีขึ้นได้

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-07-06
ความคิดเห็นจาก Hacker News

  • สงสัยว่าตอนนี้มี coverage-based fuzzing แล้วและใน Go ก็รองรับได้ดี ถ้าไม่ใช้ไลบรารี property-based testing จะพลาดอะไรไปบ้าง
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    ดูจากฟัซซ์เทสต์ด้านล่างและการตรวจสอบเงื่อนไขคงตัวที่สอดคล้องกันแล้ว ก็รู้สึกว่าแทบจะเหมือน property test อยู่แล้วไม่ใช่หรือ
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • ความแตกต่างระหว่าง property-based testing กับ fuzzing โดยมากเป็นการจัดกลุ่มแบบคร่าว ๆ ตามบรรยากาศมากกว่า
      แม้จะมีความต่างจริง แต่เส้นแบ่งค่อนข้างพร่าเลือน และการแยกให้ชัดว่าอะไรคือ fuzzing อะไรคือ property-based testing ก็ไม่ใช่เรื่องสำคัญมากนัก
      เทสต์ที่รันเร็วและมี assertion ละเอียดมักนับเป็น property-based testing ส่วนที่รันนานและเน้นหาการ crash มักเป็น fuzzing และระหว่างนั้นก็ค่อนข้างก้ำกึ่ง
      https://hypothesis.works/articles/what-is-property-based-tes...
    • coverage-based fuzzing กับ property-based testing สามารถผสานกันได้อย่างดี
      ตอนอยู่ที่ Google เคยมีเครื่องมือภายในที่รวมสองอย่างนี้ไว้ด้วยกันและมันดีมาก คุณเขียน property-based test ได้ตามปกติ แล้วตอนรัน test framework จะคอมไพล์แบบพิเศษเพื่อเก็บ coverage และปรับอินพุตแบบสุ่มเพื่อเพิ่ม coverage แน่นอนว่ามันรันแบบอัตโนมัติเต็มรูปแบบบนคลัสเตอร์หลายเครื่อง
      property-based testing แบบดั้งเดิมมักทำเป็นเพียงไลบรารี จึงไม่ได้มี ข้อมูล coverage ไว้คอยชี้นำการสร้างอินพุตแบบสุ่มเสมอไป
    • เพราะกำลัง assert คุณสมบัติอยู่ จึงมองว่าเข้าข่าย property-based testing ตามนิยาม เช่น “โหนดทุกตัวที่มีระดับมากกว่า 1 จะมีลูกสองตัว”
      เพียงแต่แล้วแต่ไลบรารี คุณอาจได้ฟีเจอร์อำนวยความสะดวกเพิ่มอีกพอสมควร หนึ่งในสิ่งที่มีแล้วดีคือ shrinking และดูส่วน “Shrinking” ได้ที่นี่: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      combinator สำหรับประกอบ generator ก็ยอดเยี่ยมมาก และบางไลบรารีก็มีชุดค่าที่ “แย่” ซึ่งรู้กันอยู่แล้วว่าสามารถทำให้เกิดพฤติกรรมผิดปกติได้
    • ไม่ค่อยแน่ใจว่า fuzz test ของ Go ต่างจากเนื้อหาในบทความที่ลิงก์ไว้อย่างไร แต่บทความนั้นบอกว่า fuzzer ที่แท้จริงควรรันเป็นวันหรือเป็นสัปดาห์ และควรเลือก property-based testing แทน fuzzing แทบทุกครั้ง
      อยากถอยออกมาหนึ่งก้าวแล้วตั้งคำถามเชิงเมตาเกี่ยวกับการทดสอบมากกว่า คือ การทดสอบที่ผ่าน หมายถึงโค้ดนั้นสำเร็จจริงหรือไม่ และในทางกลับกันจริงหรือไม่? มีตรงไหนในสัญญาของ Go ที่ระบุไว้หรือไม่ว่า ถ้าใส่อินพุตเดิมให้โค้ดเดิม ก็ต้องได้เอาต์พุตเดิม?
    • จากมุมมองของ API สิ่งที่ได้เป็นหลักคือ ไลบรารี combinator สำหรับสร้างโครงสร้างข้อมูลแบบสุ่มตามที่ต้องการ
      ถ้าจัดการกับชนิด Arbitrary ที่แทนเซตของอ็อบเจ็กต์แบบสุ่ม ก็จะเขียนฟังก์ชันที่นำกลับมาใช้ซ้ำได้สำหรับสร้างอินพุตทดสอบได้ง่ายมาก ไลบรารีแบบนั้นก็น่าจะใช้ร่วมกับเฟรมเวิร์ก fuzzing ของ Go ได้ค่อนข้างง่ายเช่นกัน
      ถึงอย่างนั้นก็ยังรู้สึกว่า combinator ทั่วไปอย่าง map, filter, chain, oneOf อาจจะใช้งานได้ไม่ค่อยลื่นนัก เลยกำลังเขียนไลบรารี property testing ตัวใหม่สำหรับ JavaScript เป้าหมายคือทำให้ใช้งานง่ายขึ้น แต่ตอนนี้ยังอยู่ในขั้นทดลองและยังไม่เปิดเผยสู่สาธารณะ

  • clojure.spec.alpha ถือว่าให้ประสบการณ์ที่ยอดเยี่ยมไม่ว่าจะใช้ร่วมกับ test.check หรือไม่ก็ตาม แต่พอได้ลองใช้ hypothesis ของ Python แล้วกลับแย่มาก
    Hypothesis ดูเหมือนจะไม่สามารถจัดการชุดข้อมูลที่เรียบง่ายแต่ “ใหญ่” ได้ตามข้อจำกัดเชิงออกแบบ และคำว่า “ใหญ่” ในที่นี้จริง ๆ ก็ไม่ได้ใหญ่ขนาดนั้น [0] มันทรมานมากจนสุดท้ายถอด Hypothesis และการทดสอบแบบ generative ออกจาก test suite ภาษา Python ที่ใช้ในที่ทำงานไปเลย
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • ในกรณีนี้ ฟังดูไม่ใช่ว่า Hypothesis จัดการชุดข้อมูลขนาดใหญ่ไม่ได้ แต่เป็นเพราะมันปฏิเสธเคสที่ถูกย่อ (shrunk) แล้วจำนวนมาก
      Hypothesis พยายามย่อจำนวนเต็มที่สร้างขึ้นมาให้เป็น 0 เพื่อดูว่าบั๊กยังเกิดที่ 0 หรือไม่ แต่ตัวทดสอบไม่ได้ล้มเหลวเพราะมี 0 อยู่ กลับปฏิเสธเคสนั้นแทน สำหรับเคสเล็ก ๆ มันเป็นแค่ความไม่มีประสิทธิภาพ แต่สำหรับเคสใหญ่ ๆ มันมากพอจน Hypothesis ยอมแพ้
      มีคนในเธรดนั้นเสนอให้ใช้กลยุทธ์สร้างอินสแตนซ์แบบอื่นที่ไม่สามารถสร้าง 0 ได้ แทนที่จะสร้างค่าที่ตัว shrinker ของ Hypothesis ชอบที่สุดแล้วค่อยปฏิเสธ ก็เปลี่ยนเป็นไม่สร้างมันตั้งแต่ต้น ไม่รู้ว่าได้ลองวิธีนั้นหรือยัง
      และก็อยากรู้เหมือนกันว่า clojure.spec.alpha จัดการเรื่องนี้ต่างออกไปอย่างไร
      คอมเมนต์ของ mjaniczek ใน https://news.ycombinator.com/item?id=40876437 ยกกรณีนี้ขึ้นมาเป็นข้อเสียของแนวทางแบบ Hypothesis
      ใจความคือ “ตัว generator จะกลายเป็นตัวแยกวิเคราะห์รายการไบต์ที่ตอนนี้อาจล้มเหลวได้ จึงมีความไม่มีประสิทธิภาพเพิ่มขึ้นเล็กน้อย และผู้ใช้ก็สามารถสร้าง generator แปลก ๆ ที่ตัว shrinker ภายในย่อได้ไม่สมบูรณ์ ถึงอย่างนั้น ในสามแนวทางนี้ประสบการณ์ของนักพัฒนาก็ยังดีที่สุด…”
      แน่นอนว่าเจ้าตัวคงไม่เห็นด้วยว่าตัวเองเขียนเทสต์แบบ “แปลก ๆ”
    • สิ่งที่ชอบใน spec ของ Clojure คือมันจัดสภาพแวดล้อมรอบ ๆ ได้ง่ายมาก แต่พอย้ายไป Elixir ถ้าจะเขียนเทสต์แบบนั้นกลับต้องลงไปใช้ propEr ซึ่งเป็นไลบรารี Erlang เก่า ๆ น่าผิดหวังพอสมควร
    • ตัวอย่างที่อยู่ใน GitHub issue ใช้ filter ในแบบที่ก่อปัญหาให้ตัวเอง
      ถ้าสุ่มสร้างขึ้นมาก่อนแล้วค่อยกรองให้ตรงกับคุณสมบัติบางอย่าง ก็แทบไม่ต่างจากการ ขูดลอตเตอรี่ ระหว่างกระบวนการสร้าง

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

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

  • ใน Rust ใช้ proptest เขียน การทดสอบคุณสมบัติแบบมีสถานะ ค่อนข้างบ่อย และโดยทั่วไปการเขียนเองก็ง่ายพอสมควร
    ตัวอย่างที่ไม่ธรรมดาซึ่งพบบั๊กได้ 6 จุดอยู่ที่ https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    การทดสอบแบบขนานอาจมีประโยชน์ในบางครั้ง แต่บ่อยครั้งแค่รันทดสอบจำนวนมากแบบขนานก็มักจะง่ายกว่า

    • ใน Rust เขียนการทดสอบคุณสมบัติแบบแมนนวลเยอะมาก และโดยมากหน้าตาจะประมาณนี้
      ระดับบนสุดใช้ความสุ่มจริง แล้วด้านล่างวางลูปซ้อนหลายชั้นเพื่อไล่จากกรณีความซับซ้อนต่ำไปสู่กรณีที่ซับซ้อนสูง จากนั้นสร้างและพิมพ์ seed ที่จะป้อนให้ตัวสร้างเลขสุ่มเทียมแบบกำหนดได้แน่นอน ถ้าการทดสอบล้มเหลว ก็แค่คัดลอก seed ของข้อผิดพลาดมาแปะเพื่อทำซ้ำกรณีที่ล้มเหลวได้
      รู้สึกว่า การทดสอบคุณสมบัติแบบแมนนวล แบบนี้เร็วกว่า ยืดหยุ่นกว่า และโดยรวมยุ่งยากน้อยกว่ากรอบงานหรือไลบรารีใด ๆ
      แต่สำหรับการทดสอบ concurrent ที่แข็งแกร่งจริง ๆ แนะนำไลบรารี AWS Shuttle อย่างมาก (https://github.com/awslabs/shuttle) มันสามารถหาสภาวะแข่งกันที่ซับซ้อนจนแทบไม่น่าเชื่อได้ ผมยังเขียนทิวทอเรียลสั้น ๆ ไว้ด้วย: https://grantslatton.com/shuttle
      ที่ AWS ก็ใช้ไลบรารีนี้เพื่อตรวจสอบความถูกต้องของไฟล์ซิสเต็มแบบคัสตอมที่เขียนขึ้นเพื่อรัน AWS S3

  • ลองไล่อ่านงานวิจัย “Testing Telecoms Software with Quviq QuickCheck” ที่ลิงก์ไว้แบบเร็ว ๆ แต่ยังไม่เห็นคำตอบชัด ๆ ของคำถามว่า “ทำไมงานแบบมีสถานะแบบนี้ถึงไม่ควรทำเอง?”
    ต้นฉบับชี้ไปที่ส่วนนี้ด้วยโมเดลคู่คีย์-ค่า ของ key-value store แต่ผมไม่เข้าใจว่าทำไมถึงเขียน state machine เองไม่ได้ หรือทำไมต้องมีเฟรมเวิร์ก สัปดาห์ก่อนที่ทำงานผมก็ทำแบบนี้ตรง ๆ เพื่อทดสอบการโต้ตอบกับไฟล์ซิสเต็ม และสุดท้ายก็ลงเอยประมาณ type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
    จากนั้นคุณสมบัติก็จะเป็น “เมื่อกำหนดรายการคำสั่งนี้มาแล้ว ...” StateModel เองก็โดยพื้นฐานแล้วบังคับให้ทำสิ่งเดียวกัน ดูไม่ค่อยเหมือนว่า StateModel จะช่วยได้สมกับที่ควรจะเป็น แต่กลับเพิ่มโค้ดเฟรมเวิร์กที่ต้องทำความเข้าใจอีกมาก แลกกับการลดโค้ดทดสอบจริง ๆ จากประสบการณ์แล้วเพียงเล็กน้อย

    • มีการทดสอบบางแบบที่การตัดสินแบบนั้นถูกต้อง แต่ส่วนที่ยากมักอยู่ที่การ ย่อกรณีล้มเหลว
      ถ้าคุณต้องการสร้างเฉพาะลำดับการเปลี่ยนสถานะที่ “ใช้ได้” ก็มักต้องมีสถานะของโมเดลไว้กำหนดว่าขั้นตอนทดสอบใดใช้ได้ในสถานะหนึ่ง ๆ และระหว่างการย่อ ก็ต้องระวังไม่ให้การลบขั้นตอนทดสอบทำลายเงื่อนไขก่อนหน้าที่รักษาไว้ตอนสร้างแต่ละขั้นตอน จนทำให้เกิดความล้มเหลวปลอม ๆ
      ถ้าคุณต้องการเพียงลำดับของการกระทำแบบสุ่มล้วน ๆ ที่การกระทำใดก็ใช้ได้ในทุกสถานะ เฟรมเวิร์ก proptest แบบมีสถานะอาจจะมากเกินไป แต่ถ้าต้องคงสถานะของโมเดลไว้และต้องระบุเงื่อนไขก่อนหน้าของหลายการกระทำ เฟรมเวิร์กเฉพาะทางจะช่วยลดงานไปได้มาก
      ปีที่แล้วผมเขียนบล็อกโพสต์เรื่องนี้ไว้ และถ้าอยากดูตัวอย่างที่ลงลึกกว่านี้ก็น่าจะมีประโยชน์: https://readyset.io/blog/stateful-property-testing-in-rust
      อย่างที่คนอื่นพูดไว้ การทดสอบ state machine แบบขนานก็เป็นข้อดีเจ๋ง ๆ อย่างหนึ่งที่ได้จากเฟรมเวิร์กเฉพาะทาง แต่ไม่ใช่ข้อดีอย่างเดียว
    • สำหรับส่วนที่มีสถานะ ผมคิดว่า การทดสอบแบบอิงโมเดล จัดการได้ดีกว่า
      จะผสมสไตล์การทดสอบกันก็ได้ โค้ดของคุณเอง
    • ผมเข้าใจว่า QuickCheck แบบขนานคือการตรวจสอบว่า interleaving ที่เป็นไปได้ทั้งหมดในโปรแกรมหลายเธรด สุดท้ายแล้วสร้างสถานะที่ยังเข้าถึงได้แม้จะเรียกคำสั่งแบบลำดับต่อเนื่องก็ตาม
      นั่นแหละคือข้อดี

  • ผู้เขียนเน้นไปที่แง่มุม state machine และการทำงานแบบขนานของการทดสอบเชิงคุณสมบัติ แต่ก็ยังมีแง่มุมอื่นที่อาจให้ผลลัพธ์ที่ดีกว่าได้
    อย่างหนึ่งคือ coverage-guided property-based testing ดูได้จากบทความของ Dan Luu: https://danluu.com/testing/
    อีกอย่างคือสิ่งที่ผมอาจมีอคติอยู่บ้าง นั่นคือการทำให้การย่อกรณีทดสอบเป็นอัตโนมัติ โดยยังคงรักษา invariant ทั้งหมดที่สร้างไว้ตอนสร้างค่า
    สรุปคือ ฟังก์ชันย่อแบบอนุพันธ์สไตล์ QuickCheck (shrink : a -> [a]) ที่ทำงานกับค่านั้นมีข้อจำกัดและปัญหาเรื่องเงื่อนไขบังคับ ทำให้คนมักปิดการย่อไปเลยแทนที่จะจัดการปัญหา
    rose tree แบบ “integrated shrinking” (เช่น Hedgehog) ทำตามเงื่อนไขบังคับของ generator แต่มีปัญหาเมื่อใช้ monadic bind กล่าวคือ กรณีที่ใช้ผลลัพธ์ของ generator หนึ่งไปแตกแขนงเป็น generator อื่น
    แนวทางเดียวที่ดูเหมือน “มันใช้ได้เลย” แบบมหัศจรรย์คือ internal shrinking ของ Hypothesis โดยใช้ชั้นทางอ้อมที่ลดรายการของการสุ่มเลือก แทนที่จะลดค่าตัวมันเอง ข้อเสียคือ generator จะกลายเป็น parser ของรายการไบต์ที่อาจล้มเหลวได้ จึงมีความไม่มีประสิทธิภาพเพิ่มขึ้นเล็กน้อย และผู้ใช้ก็สามารถสร้าง generator แปลก ๆ ที่ตัว internal shrinker ลดได้ไม่สมบูรณ์ ถึงอย่างนั้น ในสามแนวทางนี้ก็ยังให้ประสบการณ์นักพัฒนาที่ดีที่สุด และเมื่อคิดว่าการที่คนลงมือเขียนเทสต์กันอยู่แล้วก็เป็นปาฏิหาริย์เล็ก ๆ อย่างหนึ่ง สำหรับผู้เขียนไลบรารีทดสอบแล้ว มันจึงดูเป็นแนวทางที่คุ้มค่าที่สุดในการสร้าง

    • เรื่องที่ rose tree แบบ “integrated shrinking” (เช่น Hedgehog) ทำตามเงื่อนไขของ generator แต่มีปัญหากับ monadic bind นั้น เท่าที่ความรู้สมัครเล่นของผมพอมี ผมมองว่านี่คือข้อจำกัดพื้นฐานของ monadic bind/generator เอง
      ทางเลือกคือควรเอนเอียงไปใช้ generator แบบ applicative เพื่อให้ย่อได้เหมาะสมที่สุด: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      พูดอีกอย่างคือ generator แบบ applicative จะไม่ “ใช้ผลลัพธ์ของ generator ไปแตกแขนงเป็น generator อื่น” และด้วยธรรมชาติแบบ “ขนาน” ของ applicative การย่อจึงถูกทำให้เหมาะสมได้ โดยคำว่าขนานที่นี่ไม่ใช่ความหมายแบบเธรดในบทความ แต่เป็นความหมายเชิง monad applicative นั้น “ขนาน” จึงสามารถย่อ generator ได้อย่างอิสระจากกัน ในทางกลับกัน generator แบบ monad นั้น “อนุกรม” ดังนั้นถ้าย่อตัวหนึ่ง พฤติกรรมของ generator ที่ตามมาก็ต้องเปลี่ยนไปด้วย
      ถ้ามีลิงก์ไปยังงานนำเสนอที่เผยแพร่แล้ว ผมอยากดู
    • โดยส่วนตัวแล้ว Hypothesis สำหรับผมยังห่างไกลจากคำว่า “มันใช้ได้เลย”
      ผมไม่คิดว่ามันพร้อมสำหรับ production จริง ๆ และดูเหมือนจะเป็นเช่นนั้นตั้งแต่การออกแบบด้วยซ้ำ[0]
      ผมเคยใช้ clojure.spec.alpha ควบกับ test.check และแบบไม่ใช้มันมาพอสมควร ดังนั้นแม้จะมีความต่างกัน ผมก็ไม่ได้แปลกแยกกับแนวคิดทั่วไปเสียทีเดียว
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • เฟรมเวิร์กที่ผมชอบคือ falsify ซึ่งมี “internal integrated shrinking”
      มันคล้าย Hypothesis แต่ใช้ tree ของ generator แทน linear sequence และอิงกับ selective functor ซึ่งเป็นอินเทอร์เฟซที่ดีและมีประโยชน์กับสิ่งอย่าง validator ด้วย
      ตาม https://hackage.haskell.org/package/falsify ไลบรารีนี้ให้ property-based testing ที่รองรับ internal integrated shrinking โดย integrated ในความหมายแบบ Hedgehog คือไม่ต้องเขียน shrinker แยกจาก generator และ internal ในความหมายแบบ Hypothesis คือยังทำงานได้ดีตลอดทั้ง monadic bind

  • ผมพยายามใช้ property-based testing แต่ก็มักรู้สึกเหมือน นั่งอยู่ระหว่างเก้าอี้สองตัว
    ถ้าผมเข้าใจคุณสมบัติบางอย่างดีพอที่จะทดสอบมันอย่างเข้มงวด ปกติผมก็มักจะผลักมันเข้าไปไว้ใน type system ให้มันเป็นจริงโดยโครงสร้างอยู่แล้ว ถ้าแค่อยากได้ smoke test ง่าย ๆ อินพุตสุ่มเพียงตัวเดียวก็มักง่ายกว่า

    • อยากรู้ว่าคุณนึกถึงคุณสมบัติประเภทไหนอยู่
      ตัวอย่างเช่น บ่อยครั้งเรามีทั้ง implementation แบบตรงไปตรงมาที่ช้าแต่เรียบง่าย และ implementation แบบปรับแต่งประสิทธิภาพ แล้วเราสามารถเปรียบเทียบผลลัพธ์ของทั้งสองกับอินพุตสุ่มได้ นี่เป็นคุณสมบัติเรียบง่ายที่เข้าใจได้ง่าย แต่โดยทั่วไปก็ยากจะใส่เข้าไปใน type system
      เช่นเดียวกัน อาจมีคุณสมบัติว่าไม่ควรขึ้นอยู่กับลำดับที่ป้อนอินพุต หรือข้อมูลอาจแบ่งออกได้ในลักษณะที่มีสมบัติอย่าง max(ค่าสูงสุดของ A, ค่าสูงสุดของ B) = maximum(A union B) แล้วจะเข้ารหัสสิ่งแบบนี้ใน type system ได้อย่างไร?
      หรืออย่าง “สำหรับ A และ B ใด ๆ คำตอบที่เหมาะที่สุดบางตัวที่หาได้จาก A นั้นแย่กว่าคำตอบที่เหมาะที่สุดบางตัวที่หาได้จาก A union B” หรือ idempotence อย่าง f(f(A)) = f(A)
      ทั้งหมดนี้เป็นคุณสมบัติที่เข้าใจได้ง่าย แต่ส่วนใหญ่ก็อธิบายได้ไม่ง่ายใน type system ทั่วไป
    • แน่นอนว่าถ้าบังคับข้อจำกัดได้ตั้งแต่ตอนคอมไพล์ก็ดีกว่าอย่างชัดเจน
      แต่ก็ยังมีข้อจำกัดอีกมากที่ตัวตรวจชนิดข้อมูลกระแสหลักจัดการไม่ได้ dependent types น่าจะช่วยได้มาก แต่ตอนนี้ก็ดูเหมือนยังจำกัดอยู่ในโลกเฉพาะทางอย่างพวก theorem prover

  • ผมสงสัยว่ารายชื่อนี้ลืม QuviQ Erlang QuickCheck ต้นฉบับไปหรือเปล่า
    ตัวผลิตภัณฑ์เต็มเป็นซอฟต์แวร์ปิด แต่ก็มี QuickCheck Mini เวอร์ชันฟรีให้ด้วย: http://www.quviq.com/downloads/

  • ตอนนี้ Clojure ก็มีไลบรารี quickcheck แบบมี state แล้ว: https://github.com/griffinbank/test.contract
    การทดสอบแบบขนาน ฟังดูน่าสนใจ แต่จนถึงตอนนี้ก็ยังไม่ใช่แหล่งของความเจ็บปวดใหญ่สำหรับผม

  • สำหรับการทดสอบใน C#/.NET ผมใช้ CsCheck[0] มาตลอด และค่อนข้างพอใจมาก
    เข้าถึงได้ง่ายกว่า Hedgehog หรือ FsCheck มาก และก็ทำงานได้ค่อนข้างเร็วด้วย
    [0] https://github.com/AnthonyLloyd/CsCheck

    • พออ่านบทความต่อ ก็พบว่า CsCheck รองรับไม่ใช่แค่การทดสอบแบบ property-based แต่ยังรองรับการทดสอบแบบ “stateful”/“model-based” ด้วย
      และยังรองรับการทดสอบ linearizability/แบบขนานที่อธิบายในบทความด้วย
      อ้างอิง:
      https://github.com/AnthonyLloyd/CsCheck?tab=readme-ov-file#m...
      https://github.com/AnthonyLloyd/CsCheck?tab=readme-ov-file#c...
    • FsCheck นั้นยอดเยี่ยม แต่มีความเฉพาะทางกับ F# มาก ชื่อจึงเป็น FsCheck
      การมี เวอร์ชันแยกสำหรับ C# ก็ดูสมเหตุสมผล