CALENDAR@IBM.COM (IBM Almaden Research Center Calendar) (03/19/87)
IBM Almaden Research Center
650 Harry Road
San Jose, CA 95120-6099
EFFIGY: SYMBOLIC EXECUTION OF PROGRAMS
J. C. King, IBM Almaden Research Center
Computer Science Coll. Thurs., March 26 3:00 P.M. Room: Front Aud.
Long ago and far away, a group in IBM Yorktown Heights devised a
computer system called "EFFIGY" which executed computer programs
"symbolically." On a recent archeological dig in musty old CMS files,
I stumbled upon what appeared to be a genuine EFFIGY MODULE. After a
time, with a new FILEDEF and a long forgotten LINK, I was able to
execute the model, just as the ancients did. It was amazing for me to
remember how advanced civilization was, even then (12-15 years ago).
For some reason, the art of symbolic execution never caught on in a
big way, and it has nearly been lost. For those of the younger
generation, who have never seen the chanting and chest beating of the
symbolic executors (sexers for short), I will try to recreate some of
that ancient spirit. Especially with the new projection system in the
Front Auditorium, which is capable of showing computer terminal output
on-line, I can demonstrate this EFFIGY system, as it was only possible
to do before in a one-on-one situation in a Yorktown cave. The sexers
had discovered that the same leverage obtained by using algebra to
understand and prove things about arithmetic can be applied to
computer programs. If one executes a program using mathematical
symbols, instead of numbers, as program inputs, the same algebraic
leverage can be obtained. Of course, the dynamic aspects of program
execution makes this process tantalizingly non trivial. Combining the
well-known concepts of program execution and algebra, the notions of
"proving the correctness of programs" and "inductive assertions" can
be easily understood without knowingly resorting to heavy mathematical
concepts.
Host: R. Williams
(Refreshments at 2:45 P.M.)