2.4 VericationProving properties o

2.4 Verication
Proving properties of programs has long been a central goal in programming
research. These days type systems are being developed that blur or erase the
distinction between type checking and verication|types are suciently rich as
to be able to state and enforce detailed correctness properties of programs, often
with sucient automation as to make it routinely possible to ensure compliance
with useful specications [Appel et al., 2014]. It seems clear that the trend is
now irreversible, for both practical and theoretical reasons.

ผลลัพธ์ (ไทย) 2:

2.4 Veri
ไอออนบวกคุณสมบัติพิสูจน์ของโปรแกรมได้รับการเป้าหมายหลักในการเขียนโปรแกรมการวิจัย
ระบบเหล่านี้ประเภทวันที่มีการพัฒนาเบลอหรือลบแตกต่างระหว่างการตรวจสอบชนิดและไอออนบวก Veri | ประเภท su อย่างมีประสิทธิภาพที่อุดมไปด้วย? เพื่อให้สามารถระบุและการบังคับใช้คุณสมบัติความถูกต้องรายละเอียดของโปรแกรมมักจะมีซูอัตโนมัติเพียงพอที่จะทำให้มันได้หรือไม่เป็นไปได้เป็นประจำเพื่อให้สอดคล้องกับไพเพอร์ speci ประโยชน์ [แตะ et al., 2014] มันเห็นได้ชัดว่าแนวโน้มในขณะนี้กลับไม่ได้ด้วยเหตุผลทั้งในทางปฏิบัติและทฤษฎี

ผลลัพธ์ (ไทย) 3:

2.4 ข้อมูล  ไอออนบวก
พิสูจน์คุณสมบัติของโปรแกรมมีเป้าหมายเป็นศูนย์กลางในการวิจัยโปรแกรม

ทุกวันนี้ระบบชนิดที่ถูกพัฒนาให้เบลอหรือลบ
ความแตกต่างระหว่างประเภทที่มีการตรวจสอบและ  | ประเภทซู  ciently รวย
สามารถรัฐและบังคับใช้คุณสมบัติความถูกต้องรายละเอียดของโปรแกรมมักจะ
กับ ซู  cient อัตโนมัติเพื่อให้ตรวจเป็นไปได้เพื่อให้สอดคล้องกับประโยชน์  แคต speci
[ ชื่อ et al . , 2010 ) ดูเหมือนว่าชัดเจนว่าแนวโน้ม
ตอนนี้กลับไม่ได้เหตุผลทั้งในทางปฏิบัติและทางทฤษฎี