4

This question is more theoretical than practical. Imagine we have an intelligent machine that if is fed with a fully complete specification of an object then that machine will produce exactly that object, and not anything else.

Now, can we ever achieve a fully complete specification of anything?

If you want a more practical question: is the official "Java Language Specification" complete? Or in other word: is there a piece of Java code that complies to the JLS, but is not accepted by the compiler corresponding to that JLS?

CuongHuyTo
  • 149
  • 4
  • 6
    Yes. The full specification is the program itself. – JacquesB Apr 06 '16 at 05:46
  • @JacquesB: to my understanding, a spec is something separated from the implementation. – Doc Brown Apr 06 '16 at 05:49
  • 7
    @DocBrown: Yeah a specification is much higher level, but if the specification should be detailed enough that the exact program could be automatically generated, then it would have to contain the same information as the program. – JacquesB Apr 06 '16 at 05:53
  • @JacquesB and DocBrown: I agree with both of you. That "complete spec" must convey the same information as the "object" or "program" that it specifies. What I really want to ask is: can there exist two spaces (one space for all specifications and one space for all programs) that have a 1-to-1 mapping between them (i.e. one element of spec space corresponds to only one element of the program space, and vice versa) ??? – CuongHuyTo Apr 06 '16 at 08:21
  • 4
    @CuongHuyTo: if you make that, then what you have made is called a higher level programming language and the process to turn it into the lower level language is called compilation. – RemcoGerlich Apr 06 '16 at 08:43
  • Take Coq. It is a proof assistant where you can define types, functions etc and prove theorems. It also allows to extract programs from the specification. – Bakuriu Apr 06 '16 at 09:17
  • @CuongHuyTo: that would be pretty useless. The whole point of a formal specification is to *separate* it from the implementation. Something like a JLS is for allowing **different implementations** of compilers which all conform to the same spec. And if those compilers are bug free, they will all accept the same piece of code as correct (or not correct). – Doc Brown Apr 06 '16 at 10:55
  • @Doc Brown: when a space A is separate from a space B, then requiring a 1-to-1 mapping between A and B is NOT useless. It seems that the answer by Basile Starynkevitch does go on the direction that I am asking. – CuongHuyTo Apr 06 '16 at 12:45
  • 1
    @CuongHuyTo: honestly, I think your question is very unclear. What is the "object" you have in mind to be produced by that "hypothetical machine", when you stick to the JLS example? A Java compiler (piece of software), or the abstract thing "Java programming language" (which can be seen as a mathematical, infinite set of finite character strings)? And do you talk about "software specifications" or "language specifications" (these are very different things)? – Doc Brown Apr 06 '16 at 14:08

4 Answers4

8

Yes, it is possible. Mathematics and formal logic allows you to define computations that have exactly the properties you want and nothing else. And then the same logic allows you to prove that it is so.

The problem is that it requires huge amount of effort to do so. Even writing a simple for loop might take days to validate. This is why this approach is rarely used and even if it is used, it is only applied to critical parts of the system.

