Formal Engineering Methods for Software Development --An Introduction to SOFL--

Size: px

Start display at page:

Download "Formal Engineering Methods for Software Development --An Introduction to SOFL--"

ことこてらわ
5 years ago
Views:

1 13~15. 形式設計仕様に基づく Java プログラムの作成と Suica カードシステムの small プロジェクト 6 ー実装目標 : 1.SOFL で作成した形式設計仕様に基づきその仕様を実現した Java プログラムを作成する

2 作成方法 : 次の 3 レベルのものから Java プログラムを作成する (a) モジュールから Java プログラムクラスの作成つまり一つの SOFL モジュールから一つの Java クラスを作成する (b) CDFD から Java クラスのメソッドの作成すなわち一つの CDFD から関連する Java クラスの一つのメソッドを作成する (c) プロセス仕様から Java クラスのインスタンスメソッドの作成つまり一つの SOFL プロセス仕様から関連する Java クラスの一つのメソッドを作成する

3 モジュールから Java へ変換次の変換を含める : (1)SOFL 形式仕様に定義された型例えば (a) 複合型 (composite type) Javaクラス (b) 集合型 (set type) Java arraylist (c) 列型 (sequence type) Java arraylist

4 (2)SOFL 形式仕様に定義されたストア変数基本的にはこのようなストア変数は Java クラスのインスタンス変数へ変換する (3)SOFL 形式仕様に定義された不変量 ( invariant) 定義された不変量を一つずつ Java クラスの適切なメソッドの本体で実装する一般てきには一つの不変量は一つの判断条件になる (4)SOFL 形式仕様に定義された定数基本的には一つの定数は Java クラスの一つの final 変数へ変換する

5 ATM システムの仕様から Java プログラムを作成する事例本 ATM システムの設計仕様には二つのモジュールがありそれを対応する二つの CDFD がある一つのモジュールにはいくつかのプロセス仕様が書かれている具体的にはその ATM の仕様は次の通りである

6 ATM システムの形式設計仕様の事例 ATM システムのトップレベル CDFD: No.1

7 (3)ATM の SOFL 形式設計仕様の事例 module SYSTEM_ATM; type AllAccounts = map AccountNo to CustomerAccountInfo; AccountNo = seq of nat0; /*6 digits */ CustomerAccountInfo = composed of name: string date_of_birth: Date address: string password: Password balance: nat0 /* 日本円だけを扱う */ end; Date = nat0 * nat0 * nat0; /*year * month * day*/ Password = seq of nat0 /*4 digits */

8 FullServices = {<Open_Account>, <Transfer>, <Deposit>, <Withdraw>, <Show_Balance>}; /* 形式仕様に新たな導入された型 */ Services = {<Transfer>, <Deposit>, <Withdraw>, <Show_Balance>}; /* 形式仕様に新たな導入された型 */ var ext #account_file: AllAccounts;

9 inv dom(account_file) <= 50000; /* 最大 5 万人のカスタマ */ not exists[acc_no1, acc_no2: dom(account_file)] account_file(acc_no1).name = account_file(acc_no2).name and account_file(acc_no1).address = account_file(acc_no2).address; /* 一人一つの口座 */ forall[acc: AccountNo] len(acc) = 6; /* 口座番号の長さは 6 個の自然数 */ forall[pass: Password] len(pass) = 4; /* パースワールドの長さは 4 個の自然数 */ forall[acc_no: dom(account_file)] account_file(acc_no).balance >= 0; /* 残高は 0 以上 */

10 behav: CDFD_No.1; process Init() end_process; /* ローカルストアがないので何もしない */ process Receive_Command(service: FullServices) open_acc: sign otherservices: Services pre true post if service = <open_account> then bound(open_acc) else otherservices = service comment 事前条件 : 入力に対して具体的な制約がない事後条件 : もし入力 service は <open_account> であれば出力 open_acc を生成するそうでなければ出力 otherservices は入力 service と同じになる end_process;

