Chulalongkorn University Theses and Dissertations (Chula ETD)
การสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี
Other Title (Parallel Title in Other Language of ETD)
A construction of formal specification in the Z notation from C programs
Year (A.D.)
2000
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Degree Name
วิทยาศาสตรมหาบัณฑิต
Degree Level
ปริญญาโท
Degree Discipline
วิทยาศาสตร์คอมพิวเตอร์
DOI
10.58837/CHULA.THE.2000.989
Abstract
วิทยานิพนธ์นี้ได้กำหนดกฎและออกแบบขั้นตอนวิธีในการสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี กฎที่ได้แบ่งเป็น 2 ส่วน คือ กฎสำหรับการแปลงส่วนการประกาศ และกฎสำหรับการแปลงส่วนการทำงาน เนื่องจากพบว่ามีความคล้ายคลึงระหว่างโครงสร้างของโปรแกรมภาษาซีและข้อกำหนดเซด งานวิจัยนี้ครอบคลุมถึงการแปลงชนิดข้อมูลพื้นฐานในภาษาโปรแกรมซี 7 ชนิด และข้อความสั่งหลัก 5 ประเภทในภาษาโปรแกรมซีได้แก่ ข้อความสั่งกำหนดค่า ข้อความสั่งเลือกทางเดิน ข้อความสั่งตามลำดับ ข้อความสั่งวนซ้ำ และข้อความสั่งเรียกใช้ฟังก์ชัน นอกจากนั้นงานวิจัยนี้ยังได้นำเอาขั้นตอนวิธีที่ได้มาทำการพัฒนาเป็นเครื่องมือในการแปลงโปรแกรมภาษาซีเป็นข้อกำหนดรูปนัยในรูปสัญกรณ์เซด ซึ่งโปรแกรมที่พัฒนาได้รับการทดสอบโดยใช้กรณีทดสอบ 9 กรณีและผลลัพธ์ได้รับการตรวจสอบในส่วนวากยสัมพันธ์และการพิสูจน์ทางคณิตศาสตร์จากโปรแกรม Z/EVES
Other Abstract (Other language abstract of ETD)
This thesis defines rules and designs algorithms for constructing formal specification in Z notation from C programs. Because of the similarity between C program structure and Z specification structure, the rules are categorized into two parts-the declaration-part translating rules an doperation-part translating rules. Seven primitive data types in C and five kinds of statement in C-assignment statement, alternative statement, sequence statement, iterative statement and function call statement, are covered in our approach. Moreover, a tool for translating C programs to formal specification in Z notation is developed by using our algorithm. The software tool is tested to satisfy 9 test cases and the results are syntactically checked and theoretically proved using the program Z/EVES.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
วรเจนวณิชย์, เรืองยศ, "การสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี" (2000). Chulalongkorn University Theses and Dissertations (Chula ETD). 63666.
https://digital.car.chula.ac.th/chulaetd/63666