[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / class_managers_assistent
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Wed Jun 1 11:18:40 PDT 2011

Contents


    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. |-Class_managers_assistant_state.


      2. |- (L): |Enrolled| <= Maximum_enrolled.
      3. |- (T1): Tested = Passed | Failed.
      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. |-Class_managers_assistant.
      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.

      Bad Events

    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. Initially.

          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 [socket symbol] CMA if you can fill this hole]

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

End