Chulalongkorn University Theses and Dissertations (Chula ETD)

Formal approach to program verification

Other Title (Parallel Title in Other Language of ETD)

วิธีการตรวจสอบโปรแกรมโดยหลักการเชิงรูปนัย

Year (A.D.)

2001

Document Type

Thesis

First Advisor

Peraphon Sophatsathit

Faculty/College

Faculty of Science (คณะวิทยาศาสตร์)

Degree Name

Master of Science

Degree Level

Master's Degree

Degree Discipline

Computational Science

DOI

10.58837/CHULA.THE.2001.988

Abstract

Program verification has played an important role in today's production of reliable software [3]. The most popular method of verification is given by Hoare. Other mathematicians and programmers also offered their method based on Hoare's principles. This thesis proposes a different approach to program verification using Hoare notation. In this thesis, we introduced a new method based on Hoare triple and some inference rules as a tool for program correctness proof. The proposed approach adopted conventional black-box and white-box tests [6] to carried out a systematic and rigorous program verification.

Other Abstract (Other language abstract of ETD)

ในกระบวนการผลิตซอฟแวร์ที่มีความน่าเชื่อถือนั้น การตรวจสอบความถูกต้องของโปรแกรมมีความสำคัญมาก ซึ่งวิธีการตรวจสอบที่เป็นรู้จักกันดีได้แก่ วิธีที่นำเสนอโดย Hoare และหลังจากนั้นได้มีนักคณิตศาสตร์และ โปรแกรมเมอร์จำนวนมากที่อาศัยพื้นฐานจากวิธีการของ Hoare ในการสร้างวิธีการตรวจสอบใหม่ๆ รวมถึงงานวิจัยชิ้นนี้ด้วย ในงานวิจัยชิ้นนี้ได้นำเสนอวิธีการตรวจสอบความถูกต้องของโปรแกรม โดยใช้ Hoare triple และ Rule of Inference เป็นพื้นฐานในการสร้างวิธีการตรวจสอบความถูกต้องของโปรแกรม เนื่องจากมีการประยุกต์การตรวจสอบแบบ Black-Box และ White-Box อย่างมีระบบแน่นอน มาใช้ในกระบวนการนี้ด้วย

Link to Full Text

Share

COinS