Crispin Cowan wrote: >> The above is the art of programming language design. Programs written in high-level languages are *precisely* specifications that result in the system generating the program, thereby saving time and eliminating coding error. You will find exactly those arguments in the preface to the K&R C book. <<
Whilst I agree that the distinction between specification and programming languages is not completely clear cut, there is nevertheless a fundamental difference between specification and programming. In a programming language, you tell the computer what you want it to do, normally by way of sequential statements and loops. You do not tell the computer what you are trying to achieve. Indeed, current programming languages provide hardly any means of expressing what you want to achieve; typically, the only concession they make in this direction is an "assert" statement, which lacks the expressivity needed (e.g. you can't easily use an assert statement to say that an array contains the same objects that it did on entry to the current function, but they are now arranged in ascending order). In a specification language, you tell the computer what you are trying to achieve, not how to achieve it. This is typically done by expressing the desired relationship between the input state and the output state. The state itself is normally modelled at a higher level of abstraction than in programming (e.g. you wouldn't refer to a hash table, because that is implementation detail; you would refer to a set or mapping instead). The distinction becomes somewhat blurred when you assemble a program from library classes, because you are relying on those classes to represent some data without worrying about how they represent it, and calling their methods to achieve some state changes without worrying about the steps they go through to achieve it. Unfortunately, in the absence of precise specifications for those classes, it sometimes happens that what is achieved by calling a method is not quite what you wanted; or you may sometimes fail to meet the preconditions of the method, resulting in a crash or exception. My belief is that a software development language should be capable of expressing both specification and programming. Most of the time, its users will write the specifications and let a tool refine them to a program. Where a higher degree of optimization is needed, the software developer can manually refine parts of the specification to a program. It is not difficult to extend such a language to be capable of expressing expected behaviour as well. This paves the way for tools that attempt to prove that the specification exhibits the expected behaviour (and that any manual refinements are correct implementations of the corresponding specification). In case anyone is wondering what this has to do with security, "expected behaviour" includes things like "array indices are always in bounds" (i.e. no buffer overflows no matter what input is provided), and "the browser address bar always shows the full URL of the current page". David Crocker Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
