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
