x : = y
In such cases of assignment of variables, Pascal compilers first check whether the two variables are of the same type, to avoid equating apples with oranges. Gurevich happened to run his program through two different compilers. The first had no problem with the assignment. The second compiler, though, would not accept the x : = y assignment because it read the variables as being of two different types. Even though the type definitions Gurevich had given for the variables were letter-for-letter the same, the second compiler expected that if two variables were of identical type, that type would be defined in this fashion:
VAR x, y : RECORD
a: INTEGER;
b: REAL;
END;
In short, the two compilers used two different standards of appropriate Pascal syntax. Unsure of why this would be, Gurevich went searching for a definitive standard for the computer language. "I began to wonder what Pascal is," he says. What he discovered is that there is no single Pascal, but many Pascals: there is no binding definition of the language.
"It turns out the semantics - the meaning - of Pascal, or any other programming language, is not well defined," according to Gurevich. "In fact it's defined by a compiler." And it is defined based largely on syntax - the patterns or order of the commands - rather than by content - the logic of what the commands state. To base the semantics on the logic of the content would make for either a too demanding literalness requiring letter-for-letter equivalence among logical equivalents, or a slipperiness in meaning that it would be nearly impossible to put boundaries on.
Gurevich makes the contrast between the strict needs of a programming language and the more forgiving strictures of natural language. "In natural language," he points out, "you say something and some people can interpret it a little differently. Without this we would not have jokes. But when you start to compile, you'd better not be in the mood to make jokes."
Gurevich wanted "precise, mathematical definitions" of programming languages, so he researched the literature on the semantics of programming languages and found two primary approaches to it. First was the engineering approach, which was not mathematically precise but provided for robust explanation. Second were the precise mathematical approaches. Most prominent among these was - and still is - denotational semantics, which translated every element into a mathematical formulation. But these latter approaches tended to become so complex that they could deal only with fragments of languages, or with narrowly bounded "toy examples."
The problem, as Gurevich came to see it, was that the actual machine that performed the execution was itself generally functioning on a much lower level of abstraction: the Pascal compilers he had been dealing with, for example, spoke in bytes. Gurevich's question: "Does there exist an abstract mathematical machine which can be used to interpret programming languages and other computer systems on their natural abstraction levels?"
Gurevich the logician approached an answer. In logic there is the notion of a structure, a mathematical organization composed of domains, functions, and relations - a simple notion but one that can be employed to describe all static situations one might encounter. A graph, for example, can be described as "a domain of vertices with a binary adjacency relation."
Gurevich's idea was to create a machine whose states are such structures, that works at the same level of abstraction, and that is very faithful to the original algorithm. People had thought of such an approach in different settings, but they had not pursued it to any great extent. The main problem as Gurevich saw it was the question of whether such an approach could be tailored to dynamic situations-true computational situations-as readily as it had been to static situations. He has come to believe that it can be.
Each structure has a vocabulary. If the vocabulary is right, a program in a simple fixed language can describe the dynamics of any computer system at the natural abstraction level. "In other words," says Gurevich, "we have a systematic way to construct mathematical models of arbitrary computer systems."
This leads to a central tenet of ASMs: any computer system, if looked at correctly, is an abstract state machine of the kind mentioned above.
Suppose you have an architecture or a programming language or a protocol, and you want to prove something about it. Ideally, you would want a real mathematical proof. Soon after Intel introduced its Pentium processor, for example, a flaw was found in it that could introduce computational errors during use. Ideally, Intel would have wanted mathematical proof that their design was flawless. But mathematical proofs can be created only for mathematical objects, and a program by itself is not a mathematical object because its meaning is not completely clear.
"So before you prove anything about a program or protocol or whatever it is, you would like to convert it into a mathematical object, and that's what we do," says Gurevich. "Our ambition is this: give us any computer system, we will create a mathematical model which will be very close to the system, the description will be more or less the same size, and a normal engineering education will suffice to understand the model." Stated more formally: every algorithm can be simulated on its natural abstraction level by an appropriate ASM in strict lock-step, so that the ASM needs only one step to simulate a step of the algorithm.
Algorithms tend not to be initially conceived of within the parameters, syntax, and semantics of a specific programming language. They tend to be much more abstract. They may use data structures the programming language itself does not have, for example. "So when you try to code your ideas into the language," says Gurevich, "you have to adapt to the language, and there is a lot of overhead. So in the program you see trees but not the forest. . . . We wanted to create an abstract state machine for the algorithm itself, and try to prove something about the algorithm on its own abstraction level."
Once an ASM has been created that represents the original algorithm at the same high level of abstraction, a programmer or mathematician can create another ASM at the lower abstraction level of the program. Once the two ASMs exist, he or she can prove that the lower one faithfully implements the upper one. In practice, a whole series or hierarchy of ASMs is often created to get from upper levels of algorithmic abstraction to lower levels of coding abstraction. This approach to the stepwise refining of ASMs leads to executable code that is well documented and that can be readily inspected by mathematical means.
"The idea is not to be a slave to the programming language," Gurevich says, "but to go directly to where things happen, and deal with them there."
And where things happen is where the growing ASM community has been. In a decade of work they have amassed a convincing group of complex real-life case studies, ranging from semantics and implementation of full fledged programming languages - including C++, Prolog, and Java - to specification and verification of protocols and hardware designs.
The need for developing computer systems that lend themselves to mathematical inspection will only grow as the global electronic village shrinks. "Imagine you write a program, and you want this program to be used all over the world," Gurevich says. "Some compilers interpret it correctly and some incorrectly. And then people complain, and you say 'On my compiler it was correct.'" The growing attention to Gurevich abstract state machines may help programmers avoid such frustrations in the future.
Reach the University of Michigan Abstract State Machines Web site at http://www.eecs.umich.edu/gasm/. A quote from a paper linked there: "We hope the reader will benefit from the ASM papers appearing here and will be tempted to try the method for his next challenging application problem."
[an error occurred while processing this directive]