Contents

• Formal Model in the Z Style of a Body of Knowledge
• : Source

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