11 process Open_Account( account_no: AccountNo, ext wr account_file : AllAccounts cus: CustomerAccountInfo, open_acc: sign ) pre account_no notin dom(account_file) post override(~account_file, {account_no -> cus}) comment 事前条件 : 入力 account_no と cus は account_file に入っていない事後条件 : account_no -> cus を account_file に加える end_process;

12 process Authenticate( pass: Password, otherservices: Services, acc_no: AccountNo) from_acc_no: AccountNo acc_no1: AccountNo acc_no2: AccountNo acc_no3: AccountNo err: string ext rd account_file : AllAccounts pre true post if acc_no inset dom(account_file) then if account_file(acc_no).password = pass then case otherservices of <Transfer> -> from_acc_no = acc_no; <Deposit> -> acc_no1 = acc_no; <Withdraw> -> acc_no2 = acc_no; <Show_Balance> -> acc_no3 = acc_no end_case else err = The password is incorrect. else err = The account does not exist. comment 入力された acc_no と pass がただしなければエラーメッセージを出すそうでなければ適切な出力を作成する end_process;

13 process Deposit( amount: nat0, acc_no1: AccountNo) ext wr account_file: AllAccounts pre acc_no1 inset dom(account_file) post override(~account_file, {acc_no1 -> ~account_file(acc_no1).balance + amount}) comment 事前条件 : account_file に口座番号が acc_no と同じである口座が存在事後条件 : amount を account_file に口座番号が acc_no と同じである口座に入れる end_process;

14 process Withdraw( acc_no2: AccountNo, amount: nat0) error: string cash: nat0 ext wr account_file : AllAccounts pre acc_no2 inset dom(account_file) post if amount <= ~account_file(acc_no2).balance then account_file = override(~account_file, {acc_no2 -> ~account_file(acc_no2).balance amount}) else error = The withdrawal amount is over the limit. comment 事前条件 : account_file に口座番号が acc_no と同じである口座が存在する事後条件 : amount を account_file に口座番号が acc_no と同じである口座の残高から減らし出力 cash が amount にするただし amount は acc_no の口座の残高より大きい或いは amount は 20 万円を超えるのであれば本引き出すことができない end_process;

15 process Show_Balance(acc_no3: AccountNo) balance: nat0 ext rd account_file : AllAccounts pre acc_no3 inset dom(account_file) post balance = account_file(acc_no3).balance comment 事前条件 : account_file に口座番号が acc_no と同じである口座が存在する事後条件 : acc_no と同じである口座の残高を出力変数 balance に与える end_process;

