MATHS Model of Project

This is a formalization of a part of a project submitted by Shenning Wen to the CSci Dept CSUSB as part of his Masters Degree. It solely my own work and does not reflect the extreme usefulness of the Visual Basic and MS Access system that he produced.

Conceptual Model of the Legacy Data Base

1. Address::String.
2. Time_period::linearly_ordered_set.
3. Customer::Finite_sets.
4. ac::Customer->Address. This notation declares that ac is a map from Customers to addresses. See Maps.

5. Notice::Finite_sets.
6. tn::Notice->Time_period, time notice sent,
7. cn::Notice->Customer, customer to whom notice is sent.

8. Region::Finite_sets.
9. Store::Finite_sets.
10. rs::Store->Region, the store's region.

11. Bank::Finite_sets.

12. Account::Finite_sets.
13. ca::Account->Customer
14. ba::Account->Bank

15. Check::Finite_sets.
16. Status::Finite_sets.
17. tc::Check->Time_period,
18. sc::Check->Store,
19. ac::Check->Account,
20. st::Check->Status, status of check.

21. bad::Status.
22. Bad_check:: @ Check,

    
    

23. |- (1): For Check x, x in Bad_check iff st(x) = bad.

    The "|-" indicates an assertion without reason -- an axiom or assumption.

    
    

24. (1)|- (2): Bad_check= /st(bad).

    The "|-" above indicates an assertion with reason -- a theeorem.

25. Bad_customer::@Customer,

    
    

26. |- (3): for Customer x, x in Bad_customer iff for some Bad_check y ( x = ca( ac( y ) ) ).

    
    

27. (3)|- (4): Bad_customer= ca (ac (Bad_check)).

    
    

28. (2, 4)|- (5): Bad_customer= ca o ac o /st(bad).

    Proof of 5

    Substitute in 4 the values of Bad_check in 2.

    Proof of 4

    STANDARD overloading of functions from elements in domain to subsets of domain.

    Proof of 2

    STANDARD overloading of functions from elements in domain to substes of domain.

    The Datamart

    A Datamart is a summarized user-friendly subset of a large database called a data warehouse. A Data warehouse is a collection of data for many possible purposes, some of which are not known at the time of collection and storage. A data mart is focused on a few critical known user needs.

    In this case the user only wants to know about bad customers. It is not worth wasting storage in the datamart for information on all customers.

    The datamart is also simplified by relating checks directly to the customers that wrote them.

29. Data_Mart::=following,
    Net
    No need to duplicate the global definitions. Definitions for the Datamart are prefixed with a DM.
    1. DM_Customer::=Bad_Customer.
    2. DM_ac::DM_Customer->Address.
       
    3. |- (DM1): DM_ac = ac o DM_Customer. -- the ac map limited to operate on DM_Customer only.

    4. DM_Notice::Finite_sets=Notice.
    5. DM_tn::DM_Notice->Time_period, time notice sent,
       
    6. |- (DM2): DM_tn = tn o DM_Notice.
    7. DM_cn::DM_Notice->DM_Customer, customer to whom notice is sent.
       
    8. |- (DM3): DM_cn = cn o DM_Notice.

    9. DM_Account::@ Account = { a:Account || cs(a) in DM_Customer }.
    10. DM_ba::DM_Account->Bank = ba o DM_Account.
    11. DM_ca::DM_Account->DM_Customer = ca o DM_Account.

        I assume, below, that the executive is interested in all the checks that a bad customer tends whether they are good or bad. For an alternative see [ Exercise 1 ] below.

    12. DM_Check::@ Check = Checks written by bad customers.
        
    13. |- (DM4): DM_Check = { c: Check || ca(ac(c) in DM_Customer }.
    14. DM_bc::DM_Check->DM_Customer,
        
    15. |- (DM5): For DM_Check c, bc(c) = ca(ac(c)).

    16. DM_Bad_Check::= DM_Check & Bad_check.
        
    17. (DM_customer, DM_checks, DM5)|- (DM6): For all DM_Customer b, some DM_Bad_check c, DM_bc(c)=b.

        Proof of DM6

        
        Let
        
        
        1. (above)|-DM_customers are customers with at least one bad check.
           
        2. (above)|-DM_checks are all checks from DM_customers.
           
        3. (above)|-All bad_checks are in the DM.
           
        4. (above)|-The customer associated by the DM to a badcheck is by DM5, the customer in the main data base.
        
        (Close Let )
        

    
    (End of Net)
    
    

    Exercise 1

    Shenning Wen's datamart only showed Bad_checks. What do you change Data_Mart above to reflect this?

    Exercise 2

    Shenning Wen's datamart also limited the number of Bad_Checks and Notices in the Data Mart to 3 of each. What do you change in the result of Exercise 1 to reflect this? There are a number of ways to do this. Choose one that might suit a decision make and state why this is a good choice.

    Exercise 3

    Suppose that the datamart has a map from each customer to a account and each account to its bank. Is this necessarily true or does it add an assumption? Either prove correctness or state (and prove) a required axiom.

    References

    For a summary of the notation see [ math.syntax.html ]

30. linearly_ordered_set::= See http://csci.csusb.edu/dick/maths/math_21_Order.html#toset.
31. Maps::= See http://www.csci.csusb.edu/dick/maths/logic_5_Maps.html#Applying functions and maps.
32. o::=functional composition, see Relations and Maps. / ::=functional inversion, see ConverseRelations.
33. in::=is an element of set, see Sets
34. ConverseRelations::= See http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html#Converse Relations.
35. Relations::= See http://www.csci.csusb.edu/dick/maths/logic_40_Relations.html.
36. Sets::= See http://csci.csusb.edu/dick/maths/logic_30_Sets.html
37. STANDARD::= See http://csci.csusb.edu/dick/maths/math_11_STANDARD.html.
38. String::= See http://csci.csusb.edu/dick/maths/math_62_Strings.html.

. . . . . . . . . ( end of section MATHS Model of Project) <<Contents | End>>