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

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

การเตรียมรายการความต้องการผลิตภัณฑ์ (รายการข้อกำหนด) อย่างต่อเนื่องและทันท่วงทีใน แนวทาง การพัฒนาซอฟต์แวร์แบบ Agileเช่นScrumมักถูกอธิบายว่าเป็นการปรับปรุงแก้ไข^{[ 1 ]}

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

ตัวอย่างเช่นx ∈ {1,2,3} (โดยที่xคือค่าของตัวแปรxหลังจากการดำเนินการ) สามารถลดรูปเป็นx ∈ {1,2} จากนั้นx ∈ {1} และนำไปใช้เป็นx  := 1 ได้ การนำx  := 2 และx  := 3 ไปใช้ก็เป็นที่ยอมรับได้เช่นกันในกรณีนี้ โดยใช้เส้นทางการลดรูปที่แตกต่างกัน อย่างไรก็ตาม เราต้องระมัดระวังไม่ให้ลดรูปเป็นx ∈ {} (เทียบเท่ากับเท็จ ) เนื่องจากไม่สามารถนำไปใช้ได้จริง เพราะเป็นไปไม่ได้ที่จะเลือกสมาชิกจากเซต ว่าง

บางครั้งก็มีการใช้ คำว่าการทำให้เป็น รูปธรรม (reification ) (ซึ่งบัญญัติโดยคลิฟฟ์ โจนส์ ) การลดทอน (retrenchment)เป็นเทคนิคทางเลือกเมื่อไม่สามารถปรับปรุงรูปแบบได้ สิ่งที่ตรงข้ามกับการปรับปรุงคือการนามธรรม (abstraction )

แคลคูลัสการปรับปรุง (Refinement calculus)เป็นระบบที่เป็นทางการ (ได้รับแรงบันดาลใจจากตรรกะของ Hoare ) ที่ส่งเสริมการปรับปรุงโปรแกรมระบบการแปลง FermaT (FermaT Transformation System)เป็นการนำแคลคูลัสการปรับปรุงไปใช้ในระดับอุตสาหกรรมวิธี B (B-Method)ก็เป็นวิธีการที่เป็นทางการ อีกวิธีหนึ่ง ที่ขยายแคลคูลัสการปรับปรุงด้วยภาษาส่วนประกอบ: วิธีนี้ถูกนำไปใช้ในการพัฒนาทางอุตสาหกรรมแล้ว

ในทฤษฎีประเภทประเภทการปรับปรุง^{[ 2 ] [ 3 ] [ 4 ]}คือประเภทที่มีเงื่อนไขซึ่งถือว่าเป็นจริงสำหรับองค์ประกอบใดๆ ของประเภทการปรับปรุง ประเภทการปรับปรุงสามารถแสดงเงื่อนไขก่อนหน้าเมื่อใช้เป็นอาร์กิวเมนต์ของฟังก์ชันหรือเงื่อนไขหลังเมื่อใช้เป็นประเภทการส่งคืนตัวอย่างเช่น ประเภทของฟังก์ชันที่รับจำนวนธรรมชาติและส่งคืนจำนวนธรรมชาติที่มากกว่า 5 อาจเขียนได้เป็นประเภทการปรับปรุงจึงเกี่ยวข้องกับประเภทย่อยเชิงพฤติกรรม ${\displaystyle f:\mathbb {N} \rightarrow \{n:\mathbb {N} \,|\,n>5\}}$

• การทำให้เป็นรูปธรรม (วิทยาการคอมพิวเตอร์)