Definitions:
  Implementation defined:  Arbitrary at the discretion of the
    underlying MMII implementation.
  Undefined: Any behaviour at all.  You may not rely on it.
    The program may or may not crash, monkey may or may not
    fly out of your monitor, etc.
  "It is an error to <foo>": Doing <foo> will result in undefined
    behaviour.
  Application defined:  Anything written by you, the application
    programmer.
  User: The person twiddling the GUI at runtime.

Known Bugs:

- Too much implementation-defined and undefined behaviour.
- No good way to show/hide/destroy widgets.
- Not very useful for large applications.

MMII Library Summary:


makeApplication(name:string):Application
====
Precondition: name is a non-null string, makeApplication() has not
  been called previously.

Postcondition: the return value is an instance of a class implementing
  the Application interface (below).

On Error: returns null if there is an error creating an application
  instance.  returns the previous application instance if
  makeApplication() has been called previously.
....

interface Application
====
The Application instance manages the main event loop of the program.
It is responsible for zero or more windows, and zero or more idle
tasks.
....

Application.addIdleTask(t:IdleTask)
====
Precondition: t is a non-null instance of IdleTask that has not
  been previously used as an argument to addIdleTask()

Postcondition: At implementation defined periods of time, the
  application instance will issue a call to the work() method of t.
  The relative order of execution of two IdleTasks is undefined.
  The frequency of execution of an IdleTask is undefined.

Errors: Implementation defined result if addIdleTask() is called
  more than once on the same IdleTask instance.  Undefined result
  if addIdleTask() is called with a null argument.
....

Application.removeIdleTask(t:IdleTask)
====
Precondition: t is a non-null instance of IdleTask that has been
  previously used as an argument to addIdleTask()

Postcondition: t will no longer be called during implementation
  defined periods of inactivity.

Errors: Undefined result if t is null.  Undefined result if
  addIdleTask() was not previously called on t.

Note: It is okay to call removeIdleTask(t) from within the work()
  method of t.
....

Application.run()
====
Precondition: The run() method was not previously called on the
  current applicaiton instance.

Postcondition: The application will dispatch messages on behalf of
  its Frames and their children and will execute idle tasks.

Errors: After run() returns, the application has exited and it is an
  error to call any method on any instance of an object from the MMII
  package.
....

Application.requestApplicationExit()
====
Precondition: The run() method of the application has been called,
  but has not yet returned.

Postcondition: After some implemenetation defined, finite, period of
  time, the Application instance will exit (that is, the run() method
  will return).

Errors: Undefined result if requestApplicationExit() is called before
  the run() method has been called, or after it has returned.
....

Application.makeFrame(title:string, width:int, height:int):Frame
====
Precondition: title is a non-null string, width and height are
  non-negative integers

Postcondition: A new window will appear on the screen with the
  requested titlebar string and the given width and height.  The
  window will be visible. The window or its children will not process
  user events unless the run() method has been called but has not yet
  returned. The method returns the Frame object that can be used to
  manipulate the window.

Errors: It is an error to call this method after the run() method has
  returned.
....

interface IdleTask
====
Instances of IdleTask should be implemented by the application
programmer in order to request that the Application perform some
background task(s).
....

IdleTask.work(x:Application)
====
Precondition: The current instance of IdleTask has been previously
  used as an argument to Application.addIdleTask() but has not
  yet been used as an argument to Application.removeIdleTask(), and
  the Application.run() method has been called but has not yet returned.

Postcondition: Implemented by application programmer.

Errors: Application dependent.

Caveat: The work() method should return quickly.  No UI event handling
  can take place until all the work() methods for all idle tasks return.
....

interface Frame
====
A Frame (or window) is a handle to a top-level application window.  It
has a title, and a Composite that represents the main canvas of the
window where child widgets may be installed.  The Frame has an
implementation-defined menu bar that contains some
implementation-defined menus.  A window may be closed.  Note that the
closing of a window is not normally related in any way to exiting
from the application, you should add a FrameListener that calls
Application.requestApplicationExit() in order to have the application
exit if the window is closed.
....

Frame.composite():Composite
====
Precondition: None

Postcondition: Returns the instance of Composite reponsible for the
  children of this frame.

Errors: None
....

Frame.addListener(x:FrameListener)
====
Precondition: x is a non-null instance of FrameListener.

Postcondition: Methods in x will be called by the current frame when
  interesting events happen.

Errors: Implementation defined results if x has already been used as
  an argument to addListener for this instance of Frame.
....

Frame.removeListener(x:FrameListener)
====
Precondition: x has been used as an argument to addListener for this
  Frame instance.

Postcondition: x will no longer have its methods called by this Frame
  when interesting events happen.

Errors: Implementation defined results if x is not a listener for this
  Frame.  Undefined results if removeListener is called from within a
  method of a FrameListener (this is a bug in the current version of
  MMII).
....

interface FrameListener
====
Instances of FrameListner should be implemented by the application
programmer in order to receive and process Frame-related events.
....

