ดาฟนี
กระบวนทัศน์	เชิงบังคับ , เชิงฟังก์ชัน
ออกแบบโดย	เค. รัสตัน เอ็ม. ไลโน
นักพัฒนา	การวิจัยของไมโครซอฟต์
ปรากฏครั้งแรก	2009 ( 2009 )
เวอร์ชันเสถียร	4.11.0 / 25 สิงหาคม 2568 ( 25 สิงหาคม 2568 )
วินัยในการพิมพ์	มั่นคงแข็งแรงปลอดภัย
ใบอนุญาต	เอ็มไอที
นามสกุลไฟล์	.dfy
เว็บไซต์	dafny.org​

Dafnyเป็นภาษาคอมไพล์เชิงคำสั่งและเชิงฟังก์ชัน ที่คอมไพล์เป็นภาษาโปรแกรม อื่นๆ เช่นC# , Java , JavaScript , GoและPythonรองรับการกำหนดคุณสมบัติอย่างเป็นทางการผ่านเงื่อนไขก่อนการทำงาน เงื่อนไขหลังการทำงานตัวแปรของลูป การกำหนด คุณสมบัติการสิ้นสุด และการกำหนดคุณสมบัติเฟรมการอ่าน/เขียน ภาษานี้ผสมผสานแนวคิดจากกระบวน ทัศน์ การเขียนโปรแกรมเชิง ฟังก์ชัน และการเขียนโปรแกรมเชิงคำสั่งรวมถึงการสนับสนุนการเขียนโปรแกรมเชิงวัตถุคุณสมบัติประกอบด้วยคลาสทั่วไปการจัดสรรแบบไดนามิก ชนิดข้อมูลแบบอุปนัยและรูปแบบหนึ่งของตรรกะการแยกที่เรียกว่าเฟรมไดนามิก โดยปริยาย ^{[ 1 ]}สำหรับการให้เหตุผลเกี่ยวกับผลข้างเคียง^{[ 2 ]} Dafny ถูกสร้างขึ้นโดย Rustan Leino ที่Microsoft Researchหลังจากงานก่อนหน้านี้ของเขาในการพัฒนา ESC/ Modula-3 , ESC/Javaและ Spec#

Dafny มักปรากฏในการแข่งขันการตรวจสอบซอฟต์แวร์ (เช่น VSTTE'08, ^{[ 3 ]} VSCOMP'10, ^{[ 4 ]} COST'11, ^{[ 5 ]}และ VerifyThis'12 ^{[ 6 ]} )

Dafny ถูกออกแบบมาให้เป็นภาษาโปรแกรมที่คำนึงถึงการตรวจสอบ โดยกำหนดให้มีการตรวจสอบควบคู่ไปกับการพัฒนาโค้ด ดังนั้นจึงสอดคล้อง กับแนวคิดการพัฒนาซอฟต์แวร์ แบบ "ถูกต้องตั้งแต่เริ่มต้น" (Correct by Construction ) การพิสูจน์การตรวจสอบได้รับการสนับสนุนโดยเครื่องมือทางคณิตศาสตร์ ซึ่งรวมถึงจำนวนเต็มและจำนวนจริงทางคณิตศาสตร์ เวกเตอร์บิต ลำดับ เซต มัลติเซต ลำดับและเซตอนันต์ การอุปมาน การอุปมานร่วม และการพิสูจน์เชิงคำนวณ ภาระผูกพันในการตรวจสอบจะถูกดำเนินการโดยอัตโนมัติ หากมีข้อกำหนดที่เพียงพอ Dafny ใช้การวิเคราะห์โปรแกรมบางส่วนเพื่ออนุมานข้อความยืนยันข้อกำหนดจำนวนมาก ซึ่งช่วยลดภาระของผู้ใช้ในการเขียนข้อกำหนด กรอบการพิสูจน์โดยทั่วไปคือตรรกะ ของ Hoare

Dafny สร้างขึ้นบน ภาษาตัวกลาง Boogie ซึ่งใช้ตัวพิสูจน์ทฤษฎีบทอัตโนมัติ Z3เพื่อดำเนินการตามภาระผูกพันการพิสูจน์^{[ 7 ] [ 8 ]}

Dafny มีเมธอดสำหรับการใช้งานซึ่งอาจมีผลข้างเคียงและฟังก์ชันสำหรับใช้ในการกำหนดคุณสมบัติซึ่งเป็นแบบบริสุทธิ์^{[ 9 ]}เมธอดประกอบด้วยลำดับของคำสั่งตามรูปแบบคำสั่งที่คุ้นเคย ในขณะที่ตัวฟังก์ชันนั้นเป็นเพียงนิพจน์ คำสั่งที่มีผลข้างเคียงใดๆ ในเมธอด (เช่น การกำหนดค่าให้กับองค์ประกอบของพารามิเตอร์อาร์เรย์) จะต้องได้รับการพิจารณาโดยการสังเกตว่าพารามิเตอร์ใดสามารถเปลี่ยนแปลงได้โดยใช้ ข้อความ Dafny ยังมีประเภทคอลเลกชัน ที่ไม่เปลี่ยนแปลงได้modifiesหลากหลายประเภท ได้แก่ ลำดับ (เช่น) เซต (เช่น) แผนที่ ( ) ทูเปิล ประเภทข้อมูลแบบอุปนัย และ อาร์เรย์ ที่เปลี่ยนแปลงได้ (เช่น) seq<int>set<int>map<int,int>array<int>

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

