[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [ MATHS ] / intro_objects
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Fri May 2 11:29:05 PDT 2008

Contents

    Documenting Objects in MATHS

    MATHS predates the OO explosion of the middle 1990s. However it had already incorporated several ideas that have been absorbed into OOP/OOA/OOD. Inheritance for example was present in some of the very earliest notes prepared like this in the late 1960's.

    An object has both a state and a pattern of behavior. Both of these must be documented:

    Static Aspects

    If you only look at the possible states that an object can have then you are looking at a static picture... and one that is easliy expressed by the record structures used in MATHS: [ intro_structures.html ]

    The static interrealtionships between objects is treated using the MATHS techniques that also apply to "data bases": [ math_13_Data_Bases.html ]

    Behavior

    The behavior of objects is expresed in diffeernt ways by different methodologists. One technique is to list and define the operations that apply to objects of a given class. THis can be like an Abstract Data Type. Or it can be describing the changes that can occur to an implicit object [ intro_dynamics.html ]

    MATHS can use the Z (Zed) approach of describing change in a complex object as a Net (schema):

  1. POINT::=following,
    Net
    1. x::real.
    2. y::real.

    (End of Net)

  2. For x0,y0:real, MOVE(x0,y0)::=following,
    Net

    1. |-POINT.
    2. |-POINT'.
    3. |-x'=x+x0 and y'=y+y0.

    (End of Net)

    These 'nets' can also be abreviated and used in expressions like this:

  3. Net{x,y:real}

  4. Operations::Partly_Baked_Idea=following,
    Net
      Another (as yet informal) convention could be to include object-oriented operations inside a Network of variables and predicates. For example
    1. POINT::=following
      Net
      1. x::real.

      2. y::real.

      3. For x0:real, setX(x0)::operation = (x'=x0).
      4. For y0:real, setY(y0)::operation = (y'=y0).
      5. For x0,y0:real, move(x0,y0)::operation = (x'=x+x0 and y'=y0+y).

      (End of Net POINT)

    2. p1: POINT(x=1,y=1).
    3. p2:= p1.move(-1,-1).

      or

    4. p1.move(1,1).

      The above is a Partly_Baked_Idea. In particular, the existence of operations and constraints (invariants) introduces the need to prove that the constraints of the Net are preserved by all operations.

      [click here [socket symbol] if you can fill this hole]


    (End of Net)

    Dynamics

    Davaid Harel invented the Statechart as an improvement of the Finite State Machine and these have been put into the UML. These can be expressed in MATHS but Jackson Life History Program technique gives a cleaner structure to problems. It also means that the states are deduced from the problem rather than guessed. Here the possible lives of an object in the class are written as structured running program. Each real object is a thread executing the program. [ math_75_Programs.html ] The threads run for as long as the real object exists... when the program is not running the object must be saved in a persistent form. When the real object becomes active the saved stae is restored and the life-history is restarted. The communication between these (highly poarallel) objects is close to that in CSP.

    Scenarios

    Scenarios can described in a simple structured form using: [ intro_ebnf.html ]

    Inheritance

    If you have already written the documentation for something called N then
  5. N and w is the result of adding a condition or well formed formula to N as a constraint.

    You can add a whole set of features to a piece of documentation called N by

  6. N with{ new_features}.

    Generics and Templates

    Any loosely bound terms in a piece of MATHS documentation is generic and can be replaced by a more tightly bound and so specific form.

    Notes on MATHS Notation

     Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle = Net{radius:Positive Real, center:Point}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  7. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html

    Glossary
  8. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  9. given::reason="I've been told that...", used to describe a problem.
  10. given::variable="I'll be given a value or object like this...", used to describe a problem.
  11. goal::theorem="The result I'm trying to prove right now".
  12. goal::variable="The value or object I'm trying to find or construct".
  13. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  14. hyp::reason="I assumed this in my last Let/Case/Po/...".
  15. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  16. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  17. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

End