Euphoric
  • 36,735
  • 6
  • 78
  • 110
  • 4
    Did you also consider [Gödel's incompleteness theorems](https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems)? This might give theoretical limits because some things cannot be validated. – Sjoerd222888 Apr 06 '16 at 09:43
  • You are talking about proving that a piece of software conforms to a given specification - and yes, that is possible in theory, with a huge amount of effort, as you wrote, of course. But that is **not what the OP asked for** (maybe it is what he meant, but I don't think so). He asked if a spec can be made that leads always to the same program (which does IMHO not make much sense). – Doc Brown Apr 06 '16 at 10:59
  • 4
    @Sjoerd222888 - Godel's incompleteness theorems (if applicable) would most likely say that you can't completely specify *everything*. (Not *anything*.) – Stephen C Apr 06 '16 at 11:11
  • @StephenC and Sjoerd222888: thanks for your pointing me to Godel's incompleteness theorems, I'll read more on that. – CuongHuyTo Apr 06 '16 at 12:46
  • @StephenC: You cannot specify everything implies that you could pick a problem that cannot be specified. Therefore you cannot completely specify just any problem. Only some. That was the point I wanted to make. – Sjoerd222888 Apr 06 '16 at 13:10
7

Recall that a programming language is a specification, usually written in English -with the ambiguity of natural language- in some technical report. A programming language is not the same as its implementation in some compiler or interpreter software.

A programming language (specification) is not only or mostly about syntax (which might be formalized with EBNF), but more about semantics. The semantics can be somehow formalized, e.g. with denotational semantics.

I cannot reasonably expect from my C compiler to accept all syntactically or semantically valid programs. I'm sure no compiler & computer could process a C file containing some function with a billion of C statements, deeply nested and combined in a weird control graph. Actually, I do enable optimizations by compiling with gcc -O2, and I empirically observed that compilation time is proportional to the square of the length of the longest function. Hence, when I generate C code -I love metaprogramming-, I need to be careful to avoid generating C functions with more than a dozen of thousands of statements. AFAIK the standard or my compiler documentation is not stating that limitation.

Sadly, the JLS does not even try to partly formalize some of the semantics of the language.

Some programming languages have some partial formalizations of their semantics. A good example of that is the R5RS for Scheme, it has partly formalized some of the semantical aspects of Scheme (but leaving some well deserved freedom to implementors, like order of evaluation of arguments in function call, is challenging to formalize).

But programming languages have also some pragmatics. Read Scott's book on programming language pragmatics, it is enlightning.

A good example of pragmatics is the malloc standard function of C11. Its n1570 (draft) standard says (in §7.22.3, notably §7.22.3.5):

If the space cannot be allocated, a null pointer is returned.

...

void *malloc(size_t size);

...

The malloc function allocates space for an object whose size is specified by size and whose value is indeterminate.

...

The malloc function returns either a null pointer or a pointer to the allocated space.

...

My understanding of the C11 standard is that the following function is a valid implementation of malloc (conforming to the letter of the C11 standard, and probably some POSIX one).

 void* malloc(size_t sz) { errno = ENOMEM; return NULL; }

(of course that implementation is against the spirit of C; I claim that it follows the letter of the standard)

but no sane C developer is expecting such an implementation. A C programmer is expecting malloc to usually succeed. What that precisely means is unclear.

Now, can we ever achieve a fully complete specification of anything ?

I believe that no. A real computer is different of the abstraction we are programming. Take my Linux laptop for example. If I drop it from my desk, if it battery explodes, or if someone fires a gun bullet into it, it is not behaving as the abstraction I am programming. And a fully complete specification would require a complete description of the environment (that is, the physical universe we are in), which is not possible.

Some quantum scientists claim that the universe has a finite but very huge number of states. If that is "true", no complete description of it can exist in a subpart, e.g. on Earth.

Computer programming is always about abstractions. Read also about undefined behavior (in particular C.Lattner's blog entries about it) and about unspecified behavior. Notice that the C standard is purposely (and for good reasons) mentioning in many places undefined behavior. Try hard to avoid it.

Basile Starynkevitch
  • 32,434
  • 6
  • 84
  • 125
3

These are two very different questions in one.

You surely can give a complete spec for piece of software (I guess that is what you really mean, not "anything") which then could be build automatically, if the requirements are simple enough. For example, you can surely specify a function with no parameters which always return 0 in a formal, machine readable manner. That, however, does not mean the generated function implementation will be unique. For example, there are trillions of ways to implement a function which always returns 0.

Your second question is quite different. If a compiler does not accept a specific piece of Java code, maybe the compiler has a bug, or the spec, but that does not mean it cannot be fixed, at least in principle. But even if you have two 100% bug-free compilers (pure hypothetical!), both conforming to the spec, that does not mean those are identically implemented.

Doc Brown
  • 199,015
  • 33
  • 367
  • 565
  • The 2nd part, or the "more practical" part of my question was to address of there is a bug in the JLS, and can we ever make JLS bug-free ? On the other hand, I know that the compiler always has bugs. – CuongHuyTo Apr 06 '16 at 08:56
0

When a software is developed, by the creator himself, who knows what his software should do, then the specification is complete. Java language was developed by the developer by framing specifications that looked complete to the developer being sure that compiler will support the design. But, once Java became a common man's language, he expected it to do lot more.

For example, consider java arrays. Array is a wonderful creation by the creator. But, I guess he never imagined his creation of arrays will be so huge that it could grow upto 2^31-1 elements which compiler will reject. JLS specifies this as a limitation.

Complete spec is possible for something hypothetical or Ideal. In real time there cannot be anything that can be specified completely.

For more limitations by JLS, please refer the link below :
https://en.wikipedia.org/wiki/Criticism_of_Java