เมธอด max(arr:array<int>) คืนค่า (max:int) // อาร์เรย์ต้องมีอย่างน้อยหนึ่งองค์ประกอบ ต้องใช้ arr.Length > 0 // ค่าที่ส่งคืนต้องไม่น้อยกว่าค่าใดๆ ในอาร์เรย์ รับประกันว่าสำหรับทุก j : int :: j >= 0 และ j < arr.Length ==> max >= arr[j] // ค่าที่ส่งคืนต้องตรงกับองค์ประกอบบางอย่างในอาร์เรย์ ตรวจสอบว่า j มีอยู่จริงหรือไม่ : int :: j>=0 && j < arr.Length && max == arr[j] { สูงสุด := arr[0]; var i: int := 1; // ในขณะที่ i น้อยกว่าความยาวของ arr // ดัชนีไม่เกิน arr.Length (จำเป็นเพื่อแสดง i==arr.Length หลังลูป) ตัวแปรคงที่ i <= arr.Length // ยังไม่พบองค์ประกอบใดที่มีขนาดใหญ่กว่าค่าสูงสุด invariant forall j:int :: j >= 0 && j < i ==> max >= arr[j] // องค์ประกอบบางอย่างที่พบจนถึงตอนนี้ตรงกับค่าสูงสุด invariant exists j:int :: j >= 0 && j < i && max == arr[j] // arr.Length - i ลดลงในแต่ละขั้นและมีค่าต่ำสุดที่ 0 ลดความยาวอาร์เรย์ - i { // อัปเดตค่าสูงสุดหากพบองค์ประกอบที่มีขนาดใหญ่กว่า ถ้า (arr[i] > max) { max := arr[i]; } // ดำเนินการต่อในอาร์เรย์ i := i + 1; } } 

ตัวอย่างนี้คำนวณหาค่าสูงสุดของอาร์เรย์ เงื่อนไขก่อนและหลังการทำงานของเมธอดนั้นกำหนดไว้ด้วยข้อความ `precondition` และ `postcondition` (ตามลำดับ) ในทำนองเดียวกัน ตัวแปรคงที่ของลูปและตัวแปรแปรผันของลูปก็กำหนดไว้ด้วยข้อความ ` requiresrequire` และ ` require` (ตามลำดับ) ensuresเช่นกันinvariantdecreases

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

