Peter Amey wrote:
Yes, the posit and verify approach. We adopted this because we think there
are problems with refining specs into code. One problem is that there can be
(usually will be) more than one valid way of implementing a spec. For example,
the spec may make the abstract assertion that a list is ordered. The
implementation could build an ordered tree structure, write to a buffer that is
periodically quicksorted or even write to a set of temporary files that are
periodically merge sorted. The design choice may depend on non-functional
requirements such as performance or amount of free memory. Therefore we don't
see how you can always generate the most appropriate code for the property
ordered.
You seem to be assuming that there is only one appropriate solution to the
problem and the system cannot be trusted to find it. In reality, there are often
many appropriate solutions and it matters little which one is chosen. In the
example you give, either of the first two solutions would likely be acceptable,
and I think it would be perverse for a code generator to choose the third (i.e.
an external sort on internally-stored data). But I'm not proposing that you
should have to accept whatever the code generator comes up with: if you don't
like the result, the language should provide a way of expressing (in outline at
least) how you want the ordered property to be achieved.
One solution to this is to use very low-levels of specification that avoid the
gap between the abstract concept ordered and the code itself. This can easily
fall into the trap that the specification language simply becomes code (a
problem with B for example).
You seem to be missing the point that B allows you to specify one abstract
machine that talks about a sequence being ordered and then refine it to
another that talks about sorting a list. B does indeed allow you to write
code-like executable specifications; but it also allows you to write
higher-level abstract specifications. I agree that there may be a temptation for
developers to just write the executable version. This is why in PD we have a
semantic distinction between specification and implementation, and you can't
write an implementation without having a specification to attach it to.
David Crocker, Escher Technologies Ltd.
Consultancy, contracting and tools for dependable software development
www.eschertech.com
