Zero Defect Notes - Part 1, general introduction
=================

* Purpose/scope: Insure that code conforms to a specification

* Method/outline: to develop a module:

    1. Describe the *intended function*: what does this module do?
    2. If the I/F can *clearly* be represented in code, code it, done.
    3. Decompose the overall intended function into pieces using
       only the four allowable branch constructs:
         -- sequence: do A, then do B
         -- alternation: if A then do B else do C
         -- while loop: while A do B
         -- definite iteration: for every x in S, do f(x)
    4. Verification: 2-4 reviewers *all* agree that it is *obvious*
       that the code matches the I/F.
    5. Recursively develop submodules, and match their I/Fs
       against the points where they are called.

- Ashby's Law of Requisite Variety: The complexity of the solution
  should match the complexity of the problem.


Simple Intended Functions
-------------------------

Def: intended function == a set of changes to *state objects*
  s1, s2, ..., sn & corresponding expressions e1, e2, ..., en, notated:
	[ (s1, s2, ..., sn) := (e1, e2, ..., en) ]

Def: state objects == things that have persistent values or states
    --  Examples:
        --- Variables
        --- I/O streams (contents, current position, permissions, ...)
        --- Return values
        --- Signals

-   All assignments are done in parallel

-   If any state object s, occurs in an expression, the *old* value
    is always meant.

-   An intended function is a *contract* between module and caller;
    if the caller satisfies my *preconditions* (if any), I can
    guarantee this set of state changes.

Example: (C)

    # [ (i,j) := (j,i) ]
    temp  =  i
    i     =  j
    j     =  temp

Example: (Python)

    # [ (i,j) := (j,i) ]
	i,j = j,i

Example:

	# [ inFile,line) := (inFile advanced past the end of the 
	#       current line, all characters remaining on the current line of 
	#       inFile) ]
	line = inFile.readline()


Compound intended functions
---------------------------

Def: compound intended function == a case structure imposed on a
    set of simple intended functions, that specifies which of the
    simple intended functions happen in which cases.

Example:
	# [ if a, b, and c are real numbers -> 
	#	  return a list of the real roots of a*x*2+b*x+c=0 ]
	def quadSolve(a, b, c):
        ...

Def: precondition == a true or false statement.  If the condition
    is false, I make no guarantees about state changes.

Example:

	# [ if x and y are numbers ->
	#	  z := sum of x and y
	#   else if x and y are strings ->
	# 	  z := x and y concatenated ]
	z = x + y

    --  In this example, if x and y are any other types, we make
        no guarantees about what happens.