เมธอด sumAndZero(arr: array<int>) คืนค่า (sum: nat) ต้องเป็นไปตามเงื่อนไขสำหรับทุก i :: 0 <= i < arr.Length ==> arr[i] >= 0 แก้ไข arr { var i: int := 0; ผลรวม := 0; // ในขณะที่ i น้อยกว่าความยาวของ arr { ผลรวม := ผลรวม + arr[i]; arr[i] := arr[i]; i := i + 1; } } 

การตรวจสอบนี้ล้มเหลวเนื่องจาก Dafny ไม่สามารถพิสูจน์ได้ว่า(sum + arr[i]) >= 0เงื่อนไขดังกล่าวเป็นจริง ณ จุดกำหนดค่า จากเงื่อนไขเบื้องต้น โดยสัญชาตญาณแล้วforall i :: 0 <= i < arr.Length ==> arr[i] >= 0เงื่อนไขดังกล่าวจะเป็นจริงในลูป เนื่องจากarr[i] := arr[i];เป็นคำ สั่ง NOPอย่างไรก็ตาม การกำหนดค่านี้ทำให้ Dafny ถือว่าตัวแปรนั้นarrเป็นตัวแปรที่เปลี่ยนแปลงได้ และละทิ้งข้อมูลที่ทราบเกี่ยวกับตัวแปรนั้นก่อนเริ่มลูป เพื่อตรวจสอบโปรแกรมนี้ใน Dafny เราสามารถทำได้สองวิธี คือ (ก) ลบการกำหนดค่าที่ซ้ำซ้อนออกarr[i] := arr[i];หรือ (ข) เพิ่มเงื่อนไขคงที่ของลูปinvariant forall i :: 0 <= i < arr.Length ==> arr[i] >= 0

นอกจากนี้ Dafny ยังใช้การวิเคราะห์โปรแกรมแบบคงที่ อย่างจำกัด เพื่ออนุมานค่าคงที่ของลูปอย่างง่ายเท่าที่จะเป็นไปได้ ในตัวอย่างข้างต้น ดูเหมือนว่าค่าคงที่ของลูปinvariant i >= 0ก็จำเป็นเช่นกัน เนื่องจากตัวแปรมีการเปลี่ยนแปลงiภายในลูป แม้ว่าตรรกะพื้นฐานจะต้องการค่าคงที่ดังกล่าว แต่ Dafny จะอนุมานค่าคงที่นี้โดยอัตโนมัติ ดังนั้นจึงสามารถละเว้นได้ในระดับซอร์สโค้ด

Dafny มีคุณสมบัติหลายอย่างที่สนับสนุนการใช้งานในฐานะเครื่องมือช่วยพิสูจน์แม้ว่าการพิสูจน์คุณสมบัติง่ายๆ ภายในfunctionหรือmethod(ดังที่แสดงไว้ข้างต้น) จะไม่ใช่เรื่องแปลกสำหรับเครื่องมือประเภทนี้ แต่ Dafny ยังอนุญาตให้พิสูจน์คุณสมบัติระหว่างกัน ได้อีกด้วย functionเช่นเดียวกับเครื่องมือช่วยพิสูจน์ทั่วไปการพิสูจน์ดังกล่าวส่วนใหญ่มักเป็นการพิสูจน์แบบอุปนัย Dafny อาจมีความพิเศษตรงที่ใช้การเรียกใช้เมธอดเป็นกลไกในการประยุกต์ใช้สมมติฐานแบบอุปนัย ตัวอย่างต่อไปนี้แสดงให้เห็น:

ประเภทข้อมูล List = Nil | Link(data: int, next: List) ฟังก์ชัน sum(l: List): int { แมตช์ l กรณีไม่มีค่า => 0 กรณี Link(d, n) => d + sum(n) } เงื่อนไขคือเป็นรายการธรรมชาติ (l: รายการ) { แมตช์ l กรณีไม่มีค่า => จริง กรณี Link(d, n) => d >= 0 และ isNatList(n) } บทแทรก NatSumLemma(l: รายการ, n: int) ต้องเป็นไปตามเงื่อนไข isNatList(l) และ n == sum(l) รับประกันว่า n >= 0 { แมตช์ l กรณีไม่มีค่า => // คายประจุโดยอัตโนมัติ กรณี Link(data, next) => { // ใช้สมมติฐานอุปนัย NatSumLemma(next, sum(next)); // ตรวจสอบสิ่งที่ดาฟนีรู้ ยืนยันว่าข้อมูล >= 0; } } 

ในที่นี้NatSumLemmaพิสูจน์คุณสมบัติที่มีประโยชน์ระหว่างsum()และisNatList()(กล่าวคือisNatList(l) ==> (sum(l) >= 0)) การใช้ghost methodสำหรับการเข้ารหัสบทพิสูจน์และทฤษฎีบทเป็นมาตรฐานใน Dafny โดยใช้การเรียกซ้ำสำหรับการอุปมาน (โดยทั่วไปคือการอุปมานเชิงโครงสร้าง ) การวิเคราะห์กรณีจะดำเนินการโดยใช้matchคำสั่ง และกรณีที่ไม่ใช่การอุปมานมักจะถูกยกเลิกโดยอัตโนมัติ ผู้ตรวจสอบต้องสามารถเข้าถึงเนื้อหาของfunctionหรือpredicateเพื่อคลี่คลายเนื้อหาตามความจำเป็นได้อย่างสมบูรณ์ สิ่งนี้มีนัยสำคัญเมื่อใช้ร่วมกับตัวแก้ไขการเข้าถึงโดยเฉพาะอย่างยิ่ง การซ่อนเนื้อหาของfunctionโดยใช้protectedตัวแก้ไข อาจจำกัดคุณสมบัติที่สามารถกำหนดได้เกี่ยวกับมัน

• ออกแบบตามสัญญา

• Meyer, Bertrand; Nordio, Martin, บรรณาธิการ (2012). เครื่องมือสำหรับการตรวจสอบซอฟต์แวร์เชิงปฏิบัติ: โรงเรียนภาคฤดูร้อนนานาชาติ LASER 2011 เกาะเอลบา ประเทศอิตาลี บทบรรยายเชิงสอนฉบับปรับปรุง . Springer . ISBN 978-3642357459.
• Sitnikovski, Boro (2022). การแนะนำการตรวจสอบซอฟต์แวร์ด้วยภาษา Dafny: การพิสูจน์ความถูกต้องของโปรแกรม . Apress. ISBN 978-1484279779.

• Dafny: เครื่องมือตรวจสอบภาษาและโปรแกรมเพื่อความถูกต้องในการทำงาน - Microsoft Research
• DafnyบนGitHubภาษาโปรแกรมที่คำนึงถึงการตรวจสอบความถูกต้อง