Edit detail for Design By Contract revision 1 of 1

changed:
-
Software and especially hardware frequently is treated as "given".  More precisely,
hardware and software has properties and users depend on its properties.  Some properties
are documented, some other are discovered by experimentation or by reasoning.
Once some property is known users tend to depend on it.  This point of view has
some merits.  However, it causes troubles in longer time.  Namely, hardware and
software tend to evolve.  New hardware my execute correctly most programs for
the old machine, but some obscure properties may differ and programs depending
on changed behaviour may fail on new machine.  Similar problem appears when
replacing operation system or libraries.   To resolve problem there is concept
of specification.  There should be desription (documentation) what various parts
of system should do and what they expect (need) to function correctly.  In
principle any part could be replaced by different part with the same specification.

This is frequently explained as a contract: hardware offers service of executing programs,
promising to deliver specified results, but only when program behaves well (avoids
undefined instructions, etc).  Similarly, program or library routine promises to
deliver correct result, but only when data satisfies initial conditions.  Correct
result is not always unique: routine promising to deliver one of solutions of an
equation may deliver arbitrary one when there are multiple solutions.  Formally this
may be described by a Hoare triple: in initial condition satisfying predicate P
routine S promises to deliver result satisfying condition Q.

Design by contract makes specification central part of design process.  Design
starts from building requested specification.  Initial specification is factored
and transformed, so that task is divided into simpler parts up to stage when
subtasks can be done by existing routines or subtask is simple enough to code
directly.  Design by contract can be done at various levels of formality.  At
one end there may be set of tools that store design documents, each step is verified
either by special checker routines or by human reviewers.  There may be process
of approvals and "sign on".  Less formal process is also a possibility.  At
informal end it is possible to have no formal documents, but still use design
by contract as a guide.

FriCAS design is based on design by contract.  Design process is rather informal.
But since FriCAS deals with mathematics there are precise definitions of subject
domain.  Of course, in practice there is some fuzz and variation in definitions.
For example some authors define rings to have unit with respect to multiplication,
some other do not require this.  FriCAS must provide specific definition
(in case above FriCAS have Ring which assumes unit and Rng where unit is not
required).  Nevertheless, remaining rather informal FriCAS routines have
rather precise specification.  Of course, there are bugs, and specification
bugs need fixing like other bugs.  And there is room for improvement for
things which are not bugs but could be better/clearer.   On the other hand
some specification are loose by design: the intent of loose specifications
is to allow wider applicability (in particular more implementations)

As an example how design by contract differs from more traditional design
consider modifying some function F and checking if change is acceptable.  Traditional
approach would search for uses of F and analyse impact of change on each user.
Design by contract looks if changed F stil satisfies old specification.
The practical difference is that design by contract may accept change to F that
breaks some user and fix users that depended on properties outside of contract.
Opposite is possible too: design by contract my reject change because it
breaks contract, even if all existing users work with change (depend on
weaker contract).