การสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี

เรืองยศ วรเจนวณิชย์

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/5857

Title:	การสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี
Other Titles:	A construction of formal specification in the Z notation from C programs
Authors:	เรืองยศ วรเจนวณิชย์
Advisors:	วิวัฒน์ วัฒนาวุฒิ
Other author:	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
Advisor's Email:	Wiwat.V@chula.ac.th
Subjects:	ซี (ภาษาคอมพิวเตอร์) สัญกรณ์เซด
Issue Date:	2543
Publisher:	จุฬาลงกรณ์มหาวิทยาลัย
Abstract:	วิทยานิพนธ์นี้ได้กำหนดกฎและออกแบบขั้นตอนวิธีในการสร้างข้อกำหนดรูปนัยในรูปสัญกรณ์เซดจากโปรแกรมภาษาซี กฎที่ได้แบ่งเป็น 2 ส่วน คือ กฎสำหรับการแปลงส่วนการประกาศ และกฎสำหรับการแปลงส่วนการทำงาน เนื่องจากพบว่ามีความคล้ายคลึงระหว่างโครงสร้างของโปรแกรมภาษาซีและข้อกำหนดเซด งานวิจัยนี้ครอบคลุมถึงการแปลงชนิดข้อมูลพื้นฐานในภาษาโปรแกรมซี 7 ชนิด และข้อความสั่งหลัก 5 ประเภทในภาษาโปรแกรมซีได้แก่ ข้อความสั่งกำหนดค่า ข้อความสั่งเลือกทางเดิน ข้อความสั่งตามลำดับ ข้อความสั่งวนซ้ำ และข้อความสั่งเรียกใช้ฟังก์ชัน นอกจากนั้นงานวิจัยนี้ยังได้นำเอาขั้นตอนวิธีที่ได้มาทำการพัฒนาเป็นเครื่องมือในการแปลงโปรแกรมภาษาซีเป็นข้อกำหนดรูปนัยในรูปสัญกรณ์เซด ซึ่งโปรแกรมที่พัฒนาได้รับการทดสอบโดยใช้กรณีทดสอบ 9 กรณีและผลลัพธ์ได้รับการตรวจสอบในส่วนวากยสัมพันธ์และการพิสูจน์ทางคณิตศาสตร์จากโปรแกรม Z/EVES
Other Abstract:	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.
Description:	วิทยานิพนธ์ (วท.ม.)--จุฬาลงกรณ์มหาวิทยาลัย, 2543
Degree Name:	วิทยาศาสตรมหาบัณฑิต
Degree Level:	ปริญญาโท
Degree Discipline:	วิทยาศาสตร์คอมพิวเตอร์
URI:	http://cuir.car.chula.ac.th/handle/123456789/5857
ISBN:	9743468838
Type:	Thesis
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
Reungyos.pdf		7.39 MB	Adobe PDF	View/Open

Show full item record