Sample: 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.

Class_managers_assistant::=following,
Net

Students::Sets=given.
Enrolled::@Student.
Maximum_enrolled::Nat = given.
|-|Enrolled| <= Maximum_enrolled.
Tested::@Enrolled.
|-Tested >=={Passed, Failed}
Initially::operation= ( Enrolled = {} ).
It is easy to show that initially the invariant is true and nobody has been tested:
(-1, -2)|- (Init): $ Initially ==> $ Class_managers_assistant with { Tested = {} }.
For s:Students~Enrolled, Enroll(s)::operation= (|Enrolled| < Maximum_enrolled and Enrolled:|s)
Test_Result::={pass,fail}.
For s:Enrolled~Tested, r:Test_Result, test(s,r)::operation= (if r=pass then Passed:| s else Failed:|s).
Status::={not_enrolled, enrolled, passed, failed}.
For s:Students, Enquiry(s)::Status=following,
if (
1. s in Passed, passed, if (
  1. s in Failed, failed, if (
    1. s in Enrolled, enrolled, not_enrolled
    )
  )
).
get_certificate::@(Students, Students)=given.
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...

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]