ศึกษาจากงานวิจัย Specification Matching of Object-oriented Component

ในงานวิจัยนี้ เป็นของ Frank Feiks และ Devid Hemer ตีพิมพ์ครั้งแรกในงาน Software Engineering and Formal Methods 2003(SEFM'03) โดยได้กล่าวถึง
- หลักการเชิงวัตถุจัดเป็นวิธีการหนึ่ง ที่สนับสนุนการนำซอฟแวร์กลับมาใช้ใหม่ ด้วยคุณสมบัติต่างๆเช่น abstraction,information hiding,polymorphism,inheritance,redefinition
- โดย ชุดlibrary ที่อยู่ในคลาส อาจปรับเปลี่ยนให้เหมาะสมตรงตามความต้องการของผู้ใช้ในระบบ ทำให้ไม่ต้องสร้างชุดคำสั่งขึ้นมาใหม่
- ซึ่งจำเป็นต้องค้นคืนหรือจับคู่ดูว่าในระบบ มีชุดคำสั่งที่สามารถปรับให้เข้ากลับความต้องการของผู้ใช้ใหม่อันเป็นการนำข้อกำหนดที่มีอยู่ มาใช้ใหม่ได้หรือไม่
- วิธีการเดิมในการค้นคืนชุดคำสั่งนั้น ชุดคำสั่งจะอยู่ในรูปของ text-based ซึ่งเป็นการยากในการค้น ขาดความแม่นยำ และ กำกวม ทำให้คุณลักษณะคำสั่งที่ค้นไม่ตรงตามความต้องการที่รับเข้ามา
- จึงได้นำวิธีให้ชุดคำสั่งอยู่ในรูป formal specification แล้วทำการค้นคืนด้วยการจับคู่ชุดคำสั่งดังกล่าว
- ซึ่งงานวิจัยนี้จะกล่าวถึงการจับคู่ ชุดคำสั่งในรูป formal specification เพื่อสามารถนำชุดคำสั่ง ที่มีอยู่มาใช้ให้ตรงกับความต้องการที่เข้ามาใหม่ โดยเขียนให้อยู่ในรูป Object-oriented Components
- ในการจับคู่ชุดคำสั่ง ในงานวิจัยนี้จะให้ความสำคัญในการจับคู่ในส่วน pre / post-condition
- โดยให้เป็นการจับคู่ระหว่าง Query component:Q ซึ่งเป็นกลุ่มความต้องการของผู้ใช้ และ Library component:S ให้เป็นชุดคำสั่งที่มีอยู่ในระบบ
- ซึ่งการจับคู่จะสำเร็จได้เมื่อมีการตอบสนองตามเงื่อนไขทั้ง pre-condition และ post-condition ของ Q และ S โดย S สามารถเข้าแทนที่ Q ได้นั่นเอง
- โดยความถูกต้องของข้อมูลสามารถยืดหยุ่นได้ เช่น กรณีสถานะเงื่อนไขของ S ก่อนที่จะดำเนินการ อาจแทนที่สถานะก่อนดำเนินการของ Q ได้ไม่ดีนัก คือ ผลลัพธ์ข้อมูลอาจตรงตามที่ต้องการบ้าง แต่เมื่อหลังดำเนินการแล้ว S สามารถให้ผลลัพธ์ตรงตามความต้องการ Q ได้ (อาจไม่จำเป็นที่ผลลัพธ์ก่อนดำเนินการ และ หลังดำเนินการถูกต้องเหมือนกันหมด)

รูปแบบการจับคู่ จะ เป็นการจับคู่ระหว่าง Query Class กับ Library Class
เราให้ Query Class ดังนี้

Fig.1 Query class

และ Library Class ดังนี้

Fig.2 Library class

โดยจะจับคู่เฉพาะหน่วยภายในที่เฉพาะเจาะจงของ method และ attribute ซึ่ง Method 0ะดูที่การจับคู่ของ function ขณะที่ attribute จะดูที่ state schema
จาก Fig.1 Query class จะเป็น MousePointer class บอกลักษณะภายใน class เช่น attribute,method (ให้เป็น public)โดยใน MousePointer class มี attribute 2 attribute คือ posX,posY โดยทั้งคู่จะสร้างขอบเขตค่าพารามิเตอร์ และมี Method คือ move และ setTo
จาก Fig.2 Library class จะเป็น 2Tuple class ซึ่งจะมี 2 attribute คือ first,second โดยมี type คือ T1,T2 มี method 3 method คือ create, getfirst, getsecond และภายในระบบอาจมี library class ที่สืบทอดมาจาก library class หลักวึ่งกรณีที่ Q วึ่งเป็นความต้องการของผู้ใช้ค้นหาแล้วอาจมี attribute ตรงกับ library class หลัก แต่ method อาจไม่ตรงหรือมีมากกว่าดังนั้น

Fig.3 2DVector Library class สืบทอดจาก 2Tuple Library class

จะเห็นว่า 2DVector สืบทอดมาจาก 2Tuple โดยมี method add,scale,swap เพิ่มเข้ามา

การจับคู่ระหว่าง Query class กับ Library class
- Q จับคู่กับ S ได้ถ้าปรับเปลี่ยนค่าใน S แล้วเมื่อแทนที่ผลการดำเนินการแล้วให้ผลเหมือน attribute และ method ของ Q
- ในกรณีที่มีการสืบทอด method จะทำการจับคู่โดยเปรียบเทียบ method ใน childclass แต่ไม่เปรียบเทียบกับ method ในคลาสแม่(คือไม่ต้องปรับเปลี่ยนใน class แม่สนใจแต่ใน class ลูกแทนโดยดูที่ attribute ที่สืบทอดจากคลาสแม่ และ method ของคลาสลูก) เช่น 2DVector Library class ที่สืบทอดมาจาก 2Tuple library class ทำการจับคู่กับ MousePointer Query เราต้องการดูว่า Q ที่เข้ามาจะจับคู่กับ S ที่มีอยู่ในระบบได้หรือไม่ โดย S นี้เป็นคลาสที่สืบทอดมาจาก Sหลัก เราจะสามารถปรับเปลี่ยนค่าใน 2DVector เพื่อนำไปทดสอบค่า pre-post condition ดังนี้
- ให้คือค่าที่ปรับเปลี่ยนของ S เพื่อใช้จับคู่กับ Q
(ซึ่งจากค่า เราจะรู้ได้อย่างไรว่า add ต้องคู่กับ move หรือ create ต้องคู่กับ setTo ซึ่งงานวิจัยนี้หรืองานวิจัยอื่น ก็จะไม่บอกแต่จะมุ่งเน้นไปที่การจับคู่ในส่วน Specification matching หรือ pre/post condition มากกว่า ซึ่งเป็นการนำทฤษฎีที่มีอยู่มาประยุกต์ใช้กับงานวิจัยของตนเอง แต่ส่วนที่ระบุว่าทำไม add ต้องคู่กับ move หรือ create ต้องคู่กับ setTo งานวิจัยจะบอกแต่เพียงว่าให้ดูบริบท หลีกเลี่ยงการดำเนินการที่ขัดแย้ง หรือ ไม่มีความเป็นไปได้เท่านั้น ดังนั้นกระผมจึงคิดว่าจะนำเสนอทางแก้ปัญหาเหล่านี้โดยเพิ่มการจับคู่เชิงความหมายเข้าไปจากเดิมที่มีการจับคู่เฉพาะ Signature(Attribute)และ Specification(method))

จากคุณลักษณะของคลาสใน Object-oriented Components จะแบ่งเป็น attribute และ method ดังนั้นเราจะจับคู่ใน 2 ส่วนดังนี้

Attribute Matching
เราจะจับคู่ Q กับ S ที่อยู่ในรูปการปรับเปลี่ยน ( s()) โดยยกตัวอย่าง ค่า attribute posX,posY ใน MousePointerQuery class
กับค่า attribute first,second ของ 2Tuple ซึ่งสืบทอดไปยัง 2DVector Library class
โดยให้ S อยู่ในรูป s() โดยให้ type เหมือนกันจะได้
จะพบว่าค่า invariant ของ MousePointer จะ Stronger กว่า 2DVector คือ method ของ library สามารถดำเนินการให้ผลใน method Q ได้ภายใต้ขอบเขตของ attribute Q คือ attribute S ที่จะดำเนินการใน method S แล้วจะสามารถให้ผลเหมือนการดำเนินการใน method Q ได้ต้องอยู่ภายใต้ขอบเขตของค่า invariant ใน attribute Q เท่านั้น

Method matching
Method Q จะจับคู่กับ Method S โดยพิจารณาจากลักษณะเด่น สภาพบริบทที่สอดคล้องกัน โดยงานวิจัยนี้นำทฤษฎีการจับคู่บนเทคนิคพื้นฐาน function specification matching techniques ของ Zaremski and Wing(A.Moormann Zaremski and J.M.Wing : Specification matching of software components,ACM Transactions on Software Engineering,October 1997) โดยแบ่งเป็น exact match กับ plug-in match ในรูปของ pre/post condition ดังนี้

Definition1 :exact match
จะพบว่า create จาก 2DVector เมื่อปรับค่าแล้ว สามารถจับคู่กับ setTo ของ MousePointer(Q) ด้วยการจับคู่แบบ exact match ดังนี้
Defination2:plug-in match คืออาจไม่เหมือนกันแต่แทนนที่กันได้ โดย S pre-condition นั้น weak กว่า Q pre-condition และ S post-condition strong กว่า Q post-condition
เช่น method add ของ 2DVector กับ method move ของ MousePointer เราพิจารณาในส่วนค่า pre-condition

จะพบว่า S นั้น weak กว่า Q

ขอบเขตของค่า invariant ใน Spost() มีค่าเท่ากับ Qpost
ส่วนหัวข้อถัดไปคือ advance matching ในงานวิจัยนี้ ผมขอไม่กล่าวถึงเนื่องจากวิธีนี้จะมุ่งไปที่ค่า coupling invariant ซึ่งเกินขอบเขตของงานวิจัยที่ข้าพเจ้าสนใจ โดยยังใช้วิธีการจับคู่เหมือนเดิมคือ แบ่งการจับคู่เป็น attribute matching และ method matching แต่จะสนใจไปที่ค่า coupling invariant

สรุปงานวิจัยนี้ และส่วนที่คาดว่าจะสามารถนำมาพัฒนาต่อ
- จะใช้คุณสมบัติขององค์ประกอบของคลาสใน object-oriented component ในการพิจารณาการจับคู่คือ attribute method การสืบทอดคลาส
- พิจารณาการจับคู่ในส่วน Specification matching (pre/post condition)เป็นสำคัญ
- ในส่วนการเลือกว่า method ไหนต้องจับคู่กับ method อะไรไม่มีรายละเอียดเลยเพียงบอกแต่ว่า เลือก method นี้มาจับคู่กับ Method นี้เท่านั้น

สัญกรณ์ แซด ( Z Notation )

ในบทความนี้ผมจะขอพูดถึงภาษา ที่นำเสนอข้อกำหนดรูปแบบนึง ที่สร้างขึ้นจากพื้นฐานทางคณิตศาสตร์ คือ ภาษาแซด ซึ่งท่านผู้อ่านอาจจะงง หรือ คิดว่ามันคือภาษาอะไร ใช้ทำอะไร มีด้วยหรือ ซึ่งผมจะขอนำเสนอละกันนะครับว่า ภาษาแซดคืออะไร ? ทำไมต้องใช้ภาษาแซด
ปัจจัยสำคัญในการพัฒนาซอฟแวร์นั้นคือความเสี่ยงในการพัฒนาซอฟแวร์ไม่เป็นไปตามความต้องการของผู้ใช้ (requirement) จึงได้นำวิธีการที่มีแบบแผน (Formal Method )เข้ามาช่วยในการพัฒนาซอฟแวร์ ซึ่งสามารถตรวจพบข้อกำหนดที่ผิดพลาด และ สามารถนำเสนอข้อกำหนดของระบบที่เขียนจากภาษาที่มีแบบแผนที่สร้างขึ้นมาจากพื้นฐานคณิตศาสตร์ เพื่อช่วยในการรายงานข้อกำหนดที่ผิดพลาด และ ทดสอบอย่างมีแบบแผน โดยที่ไม่เพิ่มค่าใช้จ่ายในการพัฒนาซอฟแวร์ โดยการเขียนข้อกำหนดด้วยภาษาแซด จะเริ่มจากสร้างโมเดลของระบบโดยแบ่งการทำงานออกเป็นส่วนๆแล้วนำส่วนต่างๆที่ถูกแบ่งย่อยมาประกอบเป็นระบบงาน ซึ่งแต่ละส่วนถูกสร้างขึ้นภายใต้หลักการพื้นฐานทางคณิตศาสตร์ ได้แก่ ฟังก์ชัน ตรรกศาสตร์ เซด เพื่อนำเสนอความสัมพันธ์ภายในระบบ และ แสดงการเปลี่ยนแปลงการทำงานของระบบ

โครงสร้างพื้นฐานในการเขียนข้อกำหนดด้วยภาษาแซด ประกอบด้วย 3 ส่วนคือ
1. ชื่อของเค้าร่าง (Schema name ) เป็นชื่อของงานหรือสิ่งที่เรากำหนด
2.คุณสมบัติเฉพาะของเค้าร่าง (Schema signature ) เป็นส่วนที่อธิบายลักษณะเฉพาะหรือคุณสมบัติของเค้าร่าง โดยประกาศตัวแปรและกำหนดชนิดข้อมูล
3.ส่วนคุณลักษณะเฉพาะ หรือภาคแสดง (Schema specification ) เป็นส่วนกำหนดคุณสมบัติหรือแสดงถึงการดำเนินการของเค้าร่าง โดยส่วนคุณลักษณะเฉพาะนี้จะไม่เปลี่ยนแปลง(Invariant ) ตลอดการทำงานของระบบ โดยระบุในลักษณะของข้อบังคับหรือเงื่อนไขที่มีค่าเป็นจริงเสมอ โดยจะแบ่งเงื่อนไขก่อนการดำเนินการ (Pre-condition)และหลังการดำเนินการ (Post-condition)

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

ขั้นตอนการเขียนข้อกำหนดด้วยภาษาแซดมีดังนี้
1.เขียนข้อกำหนดในรูปแบบภาษาที่ใช้ในประจำวัน
2.แตกย่อยระบบออกเป็นส่วนๆ
3.กำหนดรายละเอียดของแต่ละส่วนของระบบดังนี้
- กำหนดเซตและชนิดตัวแปรที่ใช้อธิบายลักษณะประจำของส่วนนั้นๆ
- กำหนดตัวแปรสถานะ แต่ละตัว
- กำหนดการดำเนินการที่ควรมี
4.รวมเอาการทำงานของแต่ละส่วนเข้าด้วยกัน

การจับคู่ข้อกำหนดความต้องการ

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

2. รูปแบบการจับคู่ที่มีอยู่
- การจับคู่แบบเดิมนั้น จะทำการจับคู่โดยพิจารณาจาก
- รูปแบบการพิจารณาความต้องการการจับคู่ของแต่ละข้อกำหนดจะพิจารณาจาก context matching หรือสภาพบริบท การคาดคะเน ความเหมือน profile ที่มี ซึ่งอาจไม่แม่นยำและใช้เวลามากเกินความจำเป็นได้
- ซึ่งรูปแบบข้อกำหนดความต้องการที่ร้องขอไป อาจจะเขียนไม่เหมือนกันทั้งที่มีความหมายในการตอบสนองความต้องการเหมือนกันก็ได้
- กรณีที่เขียนเหมือนกัน แต่ ความหมายต่างกันทำให้การจับคู่นั้นได้ข้อกำหนดที่ไม่เป็นไปตามความต้องการ ไม่มีความถูกต้อง
ซึ่งจากปัญหาเหล่านี้ ข้าพเจ้าจึงได้นำหลักการ ontology หรือคำเชิงความหมาย มาพิจารณาร่วมในการเข้าคู่ข้อกำหนดความต้องการเพื่อแยกวิเคราะห์ส่วน name datatype ทั้งส่วนที่เขียนเหมือนกันให้ผลต่างกัน หรือ เขียนต่างกันให้ผลเหมือนกัน แล้วนำมาวิเคราะห์จับคู่ในส่วน Signature Matching และ Specification Matching

ศึกษาจากงานวิจัย Specification matching of state-based modular component

เนื่องจากทฤษฎีการจับคู่ได้มีงานวิจัยหลายชิ้น ที่เสนอรูปแบบการจับคู่ requirement ซึ่งมีงานวิจัยชิ้นหนึ่งที่น่าสนใจโดยวิเคราะห์การจับคู่ ด้วยหลักการ จำแนกเทคนิคการจับคู่บนพื้นฐานลักษณะเฉพาะในแต่ละส่วนโมดูล โดยพิจารณาโมดูลที่แสดงถึงลักษณะเด่นที่ช่วยให้จับคู่ได้ง่าย(visible entity )เช่น ชื่อ พารามิเตอร์ และ โมดูลที่อยู่ในสภาพกำลังใช้งาน (use of state invariant ) ซึ่งงานวิจัย " Specification matching of state-based modular components " นี้เป็นของ David Hemer : School of Information Technology and Electrical Engineering ,Univerity of Queensland ตีพิมพ์ ที่ IEEE ปี 2003

ในงานวิจัยนี้กล่าวถึง
- การใช้เทคนิคอธิบายคุณลักษณะการจับคู่แต่ละ method ด้วยพื้นฐานเฉพาะแต่ละฟังก์ชัน แล้วพิจารณาผลความต้องการจากการดำเนินการด้วยค่าพารามิเตอร์ ทั้งก่อนดำเนินการและหลังดำเนินการ
- จับคู่บนพื้นฐานเฉพาะในแต่ละโมดูลโดยพิจารณา 2 ส่วนคือ visible entity และ use of state invariant
- ใช้หลักการ Component-base software engineering โดยพิจารณาจากโครงสร้างส่วนประกอบต่างๆที่คล้ายคลึงกัน ให้เหมาะสมกับแต่ละ component โดย Component-base เราสามารถนำบางส่วนของ componet มาทำการ reuse ,ปรับให้เข้ากัน,รวมกัน และ ประกอบเข้าเป็นความต้องการของผู้ใช้ ตรงตาม library component ที่กำหนดไว้
โดยในงานวิจัยนี้ ได้ใช้ ภาษาเชิงอุปนัยเชิงคณิตศาสตร์ ด้วย Z notation เพื่อแก้ปัญหาการเขียนข้อกำหนดความต้องการแบบเดิมที่เขียนในรูป text ที่อาจมีความกำกวม ขาดความแม่นยำ

ข้อกำหนดการจับคู่
จะมีรูปแบบการจับคู่อยู่ 2 แบบด้วยกันคือจับคู่โดยพิจารณาจากค่าพารามิเตอร์ (Signature matching ) และ พิจารณาจากผลดำเนินการของค่าพารามิเตอร์ด้วยเงื่อนไขการดำเนินการทั้งก่อนและหลัง (Specification matching)
Signature Matching จะพิจารณาความเหมือนกันของชนิดของพารามิเตอร์ (Parameter Type) โดย type ระหว่าง Query ที่ทำการค้นกับ Library Component ที่มีอยู่ต้อง equivalent type แต่พบปัญหา จากการจับคู่โดยพิจารณาจาก equivalent type คือถ้ามีการพ้องรูป หรือ polymorphic type อาจจะทำให้จับคู่ไม่เป็นไปตามความต้องการได้ จึงต้องเพิ่มการพิจารณาการจับคู่นอกเหนือจาก Parameter Type ด้วยวิธีที่เรียกว่า Specification matching โดยพิจารณารายละเอียดของการดำเนินการตามเงื่อนไขของแต่ละโอเปอเรชั่นในส่วน Signature เช่น input output precondition postcondition
โดยเราแบ่งผลของการเข้าคู่ได้เป็นแบบ การเข้าคู่อย่างเท่ากันและถูกต้อง คือเหมือนกันทุกกรณี (exact match) และ เข้ากันคู่กันได้แม้ว่าค่าพารามิเตอร์จะต่างกันแต่ในความหมายแล้วมีความครอบคลุมเฉพาะ หรือเป็น subtype กัน( partial match หรือ relax match)

ในมุมมองงานวิจัยนี้ จะ มองข้อกำหนดเป็นโมดูล ซึ่งแต่ละโมดูลจะประกอบด้วยค่า parameter ,การ importing module ,visible entities ซึ่งการจำแนกข้อกำหนดให้เป็นโมดูลนั้นจะจำแนกเป็น state schemas,initialisation schemas,operation schemas ดังแสดงในรูปดังนี้


โดยค่า
parameterisation : คือ ค่าของตัวแปรในโมดูลภายใต้ขอบเขตของset of entities . Entities เหล่านี้จะประกอบด้วย given sets,operations ,functions
Importing modules: จะประกาศในส่วน module ที่อ้างถึงว่าต้องการใช้โมดูลอะไร.
การ import นำเข้าmodule ตามข้อกำหนดที่ต้องการใช้ , และต้องให้บริการโดยกำหนดค่าตัวแปรของค่าตัวแปรทั้งหมดในโมดูล คำสั่ง imports Stack module, เมื่อต้องการใช้ Stack module และกำหนดค่าตัวแปรจาก set E เป็น set of natural numbers N.
จากนั้น Import คำสั่งที่สามารถเปลี่ยนชื่อใหม่ ของทุก entities ที่ปรากฏใน module, ซึ่งประกอบด้วย state variables, operations, functions และ relations. เพื่อทำการเข้าคู่กัน(ซึ่งจุดด้อยของงานวิจัยนี้คือต้องอาศัย context match หรือ sense ของผู้จับคู่ว่าควรImport อะไรคู่กับอะไร)
โดยพิจารณาคำสั่ง import ที่ให้ผลที่เหมือนกันจากคำสั่งก่อนหน้านี้, จากตัวอย่างจะมีการเปลี่ยนชื่อใหม่ของ state variable elements ไปยัง stacknats, the operation Push ไปยัง PushNat, และ the operation Pop ไปยัง PopNat.Visible entities: จะทำให้โครงสร้างและขอบเขตของโมดูลแคบลง ด้วยการแสดงลักษณะเด่นที่ ต้องการเข้าไปไม่ต้องอ้างอิงชื่อทั้งหมดเหมือน Importing modules

Module matching
จะแบ่งเป็น Unit matching ,การพิจารณาโดยจับคู่แบบ exact และ การพิจารณาโดยจับคู่แบบ relax ด้วย Entity subset matching
Unit matching: จะเป็นการจับคู่โดยพิจารณาเป็นหน่วยแต่ละหน่วยเพื่อจับคู่ modules,เราต้องการ methods สำหรับการจับคู่เฉพาะหน่วยที่ปรากฎให้เห็นใน modules.
ในงานวิจัยนี้จะจำกัดความสนใจไปที่หน่วย 3 ชนิดคือ:
state schemas; initialisation schemas; และ operation schemas.
เราจำแนกความต้องการสำหรับการจับคู่ของแต่ละชนิดแยกกัน ; โดยไม่พยายามจับคู่หน่วยของชนิดที่แตกต่างกันไป.

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

2.พิจารณาค่าชนิดพารามิเตอร์ โดย ค่าชนิดพารามิเตอร์ใน Q ต้องเป็นชนิดเดียวกับ S หรือเป็น Subtype ที่สอดคล้องกับชนิดพารามิเตอร์ของ S โดยเมื่อแทนค่าลงไปในชื่อตัวแปรที่เปลี่ยนใน (1)เพื่อสอดคล้องกันแล้ว ผลของชนิดพารามิเตอร์ ต้องเท่ากันหรือสอดคล้องกันด้วย

โดยเมื่อทำการรีเนมชื่อแล้วผลคือค่าพารามิเตอร์ทุกตัวใน Q สามารถบ่งบอกถึงค่าบางตัวใน S ได้

–

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

– Operation Schemas: จะเป็นส่วนดำเนินการแต่ละอันภายใต้ข้อกำหนดที่เราเขียนขึ้นโดยการจับคู่จะพิจารณาจากการดำเนินการที่ไกล้เคียงกัน สอดคล้องกัน หรือพิจารณาจากลักษณะเด่นที่แสดงถึงว่าการดำเนินการนี้เกี่ยวข้องกันแล้วทำการเข้าคู่โดยจะเข้าคู่ได้นั้นต้องพิจารณา จากชื่อว่าสอดคล้องกันหรือไม่ ชนิดค่าพารามิเตอร์ว่าเหมือนกันหรือเป็น Subtype กันหรือไม่ จากนั้นพิจารณาผลการดำเนินการ ทั้งก่อนการดำเนินการและหลังดำเนินการว่า Q สามารถแสดงถึงว่าเป็น S ได้หรือบ่งบอกว่าเป็น S ได้ก็คือเข้าคู่กันได้นั่นเอง โดยเราพิจารณาดังนี้

ในส่วนของเงื่อนไขก่อนดำเนินการ ค่า precondition ของ S จะ weaker กว่า ค่า precondition ของ Q คือเงื่อนไขก่อนดำเนินการทุกตัวใน Q สามารถบ่งบอกถึง S ได้แต่ไม่ได้บ่งบอกถึง S ได้ทั้งหมด

ในส่วนเงื่อนไขหลังดำเนินการหรือผลจากการดำเนินการ ค่า postcondition ของ S จะstronger กว่า ค่า postcondition ของ Q คือเงื่อนไขหลังการดำเนินการทุกตัวใน S สามารถบ่งบอกถึงผลที่ได้สืบเนื่องมาจากผลของการดำเนินการของ Q ได้โดยในงานวิจัยนี้สามารถสรุปได้ว่า

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

Blog ความคืบหน้างานวิจัยการจับคู่ข้อกำหนดความต้องการด้วย Z ครับ

ยินดีต้อนรับเข้าสู่ระบบการแลกเปลี่ยนความรู้แบบ Social Network บนโลกอินเตอร์เนตครับ
บล๊อกนี้จะเป็นการพูดถึงความคืบหน้า งานวิจัยการจับคู่ข้อกำหนดความต้องการด้วย Z
งานวิจัยที่เกี่ยวกับการ matchmaking และ Z notation Specification ครับผม