Automatically Proving the Correctness of Translations Involving Optimized Code

accumulator ACFIELD(ARGS algorithm ARGS arguments assembly language atom axiom CALL 2 E canonical form CAR and CDR CAR CDR CDR CDR(L cell Chapter CMPLISP compiler COMPUTATION NUMBERS APPEARING CONS CAR contents corresponding data pointer denote detected effective address EQ CDR equivalence error example FEXPR function body given in Figure HIER1 HIERI HIERIA LX001 HLRZ HRRZ implementation inner loop instruction JRST O HIER1A jump to TAG1 JUMPN LABEL HIERI HIERIA LAMBDA LAP NEXT SUBR LAP program left half LISP functions LISP pointers List Structure LOADSTORE loop shortcutting MATCH THE COMPUTATION MEMG modification MOVEI 2 QUOTE NEXTINSTRUCTION NIL load register occur optimizations parameters performed POPJ predicate PROG PROGRAM COUNTER proof procedure property list PUSH 12 QUOTE LEFT& QUOTE PRIGHT& recursive call rederivation process rederived form redundant result right half RPLACA s-expression SETQ SPECIAL variables stack compute stack pointer symbolic execution TAG4 TAGB UNCONDITIONALSKIP XCONS