ในวิทยาการคอมพิวเตอร์เชิงทฤษฎีอัลกอริทึมจะถูกต้องตามข้อกำหนดหากมีพฤติกรรมตามที่ระบุไว้ ความถูกต้อง เชิงฟังก์ชันได้ รับการสำรวจอย่างดีที่สุด ซึ่งหมายถึงพฤติกรรมอินพุต-เอาต์พุตของอัลกอริทึม: สำหรับอินพุตแต่ละรายการ จะสร้างเอาต์พุตที่ตรงตามข้อกำหนด^{[ 1 ]}

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

// คืนค่าผลรวมของตัวหารแท้ของ n static int divisorSum ( int n ) { int i , sum = 0 ; for ( i = 1 ; i < n ; ++ i ) if ( n % i == 0 ) sum += i ; return sum ; } // คืนค่าจำนวนคี่สมบูรณ์ที่น้อยที่สุดint leastPerfectNumber ( void ) { int n ; for ( n = 1 ; ; n += 2 ) if ( n == divisorSum ( n )) return n ; }

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

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

ผลลัพธ์ที่สำคัญอย่างยิ่งในทฤษฎีการพิสูจน์คือการสอดคล้องกันของเคอร์รีและโฮเวิร์ดซึ่งระบุว่า การพิสูจน์ความถูกต้องเชิงฟังก์ชันในตรรกศาสตร์เชิงสร้างสรรค์นั้น สอดคล้องกับโปรแกรมบางอย่างในแคลคูลัสแลมบ์ดาการแปลงการพิสูจน์ในลักษณะนี้เรียกว่าการ สกัดโปรแกรม

ตรรกะของ Hoareเป็นระบบที่เป็นทางการ เฉพาะ สำหรับการให้เหตุผลอย่างเข้มงวดเกี่ยวกับความถูกต้องของโปรแกรมคอมพิวเตอร์^{[ 3 ]}โดยใช้เทคนิคเชิงสัจพจน์เพื่อกำหนดความหมายของภาษาโปรแกรมและโต้แย้งเกี่ยวกับความถูกต้องของโปรแกรมผ่านการยืนยันที่เรียกว่า Hoare triples

การทดสอบซอฟต์แวร์คือกิจกรรมใดๆ ที่มุ่งประเมินคุณลักษณะหรือความสามารถของโปรแกรมหรือระบบ และตรวจสอบว่าตรงตามผลลัพธ์ที่ต้องการหรือไม่ แม้ว่าจะเป็นสิ่งสำคัญต่อคุณภาพของซอฟต์แวร์และถูกนำไปใช้อย่างกว้างขวางโดยโปรแกรมเมอร์และผู้ทดสอบ แต่การทดสอบซอฟต์แวร์ก็ยังคงเป็นศิลปะเนื่องจากความเข้าใจในหลักการของซอฟต์แวร์ยังมีจำกัด ความยากลำบากในการทดสอบซอฟต์แวร์เกิดจากความซับซ้อนของซอฟต์แวร์: เราไม่สามารถทดสอบโปรแกรมที่มีความซับซ้อนปานกลางได้อย่างสมบูรณ์ การทดสอบเป็นมากกว่าการดีบัก จุดประสงค์ของการทดสอบอาจเป็นการประกันคุณภาพ การตรวจสอบและการรับรอง หรือการประเมินความน่าเชื่อถือ การทดสอบยังสามารถใช้เป็นตัวชี้วัดทั่วไปได้อีกด้วย การทดสอบความถูกต้องและการทดสอบความน่าเชื่อถือเป็นสองด้านหลักของการทดสอบ การทดสอบซอฟต์แวร์เป็นการแลกเปลี่ยนระหว่างงบประมาณ เวลา และคุณภาพ^{[ 4 ]}

• การตรวจสอบอย่างเป็นทางการ
• ออกแบบตามสัญญา
• การวิเคราะห์โปรแกรม
• การตรวจสอบแบบจำลอง
• ความถูกต้องของคอมไพเลอร์
• การอนุมานโปรแกรม