FrameListener.onClose(x:Frame):bool
====
Precondition: x is a frame, and this instance of FrameListner has been
  used as an argument to x.addListener(), but not yet as an argument to
  x.removeListner().  The user has indicated that the Frame x should be
  closed

Postcondition: The application programmer should return true from this
  method if it is okay to close this window, or false if it is not.

Errors:  Undefined results if this method calls x.removeListener()
....

NOTE: Dialog is not implemented in this version of MMII.

interface Widget
====
A Widget represents an onscreen element with which the user may possibly
interact.  Widgets are contained in one or more Composite widgets.  A
Composite widget is either the child of another Composite widget, or it
is the Composite associated with a Frame (or Dialog).

Widget.isComposite():bool
====
Precondition: None

Postcondition: returns true if this widget is a Composite widget.
....

Widget.parent():Composite
====
Precondition: None

Postcondition: returns the Composite widget that is the parent of 
  this widget, or null if this widget is the composite associated
  with a Frame.
....

interface Composite extends Widget
====
A Composite widget is a container of other widgets.
....

Composite.addWidget(x:int, y:int, w:int, h:int):WidgetMaker
====
Precondition: w, h are non-negative

Postcondition: Returns an "unfired" instance of WidgetMaker (see below)
  which when fired will create a widget within this composite at
  the given x and y coordinates with the given width and height.
  It is implementation-defined whether the width, height or on-screen
  coordinates are honored or ignored.

On Error: returns null if width or height is negative.
....

Composite.enumerateChildren(c:CompositeVisitor)
====
Precondition: c is a non-null instance of CompositeVisitor

Postcondition: c.visitChild() is called, in some implementation defined
  order, for each Widget that is a child of this Composite.

On Error: Undefined result if c is null.
....

Composite.destroy()
====
Precondition: None

Postcondition: None

Bugs:  This method is currently not implemented
....


interface CompositeVisitor
====
Instances of CompositeVisitor can be written by the application programmer
to traverse the Widget hierarchy.
....

CompositeVisitor.visitChild(c:Composite, x:Widget)
====
Precondition: this CompositeVisitor was used as an argument to
  c.enumerateChildren().  x is a Widget that is a child of c.

Poscondition: Application defined.
....
}

interface WidgetMaker
====
A WidgetMaker is a one-shot class responsible for creating a widget
as a child of a Composite widget.  Each WidgetMaker instance has
associated with it the Composite whose addWidget() method was called
to get this instance of WidgetMaker, as well as the coordinates and
dimensions with which addWidget() was called.

A WidgetMaker is "fired" by calling one of its methods.  Subsequent
firings of a WidgetMaker will fail to create any children and will
indicate this by returning null.  It is generally useless to hold on
to an instance of WidgetMaker past its first firing.  There is no good
reason to call addWidget() without immediately firing the resulting
WidgetMaker.
....

WidgetMaker.composite():Composite
====
Precondition: this WidgetMaker hasn't been fired yet.

Postcondition: a new Composite widget is created, and this WidgetMaker
  is considered to have fired.  The Composite is visible and active.

Errors: if this WidgetMaker has already fired, subsequent firings
return null.
....

WidgetMaker.command(label:string):Command
====
Precondition: this WidgetMaker hasn't been fired yet.

Postcondition: a new Command widget (a pushbutton) is created with the
  given label, and this WidgetMaker is considered to have fired.

Errors: if this WidgetMaker has already fired, subsequent firings
return null.
....

WidgetMaker.multipleChoice():MultipleChoice
====
Precondition: this WidgetMaker hasn't been fired yet.

Postcondition: a new MultipleChoice widget (a drop-down list) is created,
  and this WidgetMaker is considered to have fired.

Errors: if this WidgetMaker has already fired, subsequent firings
return null.
....
    
WidgetMaker.textEntry():TextEntry
====
Precondition: this WidgetMaker hasn't been fired yet.

Postcondition: a new TextEntry widget (a single line edit box) is created,
  and this WidgetMaker is considered to have fired.

Errors: if this WidgetMaker has already fired, subsequent firings
return null.
....

interface Command extends Widget
====
A Command widget represents a pushbutton.  A user may click a pushbutton
to generate events.  A Command widget has a label on it that the user
can see.
....

Command.getLabel():string
====
Precondition: None

Postcondition: returns the text of the current label of this Command widget.

Errors: none
....

Command.setLabel(l:string)
====
Precondition: l is a non-null string

Postcondition: The label of this Command widget is changed to l.

Errors:  Implementation defined result if l is a string.
....

Command.addListener(x:CommandListener)
====
Precondition: x is a non-null instance of CommandListener.

Postcondition: Methods in x will be called by this Command when
  interesting events happen.

Errors: Implementation defined results if x has already been used as
  an argument to addListener for this instance of Command.
....

Command.removeListener(x:CommandListener)
====
Precondition: x has been used as an argument to addListener for this
  Command instance.

Postcondition: x will no longer have its methods called by this Command
  when interesting events happen.

Errors: Implementation defined results if x is not a listener for this
  Command.  Undefined results if removeListener is called from within a
  method of a CommandListener (this is a bug in the current version of
  MMII).
