[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / BoK
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Fri Sep 30 08:55:23 PDT 2011

Contents


    Formal Model in the Z Style of a Body of Knowledge

      Source

      [BowenReeves11]
    1. This is a translation of formal portion of slides (in Z) [ fm-2011-symposium-slides ] into MATHS:
    2. BOK::=following
      Net
      1. NAMES::Sets=given, "Names of entities".
      2. REFS::Sets=given, "References to external items.
      3. ENTRIES::@NAMES. A special kind of name.
      4. CATEGORIES::@NAMES. A special kind of name.
      5. |-No ENTRIES & CATEGORIES.
      6. BOK0::=following,
        Net
        1. entries::Finite_sets(ENTRIES).
        2. categories::Finite_sets(CATEGORIES).
        3. refs::Finite_sets(REFS).

        (End of Net)

      7. BOK1::=following,
        Net

        1. |-BOK0.
        2. links::@(ENTRIES, ENTRIES).
        3. cats::@(NAMES,CATEGORIES).
        4. citations::@(ENTRIES, REFS).
        5. |-pre(links) ==>entries.
        6. |-pre(cats) ==> entries | categories.
        7. |-pre(citations)==>entries.

        (End of Net)

      8. BOK2::=following,
        Net

        1. |-BOK1.
        2. |-rng(links) ==>entries.
        3. |-rng(cats) ==> categories.
        4. |-rng(citations)==>refs.

        (End of Net)

      9. BOK2a::=following,
        Net

        1. |-BOK2.
        2. nolinks::Finite_sets(ENTRIES) = entries ~ pre(links).
        3. nocats::Finite_sets(NAMES) = (entries | categories) ~ pre(cats).
        4. nocites::Finite_sets(ENTRIES)=entries ~ pre(citations).

        (End of Net)

      10. BOK2b::=following,
        Net

        1. |-BOK2a.
        2. orphans::Finite_sets(ENTRIES) = entries ~ rng(links).
        3. uncited::Finite_sets(REFS) = refs ~ rng(citations).

        (End of Net)

      11. BOK3::=following,
        Net

        1. |-BOK2b.
        2. |-entries = pre(links) = pre(citations).
        3. |-entries ==> pre(cats).

        (End of Net)

      12. BOK4::=following,
        Net

        1. |-BOK3.
        2. |-rng(links)=entries.
        3. |-rng(cats) = categories.
        4. |-rng(ciations) = refs.

        (End of Net)

      13. BOK5::=following,
        Net

        1. |-BOK4.
        2. |-links in Irreflexive(ENTRIES).
        3. |-cats in Irreflexive(CATEGORIES).

        (End of Net)

      14. BOK6::=following,
        Net

        1. |-BOK5.
        2. |-do( cats) in Irreflexive(CATEGORIES).

        (End of Net)

      15. BOK7::=following,
        Net

        1. |-BOK6.
        2. top_level_cats::Finite_sets(CATEGORIES) = rng(cats) ~ pre(cats).
        3. |-some top_level_cats.

        (End of Net)

      16. BOK8::=following,
        Net

        1. |-BOK7.
        2. (BOK4)|-rng( cats) = categories.

        (End of Net)

      17. BOK9::=following,
        Net

        1. |-BOK8.
        2. |-pre(links) | rng(do(links)) = entries.

        (End of Net)

      18. BOK10::=following,
        Net

        1. |-BOK9.
        2. |-pre(links) = rng(do(links)) = entries.

        (End of Net)


      19. |-BOK10.
      20. |-do(cats | /cats) (top_level_cats) = categories | entries.

      21. Irreflexive::= See http://cse.csusb.edu/dick/maths/math_11_STANDARD.html#Irreflexive.

      (End of Net)


    3. (dick)|-the above mimics the Z style in the slides. A MATHS model could use the language of directed graphs. [ ../maths/math_22_graphs.html ]

End