上海大学学报（自然科学版）
上海大學學報（自然科學版）
상해대학학보（자연과학판）
JOURNAL OF SHANGHAI UNIVERSITY (NATURAL SCIENCE EDITION)
2005年
6期
589-595
,共7页
形式方法%形式规格说明%确认%动画模拟%Object-Z%Prolog%SICStus Prolog
形式方法%形式規格說明%確認%動畫模擬%Object-Z%Prolog%SICStus Prolog
형식방법%형식규격설명%학인%동화모의%Object-Z%Prolog%SICStus Prolog
形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一种可模拟执行的形式,从而帮助用户和规格说明者确认形式规格说明是否与用户的非形式化需求相一致.通过分析比较形式规格说明的两种动画策略--形式化程序合成和结构模拟的优缺点,决定使用结构模拟技术将0bject-Z规格说明转换成SICStus Prolog可执行程序并加以执行,从而实现对Object-Z规格说明的确认.
形式化方法讓軟件需求的規格說明變得更加簡潔精確,但是它的抽象難懂讓用戶難以確定形式規格說明中所敘述的用戶需求就是他們所期望的.另外,大多的規格說明語言都是不可執行的,因此人們採用一種動畫模擬的方式,將形式規格說明轉換成一種可模擬執行的形式,從而幫助用戶和規格說明者確認形式規格說明是否與用戶的非形式化需求相一緻.通過分析比較形式規格說明的兩種動畫策略--形式化程序閤成和結構模擬的優缺點,決定使用結構模擬技術將0bject-Z規格說明轉換成SICStus Prolog可執行程序併加以執行,從而實現對Object-Z規格說明的確認.
형식화방법양연건수구적규격설명변득경가간길정학,단시타적추상난동양용호난이학정형식규격설명중소서술적용호수구취시타문소기망적.령외,대다적규격설명어언도시불가집행적,인차인문채용일충동화모의적방식,장형식규격설명전환성일충가모의집행적형식,종이방조용호화규격설명자학인형식규격설명시부여용호적비형식화수구상일치.통과분석비교형식규격설명적량충동화책략--형식화정서합성화결구모의적우결점,결정사용결구모의기술장0bject-Z규격설명전환성SICStus Prolog가집행정서병가이집행,종이실현대Object-Z규격설명적학인.
