Up one level to University of Stirling - LOTOS Activities
Jin Sa and Brian C. Warboys. Specifying concurrent object-based systems using combined specification notations. Technical Report UMCS-91-7-2, Department of Computer Science, University of Manchester, Manchester, UK, July 91.
See Incremental requirements specification and the constraint-oriented style in LOTOS for the background to this specification.
specification FileAccessSystem : noexit
library
Boolean, NaturalNumber, String, OctetString
endlib
type Op is Boolean, NaturalNumber
sorts Op
opns
open, read, write, close, save : -> Op
op0, op1, op2, op3 : -> Op
Ord : Op -> Nat
_ eq _, _ ne _ : Op, Op -> Bool
eqns
forall op1, op2 : Op
ofsort Nat
Ord (open) = 0;
Ord (read) = Succ (Ord (open));
Ord (write) = Succ (Ord (read));
Ord (close) = Succ (Ord (write));
Ord (save) = Succ (Ord (close));
Ord (op0) = Succ (Ord (save));
Ord (op1) = Succ (Ord (op0));
Ord (op2) = Succ (Ord (op1));
Ord (op3) = Succ (Ord (op2))
ofsort Bool
op1 eq op2 = Ord (op1) eq Ord (op2);
op1 ne op2 = not (op1 eq op2)
endtype (* Op *)
type Dir is NaturalNumber
sorts Dir
opns
inv, ret : -> Dir
Ord : Dir -> Nat
_ eq _, _ ne _ : Dir, Dir -> Bool
eqns
forall dir1, dir2 : Dir
ofsort Nat
Ord (inv) = 0;
Ord (ret) = Succ (Ord (inv))
ofsort Bool
dir1 eq dir2 = Ord (dir1) eq Ord (dir2);
dir1 ne dir2 = not (dir1 eq dir2)
endtype (* Dir *)
type Orig is NaturalNumber
sorts Orig
opns
t1, t2, app : -> Orig
Ord : Orig -> Nat
_ eq _, _ ne _ : Orig, Orig -> Bool
eqns
forall orig1, orig2 : Orig
ofsort Nat
Ord (t1) = 0;
Ord (t2) = Succ (Ord (t1));
Ord (app) = Succ (Ord (t2))
ofsort Bool
orig1 eq orig2 = Ord (orig1) eq Ord (orig2);
orig1 ne orig2 = not (orig1 eq orig2)
endtype (* Orig *)
type Octs is OctetString
opns
_--_ : OctetString, OctetString -> OctetString
eqns
forall o1, o2 : Octet, os1, os2 : OctetString
ofsort OctetString
<> -- os2 = <>;
os1 -- <> = os1;
o1 eq o2 =<
(o1 + os1) -- (o2 + os2) = os1 -- os2;
o1 ne o2 =<
(o1 + os1) -- (o2 + os2) = <>;
endtype (* Octs *)
behaviour
hide fh, t1, t2 in
Sys [fh, t1, t2]
where
process Sys [fh, t1, t2] : noexit :=
SysGen [fh]
||
FH [fh]
||
(
Appl [fh, t1, t2]
|[t1, t2]|
(T1 [fh, t1] ||| T2 [fh, t2])
)
where
process SysGen [fh] : noexit :=
SysOpen [fh]
|[fh]|
SysClose [fh]
|[fh]|
SysWrite [fh]
where
process SysOpen [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[(op eq open) implies (orig eq t1)];
SysOpen [fh]
endproc (* SysOpen *)
process SysClose [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[(op eq close) implies (orig eq t1)];
SysClose [fh]
endproc (* SysClose *)
process SysWrite [fh] : noexit :=
fh ! read ! inv ? octs : OctetString ! t1;
fh ? op : Op ? dir : Dir ? octs : OctetString ! t1;
SysWrite1 [fh]
[]
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[(op ne read) or (dir ne inv) or (orig ne t1)];
SysWrite [fh]
where
process SysWrite1 [fh] : noexit :=
fh ! read ! ret ? octs : OctetString ! t1;
SysWrite [fh]
[]
fh ? op : Op ? dir : Dir ? octs : OctetString ! t1
[(op ne read) or (dir ne ret)];
SysWrite1 [fh]
endproc (* SysWrite1 *)
endproc (* SysWrite *)
endproc (* SysGen *)
process FH [fh] : noexit :=
FHComm [fh] || FHOper [fh] || FHCall [fh] || FHData [fh]
where
process FHComm [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig;
FHComm [fh]
endproc (* FHComm *)
process FHOper [fh] : noexit :=
FHOpname [fh] || FHOpen [fh] || FHClose [fh] || FHSave [fh]
where
process FHOpname [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig;
FHOpname [fh]
endproc (* FHOpname *)
process FHOpen [fh] : noexit :=
fh ! open ! inv ? octs : OctetString ? orig : Orig;
FHOpen1 [fh]
where
process FHOpen1 [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[(op ne open) or (dir ne inv)];
FHOpen1 [fh]
endproc (* FHOpen1 *)
endproc (* FHOpen *)
process FHClose [fh] : noexit :=
FHClose1 [fh]
[>
fh ! close ! ret ? octs : OctetString ? orig : Orig;
stop
where
process FHClose1 [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[(op ne close) or (dir ne ret)];
FHClose1 [fh]
endproc (* FHClose1 *)
endproc (* FHClose *)
process FHSave [fh] : noexit :=
fh ! write ? dir : Dir ? octs : OctetString ? orig : Orig;
FHSave1 [fh]
[]
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[op ne write];
FHSave [fh]
where
process FHSave1 [fh] : noexit :=
fh ! save ? dir : Dir ? octs : OctetString ? orig : Orig;
FHSave [fh]
[]
fh ? op : Op ? dir : Dir ? octs : OctetString ? orig : Orig
[op ne save];
FHSave1 [fh]
endproc (* FHSave1 *)
endproc (* FHSave *)
endproc (* FHOper *)
process FHCall [fh] : noexit :=
fh ? op : Op ! inv ? octs : OctetString ? orig : Orig;
fh ! op ! ret ? octs : OctetString ! orig;
FHCall [fh]
endproc (* FHCall *)
process FHData [fh] : noexit :=
FHNotIO [fh] ||| ((FHRead [fh] ||| FHWrite [fh]) || FHFile [fh] (<>))
where
process FHNotIO [fh] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString
[(op ne read) and (op ne write)];
FHNotIO [fh]
endproc (* FHRead *)
process FHRead [fh] : noexit :=
fh ! read ! ret ? octs : OctetString ? orig : Orig;
FHRead [fh]
endproc (* FHRead *)
process FHWrite [fh] : noexit :=
fh ! write ! inv ? octs : OctetString ? orig : Orig [octs ne <>];
FHWrite [fh]
endproc (* FHWrite *)
process FHFile [fh] (octs : OctetString) : noexit :=
fh ! write ! inv ? octs1 : OctetString ? orig : Orig;
FHFile [fh] (octs ++ octs1)
[]
fh ! read ! ret ! octs ? orig : Orig;
FHFile [fh] (octs)
endproc (* FHFile *)
endproc (* FHData *)
endproc (* FH *)
process T1 [fh, t1] : noexit :=
T1Op1 [fh, t1] ||| T1Op2 [fh, t1] ||| T1Op3 [fh, t1]
where
process T1Op1 [fh, t1] : noexit :=
t1 ! op1 ! inv ! <> ! app;
fh ! open ! inv ? octs : OctetString ! t1;
fh ! open ! ret ? octs : OctetString ! t1;
t1 ! op1 ! ret ! <> ! app;
T1Op1 [fh, t1]
endproc (* T1Op1 *)
process T1Op2 [fh, t1] : noexit :=
t1 ! op2 ! inv ? octs1 : OctetString ! app;
fh ! read ! inv ? octs : OctetString ! t1;
fh ! read ! ret ? octs2 : OctetString ! t1;
fh ! write ! inv ! octs1 ! t1;
fh ! write ! ret ? octs : OctetString ! t1;
fh ! read ! inv ? octs : OctetString ! t1;
fh ! read ! ret ? octs3 : OctetString ! t1;
t1 ! op2 ! ret ! octs3 -- octs2 ! app;
T1Op2 [fh, t1]
endproc (* T1Op2 *)
process T1Op3 [fh, t1] : noexit :=
t1 ! op3 ! inv ! <> ! app;
fh ! close ! inv ? octs : OctetString ! t1;
fh ! close ! ret ? octs : OctetString ! t1;
t1 ! op3 ! ret ! <> ! app;
T1Op3 [fh, t1]
endproc (* T1Op3 *)
endproc (* T1 *)
process T2 [fh, t2] : noexit :=
t2 ! op0 ! inv ? octs : OctetString ! app;
fh ! write ! inv ! octs ! t2;
fh ! write ! ret ? octs : OctetString ! t2;
t2 ! op0 ! ret ! <> ! app;
T2 [fh, t2]
endproc (* T2 *)
process Appl [fh, t1, t2] : noexit :=
fh ? op : Op ? dir : Dir ? octs : OctetString ! app;
Appl [fh, t1, t2]
[]
t1 ? op : Op ? dir : Dir ? octs : OctetString ! app;
Appl [fh, t1, t2]
[]
t2 ? op : Op ? dir : Dir ? octs : OctetString ! app;
Appl [fh, t1, t2]
endproc (* Appl *)
endproc (* Sys *)
endspec (* FileAccessSystem *)
Up one level to University of Stirling - LOTOS Activities