Hello, I am investigating how a syntactic evolution of language affects its semantics. For instance, java's for loop syntax evolved in its version 5 to a compact one. Do the designers have to prove that even with this syntax the semantics are still preserved! May be this is a trivial example.
So, in general, how can one prove that a language's semantics are still preserved even when its syntax has evolved from very verbose to compact?
Many thanks in advance for any insights/links.
Ketan
Prove that every syntax extension would have been illegal in older versions of the language.
For obvious reasons, new syntactical elements should introduced in a way that would have been syntactically illegal in the older version of the language. Because of that, most languages have a list of reserved words that goes beyond the keywords already in use.
For example, when C# introduced the var keyword in version 3.0, it's potentially problematic since var was not a reserved word in version 1.0 of C# (possibly not in 2.0, either). So a program could have legaly created a type called var in C# 1.0, but it no longer compiles in C# 3.0 and later.
Unchanged semantic of the old language elements is more a matter of how the compiler is built, since the specification rarely changes. If it changes, well, then the semantics are not preserved. The exception is when new specifications that fix things that would have constituted undefined behaviour (but are still legal) in previous versions of the specification. C comes to my mind.
Okay, your last comment is much more answerable.
Some more specific details: we have an interpreter that understands language A in a very verbose syntax. Now, we invented a new language B with a very compact syntax that is a complete departure from that of A. So, a user can now write the code in compact language B, translate to the verbose language A using a translator program that I have written. The problem is how to prove/guarantee that all possible such translations will preserve the semantics of the original language A that the interpreter understands.
The short answer is: You don't. For one thing, when you add syntactic sugar you usually just capture a well-known, wide-used pattern and give it special, nicer syntax - you don't replace large parts of the language's syntax. For such small replacements, the translation can be formulated with informative descriptions and examples - for example, PEP 343 defines the "with" statement relatively informatively.
Now, when the change in syntax is so radical the new language has hardly anything in common with the backend language, we're not talking about change of syntax - we're talking about a compiler. But compilers aren't proven correct either. Well, some people actually try it. But for real-world compilers, correctness is proven by testing, i.e. by the countless users of and programs in the language. Well, sometimes they prove incorrectness... but those are fixed and we're back in the business ;) And of course all serious language implementations have a wide range of test cases (read: example programs, from basic to absurd) that should run (and pass) at least in official releases. When they do (and the test suite is worth its salt), you still don't know that there are no bugs, but if a test fails, you know there's at least one. DIjkstra said: "Testing shows the presence, not the absence of bugs."