Contributions to Mechanical Proofs of Correctness for Compiler Front-Ends

Dissertation

PL0R: LR(0) Items

(R-LOOP)
* (setq fis (LR-0-items grammar))
  (LIST (MK-PROD 0 '(PROG) '(DOT BLK))
	(MK-PROD 0 '(PROG) '(BLK DOT))
	(MK-PROD 1 '(BLK) '(DOT DECL COLON SI BLK))
	(MK-PROD 1 '(BLK) '(DECL DOT COLON SI BLK))
	(MK-PROD 1 '(BLK) '(DECL COLON DOT SI BLK))
	(MK-PROD 1 '(BLK) '(DECL COLON SI DOT BLK))
	(MK-PROD 1 '(BLK) '(DECL COLON SI BLK DOT))
	(MK-PROD 2 '(BLK) '(DOT PROC))
	(MK-PROD 2 '(BLK) '(PROC DOT))
	(MK-PROD 3 '(DECL) '(DOT INT IDENT))
	(MK-PROD 3 '(DECL) '(INT DOT IDENT))
	(MK-PROD 3 '(DECL) '(INT IDENT DOT))
	(MK-PROD 4 '(DECL) '(DOT LB INTEGER RB INT IDENT))
	(MK-PROD 4 '(DECL) '(LB DOT INTEGER RB INT IDENT))
	(MK-PROD 4 '(DECL) '(LB INTEGER DOT RB INT IDENT))
	(MK-PROD 4 '(DECL) '(LB INTEGER RB DOT INT IDENT))
	(MK-PROD 4 '(DECL) '(LB INTEGER RB INT DOT IDENT))
	(MK-PROD 4 '(DECL) '(LB INTEGER RB INT IDENT DOT))
	(MK-PROD 5 '(PDECL) '(DOT PROCKW IDENT LP RP NI SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW DOT IDENT LP RP NI SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT DOT LP RP NI SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP DOT RP NI SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP RP DOT NI SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP RP NI DOT SPROC BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP RP NI SPROC DOT BI COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP RP NI SPROC BI DOT COLON))
	(MK-PROD 5 '(PDECL) '(PROCKW IDENT LP RP NI SPROC BI COLON DOT))
	(MK-PROD 6 '(PDECLLIST) '(DOT PDECL SI PDECLREST))
	(MK-PROD 6 '(PDECLLIST) '(PDECL DOT SI PDECLREST))
	(MK-PROD 6 '(PDECLLIST) '(PDECL SI DOT PDECLREST))
	(MK-PROD 6 '(PDECLLIST) '(PDECL SI PDECLREST DOT))
	(MK-PROD 7 '(PDECLLIST) '(DOT PDECL))
	(MK-PROD 7 '(PDECLLIST) '(PDECL DOT))
	(MK-PROD 8 '(PDECLLIST) '(DOT))
	(MK-PROD 9 '(PDECLREST) '(DOT PDECL))
	(MK-PROD 9 '(PDECLREST) '(PDECL DOT))
	(MK-PROD 10 '(PDECLREST) '(DOT PDECL SI PDECLREST))
	(MK-PROD 10 '(PDECLREST) '(PDECL DOT SI PDECLREST))
	(MK-PROD 10 '(PDECLREST) '(PDECL SI DOT PDECLREST))
	(MK-PROD 10 '(PDECLREST) '(PDECL SI PDECLREST DOT))
	(MK-PROD 11 '(PROC) '(DOT REC NI PDECLLIST BI COLON SI PROC))
	(MK-PROD 11 '(PROC) '(REC DOT NI PDECLLIST BI COLON SI PROC))
	(MK-PROD 11 '(PROC) '(REC NI DOT PDECLLIST BI COLON SI PROC))
	(MK-PROD 11 '(PROC) '(REC NI PDECLLIST DOT BI COLON SI PROC))
	(MK-PROD 11 '(PROC) '(REC NI PDECLLIST BI DOT COLON SI PROC))
	(MK-PROD 11 '(PROC) '(REC NI PDECLLIST BI COLON DOT SI PROC))
	(MK-PROD 11 '(PROC) '(REC NI PDECLLIST BI COLON SI DOT PROC))
	(MK-PROD 11 '(PROC) '(REC NI PDECLLIST BI COLON SI PROC DOT))
	(MK-PROD 12 '(PROC) '(DOT SPROC))
	(MK-PROD 12 '(PROC) '(SPROC DOT))
	(MK-PROD 13 '(SPROC) '(DOT SKIP))
	(MK-PROD 13 '(SPROC) '(SKIP DOT))
	(MK-PROD 14 '(SPROC) '(DOT STOP))
	(MK-PROD 14 '(SPROC) '(STOP DOT))
	(MK-PROD 15 '(SPROC) '(DOT VAR COLONEQ EXP))
	(MK-PROD 15 '(SPROC) '(VAR DOT COLONEQ EXP))
	(MK-PROD 15 '(SPROC) '(VAR COLONEQ DOT EXP))
	(MK-PROD 15 '(SPROC) '(VAR COLONEQ EXP DOT))
	(MK-PROD 16 '(SPROC) '(DOT INPUT QUEST IDENT))
	(MK-PROD 16 '(SPROC) '(INPUT DOT QUEST IDENT))
	(MK-PROD 16 '(SPROC) '(INPUT QUEST DOT IDENT))
	(MK-PROD 16 '(SPROC) '(INPUT QUEST IDENT DOT))
	(MK-PROD 17 '(SPROC) '(DOT OUTPUT EXCLAIM EXP))
	(MK-PROD 17 '(SPROC) '(OUTPUT DOT EXCLAIM EXP))
	(MK-PROD 17 '(SPROC) '(OUTPUT EXCLAIM DOT EXP))
	(MK-PROD 17 '(SPROC) '(OUTPUT EXCLAIM EXP DOT))
	(MK-PROD 18 '(SPROC) '(DOT CALL IDENT LP RP))
	(MK-PROD 18 '(SPROC) '(CALL DOT IDENT LP RP))
	(MK-PROD 18 '(SPROC) '(CALL IDENT DOT LP RP))
	(MK-PROD 18 '(SPROC) '(CALL IDENT LP DOT RP))
	(MK-PROD 18 '(SPROC) '(CALL IDENT LP RP DOT))
	(MK-PROD 19 '(SPROC) '(DOT SEQ NI SPROCLIST BI))
	(MK-PROD 19 '(SPROC) '(SEQ DOT NI SPROCLIST BI))
	(MK-PROD 19 '(SPROC) '(SEQ NI DOT SPROCLIST BI))
	(MK-PROD 19 '(SPROC) '(SEQ NI SPROCLIST DOT BI))
	(MK-PROD 19 '(SPROC) '(SEQ NI SPROCLIST BI DOT))
	(MK-PROD 20 '(SPROC) '(DOT IF NI GCLIST BI))
	(MK-PROD 20 '(SPROC) '(IF DOT NI GCLIST BI))
	(MK-PROD 20 '(SPROC) '(IF NI DOT GCLIST BI))
	(MK-PROD 20 '(SPROC) '(IF NI GCLIST DOT BI))
	(MK-PROD 20 '(SPROC) '(IF NI GCLIST BI DOT))
	(MK-PROD 21 '(SPROC) '(DOT WHILE EXP NI SPROC BI))
	(MK-PROD 21 '(SPROC) '(WHILE DOT EXP NI SPROC BI))
	(MK-PROD 21 '(SPROC) '(WHILE EXP DOT NI SPROC BI))
	(MK-PROD 21 '(SPROC) '(WHILE EXP NI DOT SPROC BI))
	(MK-PROD 21 '(SPROC) '(WHILE EXP NI SPROC DOT BI))
	(MK-PROD 21 '(SPROC) '(WHILE EXP NI SPROC BI DOT))
	(MK-PROD 22 '(SPROCLIST) '(DOT SPROC SI SPROCREST))
	(MK-PROD 22 '(SPROCLIST) '(SPROC DOT SI SPROCREST))
	(MK-PROD 22 '(SPROCLIST) '(SPROC SI DOT SPROCREST))
	(MK-PROD 22 '(SPROCLIST) '(SPROC SI SPROCREST DOT))
	(MK-PROD 23 '(SPROCLIST) '(DOT SPROC))
	(MK-PROD 23 '(SPROCLIST) '(SPROC DOT))
	(MK-PROD 24 '(SPROCLIST) '(DOT))
	(MK-PROD 25 '(SPROCREST) '(DOT SPROC))
	(MK-PROD 25 '(SPROCREST) '(SPROC DOT))
	(MK-PROD 26 '(SPROCREST) '(DOT SPROC SI SPROCREST))
	(MK-PROD 26 '(SPROCREST) '(SPROC DOT SI SPROCREST))
	(MK-PROD 26 '(SPROCREST) '(SPROC SI DOT SPROCREST))
	(MK-PROD 26 '(SPROCREST) '(SPROC SI SPROCREST DOT))
	(MK-PROD 27 '(GCLIST) '(DOT GC SI GCREST))
	(MK-PROD 27 '(GCLIST) '(GC DOT SI GCREST))
	(MK-PROD 27 '(GCLIST) '(GC SI DOT GCREST))
	(MK-PROD 27 '(GCLIST) '(GC SI GCREST DOT))
	(MK-PROD 28 '(GCLIST) '(DOT GC))
	(MK-PROD 28 '(GCLIST) '(GC DOT))
	(MK-PROD 29 '(GCLIST) '(DOT))
	(MK-PROD 30 '(GCREST) '(DOT GC SI GCREST))
	(MK-PROD 30 '(GCREST) '(GC DOT SI GCREST))
	(MK-PROD 30 '(GCREST) '(GC SI DOT GCREST))
	(MK-PROD 30 '(GCREST) '(GC SI GCREST DOT))
	(MK-PROD 31 '(GCREST) '(DOT GC))
	(MK-PROD 31 '(GCREST) '(GC DOT))
	(MK-PROD 32 '(GC) '(DOT EXP NI SPROC BI))
	(MK-PROD 32 '(GC) '(EXP DOT NI SPROC BI))
	(MK-PROD 32 '(GC) '(EXP NI DOT SPROC BI))
	(MK-PROD 32 '(GC) '(EXP NI SPROC DOT BI))
	(MK-PROD 32 '(GC) '(EXP NI SPROC BI DOT))
	(MK-PROD 33 '(EXP) '(DOT SIMPLE))
	(MK-PROD 33 '(EXP) '(SIMPLE DOT))
	(MK-PROD 34 '(EXP) '(DOT MOP SIMPLE))
	(MK-PROD 34 '(EXP) '(MOP DOT SIMPLE))
	(MK-PROD 34 '(EXP) '(MOP SIMPLE DOT))
	(MK-PROD 35 '(EXP) '(DOT SIMPLE DOP SIMPLE))
	(MK-PROD 35 '(EXP) '(SIMPLE DOT DOP SIMPLE))
	(MK-PROD 35 '(EXP) '(SIMPLE DOP DOT SIMPLE))
	(MK-PROD 35 '(EXP) '(SIMPLE DOP SIMPLE DOT))
	(MK-PROD 36 '(SIMPLE) '(DOT VAR))
	(MK-PROD 36 '(SIMPLE) '(VAR DOT))
	(MK-PROD 37 '(SIMPLE) '(DOT LITERAL))
	(MK-PROD 37 '(SIMPLE) '(LITERAL DOT))
	(MK-PROD 38 '(SIMPLE) '(DOT LP EXP RP))
	(MK-PROD 38 '(SIMPLE) '(LP DOT EXP RP))
	(MK-PROD 38 '(SIMPLE) '(LP EXP DOT RP))
	(MK-PROD 38 '(SIMPLE) '(LP EXP RP DOT))
	(MK-PROD 39 '(LITERAL) '(DOT INTEGER))
	(MK-PROD 39 '(LITERAL) '(INTEGER DOT))
	(MK-PROD 40 '(LITERAL) '(DOT TRUE))
	(MK-PROD 40 '(LITERAL) '(TRUE DOT))
	(MK-PROD 41 '(LITERAL) '(DOT FALSE))
	(MK-PROD 41 '(LITERAL) '(FALSE DOT))
	(MK-PROD 42 '(VAR) '(DOT IDENT))
	(MK-PROD 42 '(VAR) '(IDENT DOT))
	(MK-PROD 43 '(VAR) '(DOT IDENT LB EXP RB))
	(MK-PROD 43 '(VAR) '(IDENT DOT LB EXP RB))
	(MK-PROD 43 '(VAR) '(IDENT LB DOT EXP RB))
	(MK-PROD 43 '(VAR) '(IDENT LB EXP DOT RB))
	(MK-PROD 43 '(VAR) '(IDENT LB EXP RB DOT))
	(MK-PROD 44 '(DOP) '(DOT PLUS))
	(MK-PROD 44 '(DOP) '(PLUS DOT))
	(MK-PROD 45 '(DOP) '(DOT MINUS))
	(MK-PROD 45 '(DOP) '(MINUS DOT))
	(MK-PROD 46 '(DOP) '(DOT TIMES))
	(MK-PROD 46 '(DOP) '(TIMES DOT))
	(MK-PROD 47 '(DOP) '(DOT DIV))
	(MK-PROD 47 '(DOP) '(DIV DOT))
	(MK-PROD 48 '(DOP) '(DOT REM))
	(MK-PROD 48 '(DOP) '(REM DOT))
	(MK-PROD 49 '(DOP) '(DOT EQ))
	(MK-PROD 49 '(DOP) '(EQ DOT))
	(MK-PROD 50 '(DOP) '(DOT LT))
	(MK-PROD 50 '(DOP) '(LT DOT))
	(MK-PROD 51 '(DOP) '(DOT GT))
	(MK-PROD 51 '(DOP) '(GT DOT))
	(MK-PROD 52 '(DOP) '(DOT NE))
	(MK-PROD 52 '(DOP) '(NE DOT))
	(MK-PROD 53 '(DOP) '(DOT LE))
	(MK-PROD 53 '(DOP) '(LE DOT))
	(MK-PROD 54 '(DOP) '(DOT GE))
	(MK-PROD 54 '(DOP) '(GE DOT))
	(MK-PROD 55 '(DOP) '(DOT AND))
	(MK-PROD 55 '(DOP) '(AND DOT))
	(MK-PROD 56 '(DOP) '(DOT OR))
	(MK-PROD 56 '(DOP) '(OR DOT))
	(MK-PROD 57 '(MOP) '(DOT MINUS))
	(MK-PROD 57 '(MOP) '(MINUS DOT))
	(MK-PROD 58 '(MOP) '(DOT NOT))
	(MK-PROD 58 '(MOP) '(NOT DOT))))