[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / class_managers_assistent
Wed Jun 1 11:18:40 PDT 2011

# The Class Manager's assistant

## Background

The theory of data bases is based on Discrete Mathematics. The boxes in a normalized ERD are just sets, and the lines are functions: many-to-one relations or mappings. Each table in a relational data base is just a set of tuples. The data base operations add and delete rows/tuples or change items in certain rows. You can use the operations in set theory -- union, intersection and complement to express some operations. Other operations need either specialized symbols of "set comprehensions".

Here I present a direct transaltion of Z into MATHS.... See [ class_managers_assistent1.html ] for the same system expressed as succintly as possible in MATHS.

## Example of Expressing Z-Style Dynamics

For example (Taken form "Software Development with Z" by J B Wordsworth 1992) suppose we are keeping track of students who enroll in a class, take a test, and may pass and be awarded a certificate when they leave the class or not get a certificate if they failed the test and leave the class.

1. Class_managers_assistant_state::=following,
Net
1. Students::Sets=given.
2. Enrolled::@Student.
3. Maximum_enrolled::Nat = given.
4. Tested::@Enrolled.
5. Passed::@Tested.
6. Failed::@Tested.

(End of Net)

Note -- the '@' symbol above is written as a curly-P and stands for "Power Set" -- the set of subsets.

2. Class_managers_assistant::=following,
Net

1. |-

2. |- (L): |Enrolled| <= Maximum_enrolled.
3. |- (T1):
4. |- (T2): No (Passed & Failed).

(End of Net)

3. Initially::= Class_managers_assistant_state with { Enrolled = {} }.

It is easy to show that initially the invariant condition is true and that nobody has been tested:

4. (above)|- (Init): \$ Initially ==> \$ Class_managers_assistant with { Tested = {} }.

5. For s:Students, Enroll(s)::=following,
Net

1. |-
2. |-s not_in Enrolled.
3. (-1)|-s not_in Tested.

4. |-|Enrolled| < Maximum_enrolled.
5. |-Enrolled'=Enrolled|{s}.
6. (-1, -2)|-|Enrolled'| <= Maximum_enrolled.

(End of Net)

Note: the above Net describes a change because it contains a variable with a prime ("'") on it.

Since in the description of Enroll(s) mentions Tested but does not mention Tested' (with a prime) we know that Tested does not change.

6. (above)|-For all s:Student, x: \$ Class_managers_assistant, x.Tested = x.Enrol(s).Tested.

7. Test_Result::={pass,fail}.

8. For s:Students, r:Test_Result, test(s,r)::=Class_managers_assistant with following,
Net

1. |-s in Enrolled ~ Tested.
2. |-If r=pass then Passed'=Passed | {s}.
3. |-If r=fail then Failed'=Failed | {s}.
4. (-1, -2, T1)|-s in Tested'.

(End of Net)

The following uses some abbreviations:

9. Leave(s)::=Class_managers_assistant with following,
Net

1. |-s in Enrolled.

2. |-Enrolled :~ s, Enrolled' = Enrolled ~ {s}.
3. (-1, Tested)|-s not_in Tested'.

4. Response::{certificate, no_certificate}.
5. response::Response= if(s in Passed, certificate, no_certificate).

(End of Net)

## Enquiries

10. For s, Enquiry(s)::=Class_managers_assistant with following
Net
1. response::{not_enrolled, enrolled, passed, failed}=following, (
1. if(s in Passed, passed, if (
1. s in Failed, failed, if (
1. s in Enrolled, enrolled, not_enrolled
)
)
).

(End of Net)

## Life Histories

Ignoring erroneous events...
11. Class_Life_History::= Initially; do( |enroll | |test | |leave).
12. Student_Life_History::= enroll; test; leave.

13. For s:Students, Enroll_fails(s)::=Class_managers_assistant with { s in Enrolled or |Enrolled| = Maximum_enrolled}.
14. For s, r, Test_fails(s,r)::=Class_managers_assistant with { s not_in Enrolled }.
15. Leave_fails(s)::=Class_managers_assistant with { s not_in Enrolled }.

## Proof of Init

Let
1. Since Enrolled is {}, |Enrolled| =0 < 1 and Maximum_enrolled is in Nat and so >= 1, we have L.

Further, Tested is a subset of Enrolled and so must also be empty ({}). Since Tested is empty, T1 and T2 are trivially fulfilled.

(Close Let )

. . . . . . . . . ( end of section Proof of Init) <<Contents | End>>

## More

More TBD when I have time and motivation... [click here CMA if you can fill this hole]

. . . . . . . . . ( end of section The Class Manager's assistant) <<Contents | End>>