Download Spec2Box - Adelard

Transcript
10.16
.3
.4
.5
12.1
.2
.3
.4
.5
.6
.7
13.1
.2
.3
.4
.5
.6
.7
14.1
Illustrative examples
post
(;;
r 62dom odm ^
(;;
odm = odm [ fr 7! od g;
NEWAC (cu : Cno ) r : Acno
m Overdraft
ext rd odm : Cno ;!
m Acdata
wr acm : Acno ;!
pre cu 2 dom odm
post
;; ^
r 62dom (
acm
;; [ fr 7! mk-Acdata (cu ,0)g;
acm = (
acm
m Balance
ACINF (cu :Cno ) r : Acno ;!
m Acdata
ext rd acm : Acno ;!
post
r = f acno 7! (acm (acno )).bal
j acno 2 dom acm .
(acm (acno )).own = cu
g
end Bank
SpecBox User Manual, version: PC/2.21a