Constantes utilizadas en los casos de prueba

Estas constantes se utilizaron como sinónimos para abreviar la descripción de cada caso de prueba. Se considera que son identificadores globales y denotan la cadena de caracteres que identifican.

Todas las constantes denotan cadenas de caracteres. Es necesario que símbolos que aparecen en la definición de una constante hayan sido previamente definidos (es decir, se debe haber indicado su tipo). Todas las constantes son globales con respecto al documento en su totalidad, es decir, se pueden utilizar en todas las operaciones. Al mismo tiempo, no puede haber dos constantes con el mismo identificador.
CONSTANT u (U), u1 (U), u2 (U), u3 (U), u4 (U), root (U), secofr (U): SUBJECT
CONSTANT po (U), po1 (U), po2 (U), po3 (U), / (U): OBJNAME
CONSTANT OBJECT
(U) o ::= (po, File)
(U) o1 ::= (po1, File)
(U) o2 ::= (po2, File)
(U) o3 ::= (po3, File)
(U) barra ::= (/, Directory)
CONSTANT g (U), g1 (U), g2 (U), g3 (U), AG (U), RG (U), SAG (U): GRPNAME
CONSTANT GRPNAME -> (set SUBJECT)
(U) G ::= {g1 :-> {u}, RG :-> {root}, SAG :-> {secofr}, AG :-> {u, root, secofr}}
CONSTANT SUBJECT -> GRPNAME
(U) PG ::= {u :-> g1, root :-> RG, secofr :-> SAG}
CONSTANT nat
(U) M ::= 3
(U) N ::= 5
CONSTANT ADMIN (U), NETWORK (U), NATO (U), NUCLEAR (U): CATEGORY
CONSTANT FBI (U), SECOFR (U), ROOT (U), CIA (U), MENEM (U): CATEGORY
CONSTANT (set CATEGORY)
CAT ::= {NATO, NUCLEAR, FBI}
CONSTANT SUBJECT*SecClass
(U) rSC ::= root :-> [level := 0, categs := {ROOT}]
(U) soSC ::= secofr :-> [level := 0, categs := {SECOFR}]
(U) uSC ::= u :-> [level := N, categs := {FBI, NATO}]
(U) userSC ::= user :-> [level := M, categs := {NATO}]
CONSTANT (set SUBJECT*SecClass)
(U) SSC ::= {rSC, soSC, uSC, userSC}
CONSTANT OBJECT*SecClass
bSC ::= barra :-> [level := 0, categs := {}]
CONSTANT (set OBJECT*SecClass)
(U) OSC1 ::= {o1 :-> [level := M, categs := {FBI, NATO}], bSC}
(U) OSC ::= {o :-> [level := M, categs := {FBI, NATO}], bSC}
CONSTANT AccessCtrlListData
(U) aclo ::=
[owner := u,
group := g1,
UserReaders := {u},
GroupReaders := {},
UserWriters := {u},
GroupWriters := {},
UserOwners := {u},
GroupOwners := {RG}]
(U) acl/ ::=
[owner := root,
group := RG,
UserReaders := {root},
GroupReaders := {AG},
UserWriters := {root},
GroupWriters := {},
UserOwners := {root},
GroupOwners := {RG}]
(U) acl1 ::=
[owner := u1,
group := g1,
UserReaders := {u},
GroupReaders := {},
UserWriters := {u},
GroupWriters := {},
UserOwners := {u1},
GroupOwners := {RG}]
CONSTANT (set OBJECT*AccessCtrlListData)
(U) ACL ::=
{o :-> aclo,
barra :-> acl/}
(U) ACL1 ::=
{o1 :-> aclo,
barra :-> acl/}
CONSTANT x (U): BYTE
CONSTANT FILECONT
fc1 ::= < x >
CONSTANT (set OBJECT*FILECONT)
(U) F ::= {o :-> fc1}
(U) F1 ::= {o1 :-> fc1}
CONSTANT (set OBJECT*DIRCONT)
(U) D ::= {barra :-> < o.1 > }
(U) D1 ::= {barra :-> < o1.1 > }
CONSTANT ru (U), wu (U), pu (U): SUBJECT
CONSTANT rg (U), wg (U), pg (U): GRPNAME
CONSTANT GRPNAME -> (set SUBJECT)
(U) G3 ::=
{g :-> {u},
g1 :-> {u1},
g2 :-> {u2},
g3 :-> {u3},
RG :-> {root},
SAG :-> {secofr},
AG :-> {u, u1, u2, u3, root, secofr}}
CONSTANT SUBJECT -> GRPNAME
(U) PG3 ::=
{u :-> g,
u1 :-> g1,
u2 :-> g2,
u3 :-> g3,
root :-> RG,
secofr :-> SAG}
CONSTANT (set OBJECT*ReadersWriters)
(U) SM2 ::=
{o1 :-> [ActReaders := {u1}, ActWriters := {}],
o2 :-> [ActReaders := {}, ActWriters := {u1}],
o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}
(U) SM ::=
{o1 :-> [ActReaders := {u1}, ActWriters := {}]}
(U) SM3 ::=
{o :-> [ActReaders := {u1}, ActWriters := {}],
o2 :-> [ActReaders := {}, ActWriters := {u1}],
o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}
CONSTANT (set OBJECT*SecClass)
(U) OSCSM ::=
{o :-> [level := N, categs := {FBI, NATO}],
o1 :-> [level := N, categs := {FBI, NATO}],
bSC}
(U) OSC2 ::=
{o :-> [level := N, categs := {FBI, NATO}],
o1 :-> [level := N, categs := {FBI, NATO}],
o2 :-> [level := N, categs := {FBI, NATO}],
o3 \ bSC}
(U) OSC3 ::=
{o1 :-> [level := N, categs := {FBI, NATO}],
o2 :-> [level := N, categs := {FBI, NATO}],
o3 \ bSC}
CONSTANT OBJECT*AccessCtrlListData
(U) aclo1 ::=
[owner := u1,
group := g1,
UserReaders := {u1},
GroupReaders := {AG},
UserWriters := {u},
GroupWriters := {},
UserOwners := {u1},
GroupOwners := {RG}]
(U) aclo2 ::=
[owner := u2,
group := g2,
UserReaders := {u2},
GroupReaders := {AG},
UserWriters := {u1},
GroupWriters := {},
UserOwners := {u2},
GroupOwners := {RG}]
(U) aclo3 ::=
[owner := u3,
group := g3,
UserReaders := {u1},
GroupReaders := {AG},
UserWriters := {u},
GroupWriters := {AG},
UserOwners := {u3},
GroupOwners := {RG}]
CONSTANT (set SUBJECT*SecClass)
(U) SSC2 ::=
{u :-> [level := N, categs := {FBI, NATO}],
u1 :-> [level := N, categs := {FBI, NATO}],
u2 :-> [level := N, categs := {FBI, NATO}],
u3 :-> [level := N, categs := {FBI, NATO}], rSC, soSC}
CONSTANT (set OBJECT*FILECONT)
(U) F2 ::=
{o :-> fc1,
o1 :-> fc1,
o2 :-> fc1,
o3 :-> fc1, }
(U) F3 ::=
{o1 :-> fc1,
o2 :-> fc1,
o3 :-> fc1, }
CONSTANT (set OBJECT*DIRCONT)
(U) D2 ::= {barra :-> < o.1, o1.1, o2.1, o3.1> }
(U) D3 ::= {barra :-> < o1.1, o2.1, o3.1> }
CONSTANT RIGHTS
(U) ff ::= [read_right := false, write_right := false]
(U) rf ::= [read_right := true, write_right := false]
(U) rw ::= [read_right := true, write_right := true]
(U) fw ::= [read_right := false, write_right := true]
CONSTANT PERMS
Sólo se consideran las configuraciones más habituales; podrían considerarse todas las configuraciones posibles y generar un caso para cada una.
(U) perms1 ::= [ownerp := rf, groupp := ff, otherp := ff]
(U) perms2 ::= [ownerp := rw, groupp := ff, otherp := ff]
(U) perms3 ::= [ownerp := rw, groupp := rf, otherp := ff]
(U) perms4 ::= [ownerp := rw, groupp := rw, otherp := ff]
(U) perms5 ::= [ownerp := rw, groupp := rw, otherp := rf]
(U) perms6 ::= [ownerp := rw, groupp := rw, otherp := rw]
CONSTANT SecClass
sc := [level := M, categs := {FBI, NATO, CIA, MENEM}]
CONSTANT ACL2 (U): (set OBJECT*AccessCtrlListData)
{o :-> aclo,
o1 :-> aclo1,
o2 :-> aclo2,
o3 :-> aclo3,
barra :-> acl/}
CONSTANT GRPNAME -> (set SUBJECT)
G4 :=
{g :-> {u},
g1 :-> {u1},
g2 :-> {u2},
g3 :-> {u3},
RG :-> {root},
SAG :-> {secofr, u3},
AG :-> {u, u1, u2, u3, root, secofr}}
CONSTANT (set OBJECT*ReadersWriters)
SM4 :=
{o1 :-> [ActReaders := {u}, ActWriters := {}],
o2 :-> [ActReaders := {}, ActWriters := {u1}],
o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}
SM5 :=
{o1 :-> [ActReaders := {u1}, ActWriters := {}],
o2 :-> [ActReaders := {}, ActWriters := {u,u1}],
o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}
CONSTANT p (U), p1 (U): OBJNAME
CONSTANT pd (U), pf (U): OBJNAME
CONSTANT OBJECT
(U) od ::= (pd, Directory)
(U) of ::= (pf, File)
CONSTANT (set OBJECT*FILECONT)
(U) Fof ::=
{of :-> fc1,
o1 :-> fc1,
o2 :-> fc1,
o3 :-> fc1, }
CONSTANT (set OBJECT*DIRCONT)
(U) Dof ::= {barra :-> < of.1, o1.1, o2.1, o3.1> }
(U) Dod ::=
{barra :-> < od.1, o1.1, o2.1, o3.1>,
od :-> < >}
CONSTANT (set OBJECT*SecClass)
(U) OSCod ::=
{od :-> [level := N, categs := {FBI, NATO}],
o :-> [level := N, categs := {FBI, NATO}],
o1 :-> [level := N, categs := {FBI, NATO}],
o2 :-> [level := N, categs := {FBI, NATO}],
o3 :-> [level := N, categs := {FBI, NATO}],
bSC }
CONSTANT AccessCtrlListData
(U) acl/2 ::=
[owner := root,
group := RG,
UserReaders := {root},
GroupReaders := {AG},
UserWriters := {root},
GroupWriters := {AG},
UserOwners := {root},
GroupOwners := {RG}]
CONSTANT (set OBJECT*AccessCtrlListData)
(U) ACLod ::=
{od :-> aclo,
o :-> aclo,
o1 :-> aclo1,
o2 :-> aclo2,
o3 :-> aclo3,
barra :-> acl/2}
CONSTANT GRPNAME -> (set SUBJECT)
(U) G2 ::=
{g1 :-> {u, user},
RG :-> {root},
SAG :-> {secofr},
AG :-> {u, user, root, secofr}}
CONSTANT SUBJECT -> GRPNAME
(U) PG2 ::= {u :-> g1, user :-> g1, root :-> RG, secofr :-> SAG}
CONSTANT AccessCtrlListData
(U) acl2o ::=
[owner := u,
group := g1,
UserReaders := {root},
GroupReaders := {g1},
UserWriters := {u},
GroupWriters := {},
UserOwners := {u},
GroupOwners := {RG}]
CONSTANT (set OBJECT*AccessCtrlListData)
(U) ACL2 ::=
{o :-> acl2o,
barra :-> acl/}
CONSTANT (set OBJECT*AccessCtrlListData)
(U) ACL/2 ::=
{o :-> aclo,
o1 :-> aclo1,
o2 :-> aclo2,
o3 :-> aclo3,
barra :-> acl/2}