16 process Transfer(to_acc: AccountNo, amount: nat0, from_acc_no: AccountNo) error1: string ext wr account_file: AllAccounts pre from_acc_no inset dom(account_file) and to_acc inset dom(account_file) post if amount <= then let temacc = override(~account_file, {from_acc_no -> modify(~account_file(from_acc_no), balance -> (~account_file(from_acc_no) amount)}) in account_file = override(temacc, {to_acc -> modify(~account_file, balance -> ~account_file(to_acc).balance + amount)}) else error1 = The amount is over the limit. decom: Transfer_Decom; /* このプロセスは分解される */ comment 事前条件 : account_file に口座番号が from_acc_no かつ to_acc_no acc_no と同じである口座が存在する事後条件 : amount を account_file に口座番号が from_acc_no と同じである口座の残高から減らしその金額を口座番号が to_acc_no と同じである口座の残高に加えるただし amount は acc_no の口座の残高より大きいまたは 100 万円を超えるなら本振り込みができない end; end_module;

17 プロセス Transfer の分解 No. 2

18 module Transfer_Decom /SYSTEM_ATM; var ext #account_file: AllAccounts; behav: CDFD_No.2; process Get_To_Account(acc_no: AccountNo) acc: AllAccounts, check_am: sign ext rd account_file: AllAccounts pre acc_no inset dom(account_file) post acc = {acc_no -> account_file(acc_no)} comment 事前条件 : 口座番号が acc_no と同じである口座は account_file に入っている事後条件 : 口座番号が acc_no と同じである口座情報を出力 acc に与える end_process;

19 process Check_Amount(check_am: sign, amount: nat0) result: sign error_msg: string pre true post if amount <= then result = true else error_msg = The amount is over the limit. comment 事前条件 : ture 事後条件 : もし amount は 100 万円を超えるなら出力 result を false に成させるそでなければ result を true に成させる end_process;

20 process Transfer_To_Account(from_acc_no: AccountNo, acc: AllAccounts, result: sign) ext wr account_file: AllAccounts pre true post let temacc = override(~account_file, {from_acc_no -> modify(~account_file(from_acc_no), balance -> (~account_file(from_acc_no) amount)}) in account_file = override(temacc, override(acc, {get(dom(acc)) -> modify(get(rng(acc)), balance -> get(rng(acc)).balance + amount)}) comment 事前条件 : acc に振り込み先の口座情報しかないそして amount も 100 万円を超えていない事後条件 : account_file に口座番号は from_acc_no と同じである口座の残高から amount を減らしその amount を acc の残高に加えるそして account_file に acc と同じカスタマの口座情報を acc に置き換える end_process; end_module.

21 ATMのSOFL 形式設計仕様から生成したJavaプログラムの構造 public class SYSTEM_ATM { protected AllAccount account_file; /*account_fileは型 AllAccountで宣言する型 AllAccount は別な場所で適切に宣言する */ public SYSTEM_ATM(){ } /*SOFLのinitプロセスを対応するSYSTEM_ATM クラスのコンストラクタ */

22 public Receive_Command( ){ } /* プロセス Receive_Command を実装したインスタンスメソッド */ public Open_Account( ){ } /* プロセス Open_Account を実装したインスタンスメソッド */ public Authenticate( ){ } /* プロセス Authenticate を実装したインスタンスメソッド */

23 public Deposit( ){ } /* プロセス Deposit を実装したインスタンスメソッド */ public Withdraw( ){ } /* プロセス Withdraw を実装したインスタンスメソッド */ public Show_Balance ( ){ } /* プロセス Show_Balance を実装したインスタンスメソッド */

24 public Transfer ( ){ } /* プロセス Transfer を実装したインスタンスメソッド */ public main( ){ } /*SOFL 仕様に対応する CDFD を実装した main メソッド */ } // クラス SYSTEM_ATM 終了

25 public class Transfer_Decom extends SYSTEM_ATM { /*SOFL 仕様に定義されたモジュール Transfer_Decom からそれを実装するクラス Transfer_Decom へ変換このクラスは SYSTEM_ATM を継承 */ public Get_To_Account( ){ } /* プロセス Get_To_Accountを実装したインスタンスメソッド */ public Check_Amount( ){ } /* プロセス Check_Amountを実装したインスタンスメソッド */

26 public Transfer_To_Account( ){ } /* プロセス Transfer_To_Account を実装したインスタンスメソッド */ public Transfer_Decom_CDFD( ){ } /*SOFL 仕様に対応する CDFDを実装したインスタンスメソッド */ } // クラス Transfer_Decom 終了

27 Suica カードシステムの small プロジェクト 5 本プロジェクトでは Suicaカードシステムの SOFL 形式設計仕様またはDFD+ 構造化設計に基づきその設計仕様を実装するJavaプログラムを作成せよ

Microsoft PowerPoint ppt

Microsoft PowerPoint ppt 独習 Java ( 第 3 版 ) 6.7 変数の修飾子 6.8 コンストラクタの修飾子 6.9 メソッドの修飾子 6.10 Object クラスと Class クラス 6.7 変数の修飾子 (1/3) 変数宣言の直前に指定できる修飾子全部で 7 種類あるキーワード final private protected public static transient volatile 意味定数として使える変数同じクラスのコードからしかアクセスできない変数サブクラスまたは同じパッケージ内のコードからしかアクセスできない変数他のクラスからアクセスできる変数インスタンス変数ではない変数クラスの永続的な状態の一部ではない変数不意に値が変更されることがある変数