....

interface CommandListener
====
Instances of CommandListner can be implemented by the application programmer
in order to receive a notification when the user clicks the Command button.
....

CommandListner.onClick(x:Command)
====
Precondition: x is a Command, and this instance of CommandListner has been
  used as an argument to x.addListener(), but not yet as an argument to
  x.removeListner().  The user has clicked the button associated with x.

Postcondition: Application-programmer defined.

Errors:  Undefined results if this method calls x.removeListener()
....

interface MultipleChoice extends Widget
====
A MultipleChoice widget allows the user to make a single selection
from a finite set of choices.
....

MultipleChoice.addChoice(label:string, datum:object):int
====
Precondition: label is non-null

Postcondition: Adds a new choice with the given label and associated
  datum to this MultipleChoice widget.  Returns the position of this
  choice within the MultipleChoice widget's list.

Errors: Undefined results if label is null.
....

MultipleChoice.getLabel(pos:int):string
====
Precondition: pos is non-negative and the list contains at least pos+1
  elements.

Postcondition: the return value is the label in position pos.

Errors: Undefined result unless 0 <= pos < [number of list elements]
....

MultipleChoice.getDatum(pos:int):object
====
Precondition: pos is non-negative and the list contains at least pos+1
  elements.

Postcondition: the return value is the datum associated with
  list position pos.

Errors: Undefined result unless 0 <= pos < [number of list elements]
....

MultipleChoice.setDatum(pos:int, datum:object):object
====
Precondition: pos is non-negative and the list contains at least pos+1
  elements.

Postcondition: datum is associated with the list posisition pos and
  the old datum is returned.  Note: return value may be null on success
  if previous datum was null.

Errors: Undefined result unless 0 <= pos < [number of list elements]
....

MultipleChoice.setLabel(pos:int, label:string):string
====
Precondition: pos is non-negative and the list contains at least pos+1
  elements, label is a non-null string.

Postcondition: label is associated with the list posisition pos and
  the old label is returned.

Errors: Undefined result unless 0 <= pos < [number of list elements]
  and label is non-null.
....

MultipleChoice.enumerateChoices(v:MultipleChoiceVisitor)
====
Precondition: v non-null

Postcondition: v.visitChoice() is called once for each choice in this
  MultipleChoice widget.  The order in which choices are visited is
  implementation-defined.

Errors: Undefined result if v is null.
....

MultipleChoice.getSelected():int
====
Precondition: none

Postcondition: The return value is -1 if no choice is currently selected,
  or it is the list position of the currently selected choice.

Errors: None
....

MultipleChoice.setSelected(pos:int):int
====
Preconditions: -1 <= pos < [number of choices]

Postcondition: if pos==-1, then no choice is selected, otherwise the
  choice in position pos is selected.  The position of the previously
  selected choice is returned, or -1 if no choice was previously selected.

Errors: Undefined result if pos is not in range.
....

MultipleChoice.addListener(v:MultipleChoiceListener)
====
Precondition: v non-null.

Postcondition: subsequently until this.removeListener(v) is called,
  v will be notified of changes in the current choice in this
  MultipleChoice wigets.

Note: It is implementation-defined whether Listners will be called
  in notification to programatic changes (due to calls to setSelected())
  changed in selection.

Errors: Undefined result if v is null.
....

MultipleChoice.removeListener(v:MultipleChoiceListener)
====
Precondition: v non-null

Postcondition: v will no longer be notified in the changes to the selected
  choice in this MultipleChoice widget.

Errors:  Undefined result if this method is called from inside v.
  Undefined result if v is null.
....

interface MultipleChoiceVisitor
====
Applications should provide instances of MultipleChoiceVisitor in order
to investigate the choices of a MultipleChoice widget.
....

MultipleChoiceVisitor.visitChoice(m:MultipleChoice, pos:int,
                                  label:string, datum:object)
====
Precondition: m.enumerateChoices() was called with this
  MultipleChoiceVisitor as the argument, m is non-null, pos is in range,
  label is non-null

Poscondition: Application-defined

Errors: it is an error to call m.addChoice() from this method
....

interface MultipleChoiceListener
====
Applications should provide instances of MultipleChoiceListener to be
notified of changes in the currently selected choice in a MultipleChoice
widget.
....

MultipleChoiceListener.onChange(x:MultipleChoice, pos:int)
====
Precondition: x is non-null, and previously x.addListner(this) has been
  called, but x.removeListner(this) has not yet been.  pos is in range for
  x.  The user has changed the currently selected choice in x.

Postcondition: Application defined.

Errors: Undefined results from calls to x.removeListener().
....

interface TextEntry extends Widget
====
A TextEntry is a single-line edit control into which the user may
type text, or the application may output text to.
....

TextEntry.getText():string
====
Precondition: none

Postcondition: Returns the text in this TextEntry Widget
....

TextEntry.setText(s:string)
====
Precondition: s != null

Postcondition: The text in this TextEntry Widget is changed to s.

Errors: Undefined result if s is null.
....