とりとめのないことを書いております。
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 演習問題を解く(3)
E6.6

TYPES
- TEXTFILE
FUNCTIONS
- open : TEXTFILE x STRING |> TEXTFILE
- isopen : TEXTFILE -> BOOLEAN
- save : TEXTFILE -> TEXTFILE x BOOLEAN
- saveAs : TEXTFILE x STRING -> TEXTFILE x BOOLEAN
- close : TEXTFILE -> TEXTFILE
- lines : TEXTFILE |> INTEGER
- line : TEXTFILE x INTEGER |> STRING
- modify : TEXTFILE x INTEGER x STRING |> TEXTFILE
- delete : TEXTFILE x INTEGER |> STRING
- add : TEXTFILE x INTEGER x STRING |> TEXTFILE
- ismodified : TEXTFILE |> BOOLEAN
- undo : TEXTFILE |> TEXTFILE
AXIOMS
任意のt : TEXTFILE, i, j : INTEGER, s : STRINGに対して
[A1] not isopen(close(t))
[A2] line(modify(t, i, s), j) = (if i = j then s else line(t, j))
[A3] line(delete(t, i), j) = (if j < i then line(t, j) else line(t, j-1))
[A4] if (j < i) then line(add(t, i, s), j) = line(t, j)
[A5] line(add(t, i, s), i) = s
[A6] if (j > i) then line(add(t, i, s), j) = line(t, j-1)
[A7] lines(modify(t, i, s)) = lines(t)
[A8] lines(delete(t, i)) = lines(t) - 1
[A9] lines(add(t, i, s)) = lines(t) + 1
[A10] if isopen(open(t, s)) then not ismodified(open(t, s))
[A11] if (snd save(t)) then not ismodified(fst save(t))
[A12] if not (snd save(t)) then ismodified(fst save(t)) = ismodified(t)
[A13] if (snd saveAs(t, s)) then not ismodified(fst saveAs(t, s))
[A14] if not (snd saveAs(t, s)) then ismodified(fst saveAs(t, s)) = ism..d(t)
[A15] ismodified(modify(t, i, s))
[A16] ismodified(delete(t, i))
[A17] ismodified(add(t, i, s))
[A18] not ismodified(undo(modify(t, i, s))
[A19] not ismodified(undo(delete(t, i))
[A20] not ismodified(undo(add(t, i, s))
PRECONDITIONS
open(t) requires not isopen(t)
lines(t) requires isopen(t)
line(t, i) requires isopen(t)
modify(t, i, s) requires isopen(t)
delete(t, i) requires isopen(t)
add(t, i, s) requires isopen(t)
ismodified(t) requires isopen(t)
undo(t) requires isopen(t) and ismodified(t)

E6.7

TYPES
- HOUSE_BUYER
FUNCTIONS
- new : NONE -> HOUSE_BUYER
- find_property : HOUSE_BUYER -> HOUSE_BUYER
- property_found : HOUSE_BUYER -> BOOLEAN
- get_loan : HOUSE_BUYER -> HOUSE_BUYER
- loan_approved : HOUSE_BUYER -> BOOLEAN
- sign_contract : HOUSE_BUYER |> HOUSE_BUYER
- isdone : HOUSE_BUYER -> BOOLEAN
AXIOMS
任意のh : HOUSE_BUYERに対して
[A1] not property_found(new)
[A2] property_found(find_property(h))
[A3] property_found(get_loan(h)) = property_found(h)
[A4] property_found(sign_contract(h)) = property_found(h)
[A5~7] loan_approved...
[A8~10] isdone...
PRECONDITIONS
sign_contract(h) requires property_found(h) and loan_approved(h)

E6.8

TYPES
- STACK[G]
FUNCTIONS
- put : STACK[G] x G -> STACK[G]
- remove : STACK[G] |> STACK[G]
- item : STACK[G] |> G
- empty : STACK[G] -> BOOLEAN
- new : STACK[G]
- count : STACK[G] -> INTEGER
- change_top : STACK[G] x G |> STACK[G]
- wipe_out : STACK[G] -> STACK[G]
AXIOMS
任意のx : G, s : STACK[G]に対して
[A1] item(put(s, x)) = x
[A2] remove(put(s, x)) = s
[A3] empty(new)
[A4] not empty(put(s, x))
[A5] if empty(s) then count(s) = 0
[A6] count(put(s, x)) = count(x) + 1
[A7] change_top(s, x) = put(remove(s), x)
[A8] empty(wipe_out(s))
PRECONDITIONS
- remove(s:STACK[G]) require not empty(s)
- item(s:STACK[G]) require not empty(s)
- change_top(s:STACK[G], x:G) require not empty(s)

E6.9

TYPES
- STACK[G]
FUNCTIONS
- put : STACK[G] x G |> STACK[G]
- remove : STACK[G] |> STACK[G]
- item : STACK[G] |> G
- empty : STACK[G] -> BOOLEAN
- new : STACK[G]
- count : STACK[G] -> INTEGER
- capacity : INTEGER
AXIOMS
任意のx : G, s : STACK[G]に対して
[A1] item(put(s, x)) = x
[A2] remove(put(s, x)) = s
[A3] empty(new)
[A4] not empty(put(s, x))
[A5] if empty(s) then count(s) = 0
[A6] count(put(s, x)) = count(x) + 1
[A7] capacity >= 0
PRECONDITIONS
- put(s:STACK[G], x:G) require count(s) < capacity
- remove(s:STACK[G]) require not empty(s)
- item(s:STACK[G]) require not empty(s)

E6.10

TYPES
- QUEUE[G]
FUNCTIONS
- put : QUEUE[G] x G -> QUEUE[G]
- remove : QUEUE[G] |> QUEUE[G]
- item : QUEUE[G] |> G
- empty : QUEUE[G] -> BOOLEAN
- new : QUEUE[G]
AXIOMS
任意のx : G, q : QUEUE[G]に対して
[A1] if empty(q) then item(put(q, x)) = x
[A2] put(remove(q), x) = remove(put(q, x))
[A3] if empty(q) then empty(remove(put(q, x)))
[A4] empty(new)
[A5] not empty(put(q, x))
PRECONDITIONS
- remove(q) require not empty(q)
- item(q) require not empyt(q)

[スタックとキューの類似点]
・保持している個数は同じなので、emptyの公理、remove, itemの事前条件は同じ

[スタックとキューの相違点]
・スタックではput, removeが逆操作であるが、キューではそうでなく、
 putとremoveの関係を表すのに可換則や打ち消しルールが必要になった。

(※Exciteブログの制約によりopen, isopenをopen, isopenと表記している箇所があります)

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