ENROLLMENT, student=s, class=c, grade'=g}, and
1. For a,d:classes, student s adds a drops d::=$ Net{ENROLLMENT, student=s, class=d, class'=a }.

   If a record (in a database, program, object, etc) is described by named documentation N=Net{D} thenN' (N-prime) stands for network with the same variables as N, but with he variables in its wffs decorated by a prime[ as in Z]. For example

2. Example_of_prime_in_action::=
   Net{

   1. students::=PERSON->STUDENT,
   2. STUDENT::=
      Net{

      1. person::people.
      2. class_level::FR|SO|JR|SR,
      3. units::Real,
      4. GPA::Real.
         
      5. |- (inv): class_level=FR iff units<25.00,...
         }.

      then
      
   3. |-STUDENT'=
      Net{

      1. person::people.
      2. class_level::FR|SO|JR|SR,
      3. units::Real,
      4. GPA::Real.
         
      5. |- (inv): class_level'=FR iff units'<25.00,...
         }.

      Notice that the primes are not placed on the declarations. Thus
   4. Δ_STUDENT::=Net{ |-STUDENT. |-STUDENT'.} means the same as writing
   5. Δ_STUDENT::=
      Net{

      1. person::people.
      2. class_level::FR|SO|JR|SR,
      3. units::Real,
      4. GPA::Real.
         
      5. |-class_level=FR iff units<25.00,...
         
      6. |-class_level'=FR iff units'<25.00,...
         }.

      By the way the effect of a duplicate label on a statement is merely make it ambiguous and so invisible to the outside world. Labels do not change the meanings - they make it easier for simple markup system to do part of the work of making formal documentation look good. Notice that when combining two schema like this duplicate labels are hidden.

      Putting these above rules to work we can document the end of quarter update to an enrolment as

   6. For s:students, c:classes, g:{A,B,C,D,F}, finish_class(s, c, g) ::=$ following,
      Net
      
      
      1. |-STUDENT.
         
      2. |-STUDENT'.
         
      3. |- (gpa): units'*GPA'=units*GPA+g.(A+>4 | B+>3 | C+>2 | D+>1 | else+>0 ),
         
      4. |- (units): units'=units+units(c)

      
      (End of Net finish_class)
      
      The occurence of STUDENT and STUDENT' in the above definition declares the variables { person, class_level, units, GPA} and also enforces the formula class_level=FR iff units<25.00,... before and `class_level'=FR iff units'<25.00,...`

   
   }=::Example_of_prime_in_action.

   In general the effect of

3. Δ_D::=$ following,
   Net
   
   
   1. |-D.
      
   2. |-D'.

   
   (End of Net)
   
   is to assert that the constraint in D must be invariant under any change that uses Δ_D, or just has D, D' in it. Hence (like Z), for a piece of documentation D with name N we can define
4. Δ(N)::= N with N'. Similarly, the need for a set of variable to remain constant can be documented by:
5. Ξ(N)::=Δ(N) and for v:variables(N)(v=v').

   Conveniences

   It is usually convenient to omit the types of the variables when dynamic predicates appear in a relational expression. In this case the the predicate inherits the previous state space. Further, the dollars and braces can be ommitted without ambiguity. If Example=(y::Int; y'=x; do(y>3; y'=y-3);y<=3)
6. then
7. Example =$ Net{y:Int}; $ Net{y'=x};do($ Net{y>0}; $ Net{y'=y-3};$ Net{y<=0} =$ Net{y::Int,y'=x};do($ Net{y:Int, y>0}; $ Net{y:Int, y'=y-3};$ Net{y:Int, y<=0}.

   Calculations

   There is a calculus of programs! Here is a taster:

   Problem

   Given N1 and N2 are Dynamic - calculate $ N1;$ N2.

   Algorithm

   Suppose $ N3= $ N1; $ N2 then N3 is found by

   List

   1. Add assertions of form v=v'' for all variables v that are not dynamic in N1 or N2.
   2. Add an apostrophe to all variables in N2.
   3. Combine all declarations and definitions.
   4. If a variable appears with one apostrophe but not with two then add an apostrophe to it
   5. Apply existential quantifier to all variables with a single apostrophe.
   6. Change single prime variables to other names, and hide them
   7. Replace double primes by primes.
   8. Simplify and remove redundant invariant assertions

   . . . . . . . . . ( end of section List) <<Contents | End>>

   Example Calcuations

   
   
   1. (above)|- (ex1): (x'=x+1;x'=a*x)=(x'=a*x+a).

      Proof of ex1

   2. Consider{
      (x'=x+1;x'=a*x)=
      1. =(x'=x+1 and (x''=a*x' and a=a''))
      2. = (x'=x+1 and x''=a*x' and a=a'')
      3. =for some x'(x'=x+1 and x''=a*x' and a=a'')
      4. =for some w(w=x+1 and x''=a*w and a=a'')
      5. = for some w(w=x+1 and x'=a*w and a=a')
      6. (simp) =for w:=x+1(x'=a*w and a=a')
      7. (subs) =( x'=a*(x+1))
      8. (alg) =(x'=a*x+a).
         }
      
      
   3. |- (arith swap): (x'=x-y;y'=x+y;x'=y-x) = (x'=y and y'=x)

      Proof of arith swap

      This assumes that the operations of plus and minus etc follow the normal rules of algebra - a group even when overflow occurs.
   4. Consider{
      (x'=x-y;y'=x+y;x'=y-x)
      1. = $ Net{x'=x-y, y'=y, y''=x'+y', x''=x'};x'=y-x
      2. = for some a,b(a=x-y and b=y and y''=a+b and x''=a);x'=y-x
      3. = ((y''=x-y+y and x''=x-y);x'=y-x)
      4. = ((y'=x and x'=x-y);x'=y-x)
      5. = (y'=x and x'=x-y and y''=y' and x''=y'-x')
      6. = (x'=y and y'=x)
         }.
      
      
   5. (above)|- (exercise): (x'=x^y;y'=x^y;x'=y^x) = (x'=y and y'=x) where x^y=map[i:bits(x)] (x[i] iff y[i]).
      
   6. (above)|- (Shuttle swap): (z'=x; x'=y; y'=z) ==> (x'=y and y'=x)

      Proof of Shuttle swap

   7. Consider{
      (z'=x; x'=y; y'=z)
      1. = ( (z'=x; x'=y); y'=z)
      2. = ( z'=x and x'=y and y'=y); (y'=z)
      3. =$ Net{ ( z'=x and x'=y and y'=y) and y''=z' ) }
      4. =$ Net{ z'=x and x'=y and y'=y and y''=z' }
      5. = $ Net{ z'=x and x''=y and y'=y and y''=z' }
      6. = ( z''=x and x''=y and y'=y and y''=z''=x)
      7. = ( x''=y and y''=z''=x)
      8. = ( x'=y and y'=z'=x)
      9. ==> ( x'=y and y'=x)
         }.

      Quasi-Normal Form

      It is easy to show that any relational expression with no 'do's and made up of simple dynamic predicates can have its semicolons removed and be reduced to a non-unique but standard conjunctive form:
   8. Consider{
      (x>0; y'=2*x; y<6; x'=y-1)
      1. =(x>0;y'=2*x; y<6 and x'=y-1 )
      2. =(x>0;y'=2*x and y<6 and x'=2*x-1 )
      3. =(x>0 and y'=2*x and y<6 and x'=2*x-1 )
      4. =(x>0 and 2*x<6 and y'=2*x and x'=2*x-1 )
      5. =(x in [0..3] and y'=2*x and x'=2*x-1 )
      6. =(x in [0..3] and (x',y')=(2*x-1, 2*x)).
         }.
   9. Consider{
      (x<0; x'=-x | x>=0)
      1. = (x<0 and x'=-x | x>=0)
      2. = ( (x<0 and x'=-x ) or x>=0).
         }.

   . . . . . . . . . ( end of section Calculations) <<Contents | End>>

   Sequential Structures

   Sequence

   1. R1;R2;R3;...

      Blocks

      
      (block): with(D)(R)

      Selections

      
      (sel): R1|R2|R3|...
      (ifthenelse): A;R1 | (~A);R2 (case |[c:cases](R(c))

      Iterations

      
      (iter): do(R)
      (while): do(C; R);no(C)
      (for): with(i)(i'=a; while(b)(S; c)
      (until): R; do(C; R);no(C)

   . . . . . . . . . ( end of section Sequential Structures) <<Contents | End>>

   Concurrent Structures

   See [ math_76_Concurency.html ] and [ math_73_Process_algebra.html ] for more.

   Data flow Diagrams

   1. DFD::="Data Flow Diagrams".

      These are still used by systems analysts even tho' they are no longer fashionable [ http://www.csci.csusb.edu/dick/papers/rjb04bDFDs/ ] and misunderstood.

      A combination of my Flosets and standard Digraphs can be used to model systems of communicating parts: [ math_23_Flow_Diagrams.html ] without specifying the precise interactions.

      [click here if you can fill this hole]

      Parallel Operations

      The intersection of two relations requires both of them to hold:
   2. Simultaneous R1 & R2

      Notice that a simple expression can stop the processing
      

   3. |-(x'=x+1) & (x'=x-1) = false.

      Worse
      

   4. |-(x'=x+1) & (y'=y+1) = false. Because each assignment locks the other variable! However:
      
   5. |-(x'=x+1 and y'=y') & (y'=y+1 and x'=x') = (x'=x+1 and y'=y+1), and does what was probably wanted.

      This motivates the follwoing two abbreviations:

   6. free(v)::=(v'=v'),
   7. lock(v)::=(v=v'),

      .RoadWorksAhead

   8. wait(v) :=until( v<>v' ) ( free(v) ).

      Most intractable problems have a form like this. [click here if you can fill this hole]

   . . . . . . . . . ( end of section Concurrent Structures) <<Contents | End>>

. . . . . . . . . ( end of section Dynamics) <<Contents | End>>

Notes on MATHS Notation

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

For a more rigorous description of the standard notations see