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

Contents


    The Class Manager's assistant Version 2

      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 specialized symbols of "set comprehensions".

      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.

      A Z-style Specification

      In [ class_managers_assistent.html ] I present a more direct translation of Z into MATHS.

      MATHS with operations

      The theory for this style of specification can be found in [ ../maths/math_12_Structure.html ] and [ ../maths/math_14_Dynamics.html ] for the syntax and semantics.

    1. Class_managers_assistant::=following,
      Net
      1. Students::Sets=given.
      2. Enrolled::@Student.
      3. Maximum_enrolled::Nat = given.
      4. |-|Enrolled| <= Maximum_enrolled.

      5. Tested::@Enrolled.
      6. |-Tested >=={Passed, Failed}
      7. Initially::operation= ( Enrolled = {} ).

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

      8. (-1, -2)|- (Init): $ Initially ==> $ Class_managers_assistant with { Tested = {} }.

      9. For s:Students~Enrolled, Enroll(s)::operation= (|Enrolled| < Maximum_enrolled and Enrolled:|s)

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

      11. For s:Enrolled~Tested, r:Test_Result, test(s,r)::operation= (if r=pass then Passed:| s else Failed:|s).

      12. Status::={not_enrolled, enrolled, passed, failed}.

      13. For s:Students, Enquiry(s)::Status=following,
      14. if (
        1. s in Passed, passed, if (
          1. s in Failed, failed, if (
            1. s in Enrolled, enrolled, not_enrolled
            )
          )
        ).

      15. get_certificate::@(Students, Students)=given.

      16. For s:Enrolled, Leave(s)::operation=(Enrolled :~ s and (s in Passed and s get_certificate s' or s not_in Passed).


      (End of Net)

      Life Histories

      Ignoring erroneous events...
    2. Class_Life_History::= Initially; do( |Enroll | |Test | |Leave).
    3. For s:Students, Student_Life_History(s)::= Enroll(s); Test(s); Leave(s).

      To Be Done

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

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

End