とりとめのないことを書いております。
by tempurature
カテゴリ
全体
プログラミング
scheme
verilog
未分類
以前の記事
2016年 04月
2016年 03月
2016年 02月
2016年 01月
2015年 12月
2015年 11月
2015年 10月
2015年 09月
2015年 08月
2015年 07月
2015年 06月
2015年 03月
お気に入りブログ
PHPで競技プログラミング
メモ帳
最新のトラックバック
ライフログ
検索
タグ
人気ジャンル
ブログパーツ
最新の記事
情報処理技術者試験 お疲れ様..
at 2016-04-17 18:55
基本情報技術者試験 平成27..
at 2016-04-14 04:48
基本情報技術者試験 平成27..
at 2016-04-13 23:03
苦い薬(ハーブ、サプリメント..
at 2016-04-09 14:03
「おバカ度チェックリスト」を..
at 2016-03-24 09:54
外部リンク
ファン
記事ランキング
ブログジャンル
画像一覧
B.メイヤー「オブジェクト指向入門」6.10 演習問題を解く(2)
E6.3

TYPES
- BANK
- ACCOUNT
FUNCTIONS
- deposit : ACCOUNT x INTEGER |> ACCOUNT
- withdraw : ACCOUNT x INTEGER |> ACCOUNT
- balance : ACCOUNT -> INTEGER
- holder : ACCOUNT -> STRING
- changeName : ACCOUNT x STRING -> ACCOUNT
- new : STRING x INTEGER |> ACCOUNT
- open : BANK x ACCOUNT |> BANK
- close : BANK x ACCOUNT |> BANK
- exists : BANK x ACCOUNT -> BOOLEAN
AXIOMS
任意のb : BANK, a : ACCOUNT, c : INTEGER, s : STRINGに対して、
[A1] balance(deposite(a, c)) = balance(a) + c
[A2] balance(withdraw(a, c)) = balance(a) - c
[A3] holder(new(s, c)) = s
[A4] balance(new(s, c)) = c
[A5] holder(changeName(a, s)) = s
[A6] exists(open(b, a), a)
[A7] not exists(close(b, a), a)
PRECONDITIONS
deposit(a, c) requires c > 0
withdraw(a, c) requires c >= balance(a)
new(s, c) requires c > 0
open(b, a) requires not exists(b, a)
close(b, a) requires exists(b, a)

(※exciteブログの制限で、一部openをopenと表記しています)

E6.4

TYPES
- MAIL_MESSAGE
- MAIL_ADDRESS
- FILE_PATH
FUNCTIONS
- body : MAIL_MESSAGE -> STRING
- title : MAIL_MESSAGE -> STRING
- to : MAIL_MESSAGE -> LIST[MAIL_ADDRESS]
- cc : MAIL_MESSAGE -> LIST[MAIL_ADDRESS]
- bcc : MAIL_MESSAGE -> LIST[MAIL_ADDRESS]
- attachedFiles : MAIL_MESSAGE -> LIST[FILE_PATH]
- new : LIST[MAIL_ADDRESS] x LIST[MAIL_ADDRESS] x LIST[MAIL_ADDRESS] x STRING x STRING x LIST[FILE_PATH] -> MAIL_MESSAGE
- newReplyMessage : MAIL_MESSAGE x STRING x LIST[FILE_PATH] -> MAIL_MESSAGE
- newForwardMessage : MAIL_MESSAGE x LIST[MAIL_ADDRESS] x LIST[MAIL_ADDRESS] x LIST[MAIL_ADDRESS] -> MAIL_MESSAGE
- removeMe : LIST[MAIL_ADDRESS] -> LIST[MAIL_ADDRESS]
AXIOMS
任意のa, b, c : LIST[MAIL_ADDRESS], s, t, r : STRING, f, g : LIST[FILE_PATH] m : MAIL_MESSAGEに対して
[A1] (bodyに関する)
[A2] (title...)
[A3] (to...)
[A4] (cc...)
[A5] (bcc...)
[A6] (attachedFiles...)
[A7] body(newReplyMessage(m, s, f)) = s
[A8] title(newReplyMessage(new(a, b, c, s, t, f), s, g)) = "Re: " ++ s
[A9] to(newReplyMessage(new(a, b, c, s, t, f), s, g)) = removeMe(a)
[A10] cc(newReplyMessage(new(a, b, c, s, t, f), s, g)) = b
[A11] bcc( ... ) = c
[A12] attachedFiles( ... ) = f
[A13] body(newForwardMessage(m), a, b, c) = body(m)
[A14] title(...) = "Fw: " ++ title(m)
[A15] to(...) = a
[A16] cc(...) = b
[A17] bcc(...) = c
[A18] attachedFiles(...) = attachedFiles(m)

E6.5

TYPES
- NAME
FUNCTIONS
- newAngloSaxonPerson : STRING |> NAME
- newJapanesePerson : STRING |> NAME
- newChinesePerson : STRING |> NAME
- tostring : NAME -> STRING
AXIOMS
任意のn : NAME, s : STRINGに対して
[A1] tostring(newAngloSaxonPerson(s)) = s
[A2] tostring(newJapanesePerson(s)) = s
[A3] tostring(newChinesePerson(s)) = s
PRECONDITIONS
newAngloSaxonPerson(s) requires match(/^\S+ (\S\. )*\S+$/, s)
newJapanesePerson(s) requires match(/^\S+ \S+$/, s)
newChinesePerson(s) requires match(/^\S+ \S+(| \S+)$/, s)


[PR]
by tempurature | 2016-01-10 01:31 | プログラミング
<< Exciteブログでは本文中に... B.メイヤー「オブジェクト指向... >>